Abstract is missing.
- Randomized Algorithms for Program Analysis and VerificationGeorge C. Necula, Sumit Gulwani. 1 [doi]
- Validating a Modern MicroprocessorBob Bentley. 2-4 [doi]
- Algorithmic Algebraic Model Checking I: Challenges from Systems BiologyCarla Piazza, Marco Antoniotti, Venkatesh Mysore, Alberto Policriti, Franz Winkler, Bud Mishra. 5-19 [doi]
- SMT-COMP: Satisfiability Modulo Theories CompetitionClark W. Barrett, Leonardo Mendonça de Moura, Aaron Stump. 20-23 [doi]
- Predicate Abstraction via Symbolic Decision ProceduresShuvendu K. Lahiri, Thomas Ball, Byron Cook. 24-38 [doi]
- Interpolant-Based Transition Relation ApproximationRanjit Jhala, Kenneth L. McMillan. 39-51 [doi]
- Concrete Model Checking with Abstract Matching and RefinementCorina S. Pasareanu, Radek Pelánek, Willem Visser. 52-66 [doi]
- Abstraction for FalsificationThomas Ball, Orna Kupferman, Greta Yorsh. 67-81 [doi]
- Bounded Model Checking of Concurrent ProgramsIshai Rabinovitz, Orna Grumberg. 82-97 [doi]
- Incremental and Complete Bounded Model Checking for Full PLTLKeijo Heljanko, Tommi A. Junttila, Timo Latvala. 98-111 [doi]
- Abstraction Refinement for Bounded Model CheckingAnubhav Gupta, Ofer Strichman. 112-124 [doi]
- Symmetry Reduction in SAT-Based Model CheckingDaijue Tang, Sharad Malik, Aarti Gupta, C. Norris Ip. 125-138 [doi]
- Saturn: A SAT-Based Tool for Bug DetectionYichen Xie, Alexander Aiken. 139-143 [doi]
- JVer: A Java VerifierAjay Chander, David Espinosa, Nayeem Islam, Peter Lee, George C. Necula. 144-147 [doi]
- Building Your Own Software Model Checker Using the Bogor Extensible Model Checking FrameworkMatthew B. Dwyer, John Hatcliff, Matthew Hoosier, Robby. 148-152 [doi]
- Wolf - Bug Hunter for Concurrent Software Using Formal MethodsSharon Barner, Ziv Glazberg, Ishai Rabinovitz. 153-157 [doi]
- Model Checking x86 Executables with CodeSurfer/x86 and WPDS++Gogul Balakrishnan, Thomas W. Reps, Nicholas Kidd, Akash Lal, Junghee Lim, David Melski, Radu Gruian, Suan Hsi Yong, Chi-Hua Chen, Tim Teitelbaum. 158-163 [doi]
- The ComFoRT Reasoning FrameworkSagar Chaki, James Ivers, Natasha Sharygina, Kurt C. Wallnau. 164-169 [doi]
- Formal Verification of Pentium® 4 Components with Symbolic Simulation and Inductive InvariantsRoope Kaivola. 170-184 [doi]
- Formal Verification of Backward Compatibility of MicrocodeTamarah Arons, Elad Elster, Limor Fix, Sela Mador-Haim, Michael Mishaeli, Jonathan Shalev, Eli Singerman, Andreas Tiemeyer, Moshe Y. Vardi, Lenore D. Zuck. 185-198 [doi]
- Compositional Analysis of Floating-Point Linear Numerical FiltersDavid Monniaux. 199-212 [doi]
- Syntax-Driven Reachable State Space Construction of Synchronous Reactive ProgramsEric Vecchié, Robert de Simone. 213-225 [doi]
- Program Repair as a GameBarbara Jobstmann, Andreas Griesmayer, Roderick Bloem. 226-238 [doi]
- Improved Probabilistic Models for 802.11 Protocol VerificationAmitabha Roy 0002, K. Gopinath. 239-252 [doi]
- Probabilistic Verification for Black-Box SystemsHåkan L. S. Younes. 253-265 [doi]
- On Statistical Model Checking of Stochastic SystemsKoushik Sen, Mahesh Viswanathan, Gul Agha. 266-280 [doi]
- The AVISPA Tool for the Automated Validation of Internet Security Protocols and ApplicationsAlessandro Armando, David A. Basin, Yohan Boichut, Yannick Chevalier, Luca Compagna, Jorge Cuéllar, Paul Hankes Drielsma, Pierre-Cyrille Héam, Olga Kouchnarenko, Jacopo Mantovani, Sebastian Mödersheim, David von Oheimb, Michaël Rusinowitch, Judson Santiago, Mathieu Turuani, Luca Viganò, Laurent Vigneron. 281-285 [doi]
- The Orchids Intrusion Detection ToolJulien Olivain, Jean Goubault-Larrecq. 286-290 [doi]
- TVOC: A Translation Validator for Optimizing CompilersClark W. Barrett, Yi Fang, Benjamin Goldberg, Ying Hu, Amir Pnueli, Lenore D. Zuck. 291-295 [doi]
- Cogent: Accurate Theorem Proving for Program VerificationByron Cook, Daniel Kroening, Natasha Sharygina. 296-300 [doi]
- F-Soft: Software Verification PlatformFranjo Ivancic, Zijiang Yang, Malay K. Ganai, Aarti Gupta, Ilya Shlyakhter, Pranav Ashar. 301-306 [doi]
- Yet Another Decision Procedure for Equality LogicOrly Meir, Ofer Strichman. 307-320 [doi]
- DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference LogicRobert Nieuwenhuis, Albert Oliveras. 321-334 [doi]
- Efficient Satisfiability Modulo Theories via Delayed Theory CombinationMarco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Silvio Ranise, Peter van Rossum, Roberto Sebastiani. 335-349 [doi]
- Symbolic Systems, Explicit Properties: On Hybrid Approaches for LTL Symbolic Model CheckingRoberto Sebastiani, Stefano Tonetta, Moshe Y. Vardi. 350-363 [doi]
- Efficient Monitoring of omega-LanguagesMarcelo d Amorim, Grigore Rosu. 364-378 [doi]
- Verification of Tree Updates for OptimizationMichael Benedikt, Angela Bonifati, Sergio Flesca, Avinash Vyas. 379-393 [doi]
- Expand, Enlarge and Check... Made EfficientGilles Geeraerts, Jean-François Raskin, Laurent Van Begin. 394-407 [doi]
- IIV: An Invisible Invariant VerifierIttai Balaban, Yi Fang, Amir Pnueli, Lenore D. Zuck. 408-412 [doi]
- Action Language Verifier, ExtendedTuba Yavuz-Kahveci, Constantinos Bartzis, Tevfik Bultan. 413-417 [doi]
- Romeo: A Tool for Analyzing Time Petri NetsGuillaume Gardey, Didier Lime, Morgan Magnin, Olivier H. Roux. 418-423 [doi]
- TRANSYT: A Tool for the Verification of Asynchronous Concurrent SystemsEnric Pastor, Marco A. Peña, Marc Solé. 424-428 [doi]
- Ymer: A Statistical Model CheckerHåkan L. S. Younes. 429-433 [doi]
- Extended Weighted Pushdown SystemsAkash Lal, Thomas W. Reps, Gogul Balakrishnan. 434-448 [doi]
- Incremental Algorithms for Inter-procedural Analysis of Safety PropertiesChristopher L. Conway, Kedar S. Namjoshi, Dennis Dams, Stephen A. Edwards. 449-461 [doi]
- A Policy Iteration Algorithm for Computing Fixed Points in Static Analysis of ProgramsAlexandru Costan, Stephane Gaubert, Eric Goubault, Matthieu Martel, Sylvie Putot. 462-475 [doi]
- Data Structure Specifications via Local Equality AxiomsScott McPeak, George C. Necula. 476-490 [doi]
- Linear Ranking with ReachabilityAaron R. Bradley, Zohar Manna, Henny B. Sipma. 491-504 [doi]
- Reasoning About Threads Communicating via LocksVineet Kahlon, Franjo Ivancic, Aarti Gupta. 505-518 [doi]
- Abstraction Refinement via Inductive LearningAlexey Loginov, Thomas W. Reps, Shmuel Sagiv. 519-533 [doi]
- Automated Assume-Guarantee Reasoning for Simulation ConformanceSagar Chaki, Edmund M. Clarke, Nishant Sinha, Prasanna Thati. 534-547 [doi]
- Symbolic Compositional Verification by Learning AssumptionsRajeev Alur, P. Madhusudan, Wonhong Nam. 548-562 [doi]