Table of Contents

• Software Analysis and Model CheckingGerard J. Holzmann. 1-16 [doi]
• The Quest for Efficient Boolean Satisfiability SolversLintao Zhang, Sharad Malik. 17-36 [doi]
• On Abstraction in Software VerificationPatrick Cousot, Radhia Cousot. 37-56 [doi]
• The Symbolic Approach to Hybrid SystemsThomas A. Henzinger. 57 [doi]
• Infinite Games and Verification (Extended Abstract of a Tutorial)Wolfgang Thomas. 58-64 [doi]
• Symbolic Localization Reduction with Reconstruction Layering and BacktrackingSharon Barner, Daniel Geist, Anna Gringauze. 65-77 [doi]
• Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted FunctionsRandal E. Bryant, Shuvendu K. Lahiri, Sanjit A. Seshia. 78-92 [doi]
• Combining Symmetry Reduction and Under-Approximation for Symbolic Model CheckingSharon Barner, Orna Grumberg. 93-106 [doi]
• Liveness with (0, 1, infty)-Counter AbstractionAmir Pnueli, Jessie Xu, Lenore D. Zuck. 107-122 [doi]
• Shared Memory Consistency Protocol Verification Against Weak Memory Models: Refinement via Model-CheckingProsenjit Chatterjee, Hemanthkumar Sivaraj, Ganesh Gopalakrishnan. 123-136 [doi]
• Automatic Abstraction Using Generalized Model CheckingPatrice Godefroid, Radha Jagadeesan. 137-150 [doi]
• Property Checking via Structural AnalysisJason Baumgartner, Andreas Kuehlmann, Jacob A. Abraham. 151-165 [doi]
• Conformance Checking for Models of Asynchronous Message Passing SoftwareSriram K. Rajamani, Jakob Rehof. 166-179 [doi]
• A Modular Checker for Multithreaded ProgramsCormac Flanagan, Shaz Qadeer, Sanjit A. Seshia. 180-194 [doi]
• Automatic Derivation of Timing Constraints by Failure AnalysisTomohiro Yoneda, Tomoya Kitai, Chris J. Myers. 195-208 [doi]
• Deciding Separation Formulas with SATOfer Strichman, Sanjit A. Seshia, Randal E. Bryant. 209-222 [doi]
• Probabilistic Verification of Discrete Event Systems Using Acceptance SamplingHåkan L. S. Younes, Reid G. Simmons. 223-235 [doi]
• Checking Satisfiability of First-Order Formulas by Incremental Translation to SATClark W. Barrett, David L. Dill, Aaron Stump. 236-249 [doi]
• Applying SAT Methods in Unbounded Symbolic Model CheckingKenneth L. McMillan. 250-264 [doi]
• SAT Based Abstraction-Refinement Using ILP and Machine Learning TechniquesEdmund M. Clarke, Anubhav Gupta, James H. Kukula, Ofer Strichman. 265-279 [doi]
• Semi-formal Bounded Model CheckingJesse D. Bingham, Alan J. Hu. 280-294 [doi]
• Algorithmic Verification of Invalidation-Based ProtocolsMarco Bozzano, Giorgio Delzanno. 295-308 [doi]
• Formal Verification of Complex Out-of-Order Pipelines by Combining Model-Checking and Theorem-ProvingChristian Jacobi 0002. 309-323 [doi]
• Automated Unbounded Verification of Security ProtocolsYannick Chevalier, Laurent Vigneron. 324-337 [doi]
• Exploiting Behavioral Hierarchy for Efficient Model CheckingRajeev Alur, Michael McDougall, Zijiang Yang. 338-342 [doi]
• IF-2.0: A Validation Environment for Component-Based Real-Time SystemsMarius Bozga, Susanne Graf, Laurent Mounier. 343-348 [doi]
• The AVISS Security Protocol Analysis ToolAlessandro Armando, David A. Basin, Mehdi Bouallagui, Yannick Chevalier, Luca Compagna, Sebastian Mödersheim, Michaël Rusinowitch, Mathieu Turuani, Luca Viganò, Laurent Vigneron. 349-353 [doi]
• SPeeDI - A Verification Tool for Polygonal Hybrid SystemsEugene Asarin, Gordon J. Pace, Gerardo Schneider, Sergio Yovine. 354-358 [doi]
• NuSMV 2: An OpenSource Tool for Symbolic Model CheckingAlessandro Cimatti, Edmund M. Clarke, Enrico Giunchiglia, Fausto Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, Armando Tacchella. 359-364 [doi]
• The d/dt Tool for Verification of Hybrid SystemsEugene Asarin, Thao Dang, Oded Maler. 365-370 [doi]
• Model Checking Linear Properties of Prefix-Recognizable SystemsOrna Kupferman, Nir Piterman, Moshe Y. Vardi. 371-385 [doi]
• Using Canonical Representations of Solutions to Speed Up Infinite-State Model CheckingTatiana Rybina, Andrei Voronkov. 386-400 [doi]
• On Discrete Modeling and Model Checking for Nonlinear Analog SystemsWalter Hartong, Lars Hedrich, Erich Barke. 401-413 [doi]
• Synchronous and Bidirectional Component InterfacesArindam Chakrabarti, Luca de Alfaro, Thomas A. Henzinger, Freddy Y. C. Mang. 414-427 [doi]
• Interface Compatibility Checking for Software ModulesArindam Chakrabarti, Luca de Alfaro, Thomas A. Henzinger, Marcin Jurdzinski, Freddy Y. C. Mang. 428-441 [doi]
• Practical Methods for Proving Program TerminationMichael Colón, Henny Sipma. 442-454 [doi]
• Evidence-Based Model CheckingLi Tan, Rance Cleaveland. 455-470 [doi]
• Mixing Forward and Backward Traversals in Guided-Prioritized BDD-Based VerificationGianpiero Cabodi, Sergio Nocco, Stefano Quer. 471-484 [doi]
• Vacuum Cleaning CTL FormulaeMitra Purandare, Fabio Somenzi. 485-499 [doi]
• CVC: A Cooperating Validity CheckerAaron Stump, Clark W. Barrett, David L. Dill. 500-504 [doi]
• chi-Chek: A Multi-valued Model-CheckerMarsha Chechik, Arie Gurfinkel, Benet Devereux. 505-509 [doi]
• PathFinder: A Tool for Design ExplorationShoham Ben-David, Anna Gringauze, Baruch Sterin, Yaron Wolfsthal. 510-514 [doi]
• Abstracting C with abCDennis Dams, William Hesse, Gerard J. Holzmann. 515-520 [doi]
• AMC: An Adaptive Model CheckerAlex Groce, Doron Peled, Mihalis Yannakakis. 521-525 [doi]
• Temporal-Safety Proofs for Systems CodeThomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, George C. Necula, Grégoire Sutre, Westley Weimer. 526-538 [doi]
• Extrapolating Tree TransformationsAhmed Bouajjani, Tayssir Touili. 539-554 [doi]
• Regular Tree Model CheckingParosh Aziz Abdulla, Bengt Jonsson, Pritha Mahata, Julien d Orso. 555-568 [doi]
• Compressing Transitions for Model CheckingRobert P. Kurshan, Vladimir Levin, Hüsnü Yenigün. 569-581 [doi]
• Canonical Prefixes of Petri Net UnfoldingsVictor Khomenko, Maciej Koutny, Walter Vogler. 582-595 [doi]
• State Space Reduction by Proving ConfluenceStefan Blom, Jaco van de Pol. 596-609 [doi]
• Fair Simulation MinimizationSankar Gurumurthy, Roderick Bloem, Fabio Somenzi. 610-624 [doi]