Abstract is missing.
- Automatically Proving Program TerminationByron Cook. 1 [doi]
- A Mathematical Approach to RTL VerificationDavid M. Russinoff. 2 [doi]
- Software Bugs Seen from an Industrial Perspective or Can Formal Methods Help on Automotive Software Development?Thomas Kropf. 3 [doi]
- Algorithms for Interface SynthesisDirk Beyer, Thomas A. Henzinger, Vasu Singh. 4-19 [doi]
- A Tutorial on Satisfiability Modulo TheoriesLeonardo Mendonça de Moura, Bruno Dutertre, Natarajan Shankar. 20-36 [doi]
- A JML Tutorial: Modular Specification and Verification of Functional Behavior for JavaGary T. Leavens, Joseph R. Kiniry, Erik Poll. 37 [doi]
- Verification of Hybrid SystemsMartin Fränzle. 38 [doi]
- SAT-Based Compositional Verification Using Lazy LearningNishant Sinha, Edmund M. Clarke. 39-54 [doi]
- Local Proofs for Global Safety PropertiesAriel Cohen 0002, Kedar S. Namjoshi. 55-67 [doi]
- Low-Level Library Analysis and SummarizationDenis Gopan, Thomas W. Reps. 68-81 [doi]
- Verification Across Intellectual Property BoundariesSagar Chaki, Christian Schallhart, Helmut Veith. 82-94 [doi]
- On Synthesizing Controllers from Bounded-Response PropertiesOded Maler, Dejan Nickovic, Amir Pnueli. 95-107 [doi]
- An Accelerated Algorithm for 3-Color Parity Games with an Application to Timed GamesLuca de Alfaro, Marco Faella. 108-120 [doi]
- UPPAAL-Tiga: Time for Playing Games!Gerd Behrmann, Agnès Cougnard, Alexandre David, Emmanuel Fleury, Kim Guldstrand Larsen, Didier Lime. 121-125 [doi]
- The TASM Toolset: Specification, Simulation, and Formal Verification of Real-Time SystemsMartin Ouimet, Kristina Lundqvist. 126-130 [doi]
- Systematic Acceleration in Regular Model CheckingBengt Jonsson, Mayank Saksena. 131-144 [doi]
- Parameterized Verification of Infinite-State Processes with Global ConditionsParosh Aziz Abdulla, Giorgio Delzanno, Ahmed Rezine. 145-157 [doi]
- CADP 2006: A Toolbox for the Construction and Analysis of Distributed ProcessesHubert Garavel, Radu Mateescu, Frédéric Lang, Wendelin Serwe. 158-163 [doi]
- jMoped: A Test Environment for Java ProgramsDejvuth Suwimonteerabuth, Felix Berger, Stefan Schwoon, Javier Esparza. 164-167 [doi]
- Hector: Software Model Checking with Cooperating Analysis PluginsNathaniel Charlton, Michael Huth. 168-172 [doi]
- The Why/Krakatoa/Caduceus Platform for Deductive Program VerificationJean-Christophe Filliâtre, Claude Marché. 173-177 [doi]
- Shape Analysis for Composite Data StructuresJosh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O Hearn, Thomas Wies, Hongseok Yang. 178-192 [doi]
- Array Abstractions from ProofsRanjit Jhala, Kenneth L. McMillan. 193-206 [doi]
- Context-Bounded Analysis of Multithreaded Programs with Dynamic Linked StructuresAhmed Bouajjani, Séverine Fratani, Shaz Qadeer. 207-220 [doi]
- Revamping TVLA: Making Parametric Shape Analysis CompetitiveIgor Bogudlov, Tal Lev-Ami, Thomas W. Reps, Mooly Sagiv. 221-225 [doi]
- Fast and Accurate Static Data-Race Detection for Concurrent ProgramsVineet Kahlon, Yu Yang, Sriram Sankaranarayanan, Aarti Gupta. 226-239 [doi]
- Parametric and Sliced CausalityFeng Chen, Grigore Rosu. 240-253 [doi]
- Spade: Verification of Multithreaded Dynamic and Recursive ProgramsGaël Patin, Mihaela Sighireanu, Tayssir Touili. 254-257 [doi]
- Anzu: A Tool for Property SynthesisBarbara Jobstmann, Stefan Galler, Martin Weiglhofer, Roderick Bloem. 258-262 [doi]
- RAT: A Tool for the Formal Analysis of RequirementsRoderick Bloem, Roberto Cavada, Ingo Pill, Marco Roveri, Andrei Tchaltsev. 263-267 [doi]
- Parallelising Symbolic State-Space GeneratorsJonathan Ezekiel, Gerald Lüttgen, Gianfranco Ciardo. 268-280 [doi]
- I/O Efficient Accepting Cycle DetectionJiri Barnat, Lubos Brim, Pavel Simecek. 281-293 [doi]
- C32SAT: Checking C ExpressionsRobert Brummayer, Armin Biere. 294-297 [doi]
- CVC3Clark Barrett, Cesare Tinelli. 298-302 [doi]
- BAT: The Bit-Level Analysis ToolPanagiotis Manolios, Sudarshan K. Srinivasan, Daron Vroon. 303-306 [doi]
- LIRA: Handling Constraints of Linear Arithmetics over the Integers and the RealsBernd Becker, Christian Dax, Jochen Eisinger, Felix Klaedtke. 307-310 [doi]
- Three-Valued Abstraction for Continuous-Time Markov ChainsJoost-Pieter Katoen, Daniel Klink, Martin Leucker, Verena Wolf. 311-324 [doi]
- Magnifying-Lens Abstraction for Markov Decision ProcessesLuca de Alfaro, Pritam Roy. 325-338 [doi]
- Underapproximation for Model-Checking Based on Random Cryptographic ConstructionsArie Matsliah, Ofer Strichman. 339-351 [doi]
- Using Counterexamples for Improving the Precision of Reachability Computation with PolyhedraChao Wang, Zijiang Yang, Aarti Gupta, Franjo Ivancic. 352-365 [doi]
- Structural Abstraction of Software Verification ConditionsDomagoj Babic, Alan J. Hu. 366-378 [doi]
- An Abstract Domain for Analyzing Heap-Manipulating Low-Level SoftwareSumit Gulwani, Ashish Tiwari. 379-392 [doi]
- Adaptive Symmetry ReductionThomas Wahl. 393-405 [doi]
- From Liveness to PromptnessOrna Kupferman, Nir Piterman, Moshe Y. Vardi. 406-419 [doi]
- Automated Assumption Generation for Compositional VerificationAnubhav Gupta, Kenneth L. McMillan, Zhaohui Fu. 420-432 [doi]
- Abstraction and Counterexample-Guided Construction of ::::omega:::: -Automata for Model Checking of Step-Discrete Linear Hybrid ModelsMarc Segelken. 433-448 [doi]
- Test Coverage for Continuous and Hybrid SystemsTarik Nahhal, Thao Dang. 449-462 [doi]
- Hybrid Systems: From Verification to FalsificationErion Plaku, Lydia E. Kavraki, Moshe Y. Vardi. 463-476 [doi]
- Comparison Under Abstraction for Verifying LinearizabilityDaphna Amit, Noam Rinetzky, Thomas W. Reps, Mooly Sagiv, Eran Yahav. 477-490 [doi]
- Leaping Loops in the Presence of AbstractionThomas Ball, Orna Kupferman, Mooly Sagiv. 491-503 [doi]
- Configurable Software Verification: Concretizing the Convergence of Model Checking and Program AnalysisDirk Beyer, Thomas A. Henzinger, Grégory Théoduloz. 504-518 [doi]
- A Decision Procedure for Bit-Vectors and ArraysVijay Ganesh, David L. Dill. 519-531 [doi]
- Boolean Abstraction for Temporal Logic SatisfiabilityAlessandro Cimatti, Marco Roveri, Viktor Schuppan, Stefano Tonetta. 532-546 [doi]
- A Lazy and Layered SMT( /mathcal{BV} ) Solver for Hard Industrial Verification ProblemsRoberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Ziyad Hanna, Alexander Nadel, Amit Palti, Roberto Sebastiani. 547-560 [doi]