Table of Contents

• Formal Specifications on Industrial-Strength Code-From Myth to RealityManuvir Das. 1 [doi]
• I Think I Voted: E-Voting vs. DemocracyDavid L. Dill. 2 [doi]
• Playing with Verification, Planning and Aspects: Unusual Methods for Running Scenario-Based ProgramsDavid Harel. 3-4 [doi]
• The Ideal of Verified SoftwareTony Hoare. 5-16 [doi]
• Antichains: A New Algorithm for Checking Universality of Finite AutomataMartin De Wulf, Laurent Doyen, Thomas A. Henzinger, Jean-François Raskin. 17-30 [doi]
• Safraless Compositional SynthesisOrna Kupferman, Nir Piterman, Moshe Y. Vardi. 31-44 [doi]
• Minimizing Generalized Büchi AutomataSudeep Juvekar, Nir Piterman. 45-58 [doi]
• Ticc: A Tool for Interface Compatibility and CompositionB. Thomas Adler, Luca de Alfaro, Leandro Dias da Silva, Marco Faella, Axel Legay, Vishwanath Raman, Pritam Roy. 59-62 [doi]
• FAST Extended ReleaseSébastien Bardin, Jérôme Leroux, Gérald Point. 63-66 [doi]
• Don t Care Words with an Application to the Automata-Based Approach for Real AdditionJochen Eisinger, Felix Klaedtke. 67-80 [doi]
• A Fast Linear-Arithmetic Solver for DPLL(T)Bruno Dutertre, Leonardo Mendonça de Moura. 81-94 [doi]
• Bounded Model Checking for Weak Alternating Büchi AutomataKeijo Heljanko, Tommi A. Junttila, Misa Keinänen, Martin Lange, Timo Latvala. 95-108 [doi]
• Deriving Small Unsatisfiable Cores with DominatorsRoman Gershman, Maya Koifman, Ofer Strichman. 109-122 [doi]
• Lazy Abstraction with InterpolantsKenneth L. McMillan. 123-136 [doi]
• Using Statically Computed Invariants Inside the Predicate Abstraction and Refinement LoopHimanshu Jain, Franjo Ivancic, Aarti Gupta, Ilya Shlyakhter, Chao Wang. 137-151 [doi]
• Counterexamples with Loops for Predicate AbstractionDaniel Kroening, Georg Weissenbacher. 152-165 [doi]
• cascade: C Assertion Checker and Deductive EngineNikhil Sethi, Clark Barrett. 166-169 [doi]
• Yasm: A Software Model-Checker for Verification and RefutationArie Gurfinkel, Ou Wei, Marsha Chechik. 170-174 [doi]
• SAT-Based Assistance in Abstraction Refinement for Symbolic Trajectory EvaluationJan-Willem Roorda, Koen Claessen. 175-189 [doi]
• Automatic Refinement and Vacuity Detection for Symbolic Trajectory EvaluationRachel Tzoref, Orna Grumberg. 190-204 [doi]
• Some Complexity Results for SystemVerilog AssertionsDoron Bustan, John Havlicek. 205-218 [doi]
• Check It Out: On the Efficient Formal Verification of Live Sequence ChartsJochen Klose, Tobe Toben, Bernd Westphal, Hartmut Wittke. 219-233 [doi]
• Symmetry Reduction for Probabilistic Model CheckingMarta Z. Kwiatkowska, Gethin J. Norman, David Parker. 234-248 [doi]
• Communicating Timed Automata: The More Synchronous, the More Difficult to VerifyPavel Krcál, Wang Yi. 249-262 [doi]
• Allen Linear (Interval) Temporal Logic - Translation to LTL and Monitor SynthesisGrigore Rosu, Saddek Bensalem. 263-277 [doi]
• DiVinE - A Tool for Distributed VerificationJiri Barnat, Lubos Brim, Ivana Cerná, Pavel Moravec 0002, Petr Rockai, Pavel Simecek. 278-281 [doi]
• EverLost: A Flexible Platform for Industrial-Strength Abstraction-Guided SimulationFlavio M. de Paula, Alan J. Hu. 282-285 [doi]
• Symbolic Model Checking of Concurrent Programs Using Partial Orders and On-the-Fly TransactionsVineet Kahlon, Aarti Gupta, Nishant Sinha. 286-299 [doi]
• Model Checking Multithreaded Programs with Asynchronous Atomic MethodsKoushik Sen, Mahesh Viswanathan. 300-314 [doi]
• Causal AtomicityAzadeh Farzan, P. Madhusudan. 315-328 [doi]
• Languages of Nested TreesRajeev Alur, Swarat Chaudhuri, P. Madhusudan. 329-342 [doi]
• Improving Pushdown System Model CheckingAkash Lal, Thomas W. Reps. 343-357 [doi]
• Repair of Boolean Programs with an Application to CAndreas Griesmayer, Roderick Bloem, Byron Cook. 358-371 [doi]
• Termination of Integer Linear ProgramsMark Braverman. 372-385 [doi]
• Automatic Termination Proofs for Programs with Shape-Shifting HeapsJosh Berdine, Byron Cook, Dino Distefano, Peter W. O Hearn. 386-400 [doi]
• Termination Analysis with Calling Context GraphsPanagiotis Manolios, Daron Vroon. 401-414 [doi]
• Terminator: Beyond SafetyByron Cook, Andreas Podelski, Andrey Rybalchenko. 415-418 [doi]
• CUTE and jCUTE: Concolic Unit Testing and Explicit Path Model-Checking ToolsKoushik Sen, Gul Agha. 419-423 [doi]
• SMT Techniques for Fast Predicate AbstractionShuvendu K. Lahiri, Robert Nieuwenhuis, Albert Oliveras. 424-437 [doi]
• The Power of Hybrid AccelerationBernard Boigelot, Frédéric Herbreteau. 438-451 [doi]
• Lookahead WideningDenis Gopan, Thomas W. Reps. 452-466 [doi]
• The Heuristic Theorem Prover: Yet Another SMT Modulo Theorem ProverKenneth Roe. 467-470 [doi]
• LEVER: A Tool for Learning Based VerificationAbhay Vardhan, Mahesh Viswanathan. 471-474 [doi]
• Formal Verification of a Lazy Concurrent List-Based Set AlgorithmRobert Colvin, Lindsay Groves, Victor Luchangco, Mark Moir. 475-488 [doi]
• Bounded Model Checking of Concurrent Data Types on Relaxed Memory Models: A Case StudySebastian Burckhardt, Rajeev Alur, Milo M. K. Martin. 489-502 [doi]
• Fast and Generalized Polynomial Time Memory Consistency VerificationAmitabha Roy 0002, Stephan Zeisset, Charles J. Fleckenstein, John C. Huang. 503-516 [doi]
• Programs with Lists Are Counter AutomataAhmed Bouajjani, Marius Bozga, Peter Habermehl, Radu Iosif, Pierre Moro, Tomás Vojnar. 517-531 [doi]
• Lazy Shape AnalysisDirk Beyer, Thomas A. Henzinger, Grégory Théoduloz. 532-546 [doi]
• Abstraction for Shape Analysis with Fast and Precise TransformersTal Lev-Ami, Neil Immerman, Shmuel Sagiv. 547-561 [doi]