Invited Talks

• 
  Manuvir Das: Formal Specifications on Industrial-Strength Code-From Myth to Reality. 1
• 
  David L. Dill: I Think I Voted: E-Voting vs. Democracy. 2
• 
  David Harel: Playing with Verification, Planning and Aspects: Unusual Methods for Running Scenario-Based Programs. 3-4
• 
  Tony Hoare: The Ideal of Verified Software. 5-16

Automata

• 
  Martin De Wulf, Laurent Doyen, Thomas A. Henzinger, Jean-François Raskin: Antichains: A New Algorithm for Checking Universality of Finite Automata. 17-30
• 
  Orna Kupferman, Nir Piterman, Moshe Y. Vardi: Safraless Compositional Synthesis. 31-44
• 
  Sudeep Juvekar, Nir Piterman: Minimizing Generalized Büchi Automata. 45-58

Tool Papers

• 
  B. Thomas Adler, Luca de Alfaro, Leandro Dias da Silva, Marco Faella, Axel Legay, Vishwanath Raman, Pritam Roy: Ticc: A Tool for Interface Compatibility and Composition. 59-62
• 
  Sébastien Bardin, Jérôme Leroux, Gérald Point: FAST Extended Release. 63-66

Arithmetic

• 
  Jochen Eisinger, Felix Klaedtke: Don't Care Words with an Application to the Automata-Based Approach for Real Addition. 67-80
• 
  Bruno Dutertre, Leonardo Mendonça de Moura: A Fast Linear-Arithmetic Solver for DPLL(T). 81-94

SAT and Bounded Model Checking

• 
  Keijo Heljanko, Tommi A. Junttila, Misa Keinänen, Martin Lange, Timo Latvala: Bounded Model Checking for Weak Alternating Büchi Automata. 95-108
• 
  Roman Gershman, Maya Koifman, Ofer Strichman: Deriving Small Unsatisfiable Cores with Dominators. 109-122

Abstraction/Refinement

• 
  Kenneth L. McMillan: Lazy Abstraction with Interpolants. 123-136
• 
  Himanshu Jain, Franjo Ivancic, Aarti Gupta, Ilya Shlyakhter, Chao Wang: Using Statically Computed Invariants Inside the Predicate Abstraction and Refinement Loop. 137-151
• 
  Daniel Kroening, Georg Weissenbacher: Counterexamples with Loops for Predicate Abstraction. 152-165

Tool Papers

• 
  Nikhil Sethi, Clark Barrett: cascade: C Assertion Checker and Deductive Engine. 166-169
• 
  Arie Gurfinkel, Ou Wei, Marsha Chechik: Yasm: A Software Model-Checker for Verification and Refutation. 170-174

Symbolic Trajectory Evaluation

• 
  Jan-Willem Roorda, Koen Claessen: SAT-Based Assistance in Abstraction Refinement for Symbolic Trajectory Evaluation. 175-189
• 
  Rachel Tzoref, Orna Grumberg: Automatic Refinement and Vacuity Detection for Symbolic Trajectory Evaluation. 190-204

Property Specification and Verification

• 
  Doron Bustan, John Havlicek: Some Complexity Results for SystemVerilog Assertions. 205-218
• 
  Jochen Klose, Tobe Toben, Bernd Westphal, Hartmut Wittke: Check It Out: On the Efficient Formal Verification of Live Sequence Charts. 219-233

Time

• 
  Marta Z. Kwiatkowska, Gethin Norman, David Parker: Symmetry Reduction for Probabilistic Model Checking. 234-248
• 
  Pavel Krcál, Wang Yi: Communicating Timed Automata: The More Synchronous, the More Difficult to Verify. 249-262
• 
  Grigore Rosu, Saddek Bensalem: Allen Linear (Interval) Temporal Logic - Translation to LTL and Monitor Synthesis. 263-277

Tool Papers

• 
  Jiri Barnat, Lubos Brim, Ivana Cerná, Pavel Moravec, Petr Rockai, Pavel Simecek: DiVinE - A Tool for Distributed Verification. 278-281
• 
  Flavio M. de Paula, Alan J. Hu: EverLost: A Flexible Platform for Industrial-Strength Abstraction-Guided Simulation. 282-285

Concurrency

• 
  Vineet Kahlon, Aarti Gupta, Nishant Sinha: Symbolic Model Checking of Concurrent Programs Using Partial Orders and On-the-Fly Transactions. 286-299
• 
  Koushik Sen, Mahesh Viswanathan: Model Checking Multithreaded Programs with Asynchronous Atomic Methods. 300-314
• 
  Azadeh Farzan, P. Madhusudan: Causal Atomicity. 315-328

Trees, Pushdown Systems and Boolean Programs

• 
  Rajeev Alur, Swarat Chaudhuri, P. Madhusudan: Languages of Nested Trees. 329-342
• 
  Akash Lal, Thomas W. Reps: Improving Pushdown System Model Checking. 343-357
• 
  Andreas Griesmayer, Roderick Bloem, Byron Cook: Repair of Boolean Programs with an Application to C. 358-371

Termination

• 
  Mark Braverman: Termination of Integer Linear Programs. 372-385
• 
  Josh Berdine, Byron Cook, Dino Distefano, Peter W. O'Hearn: Automatic Termination Proofs for Programs with Shape-Shifting Heaps. 386-400
• 
  Panagiotis Manolios, Daron Vroon: Termination Analysis with Calling Context Graphs. 401-414

Tool Papers

• 
  Byron Cook, Andreas Podelski, Andrey Rybalchenko: Terminator: Beyond Safety. 415-418
• 
  Koushik Sen, Gul Agha: CUTE and jCUTE: Concolic Unit Testing and Explicit Path Model-Checking Tools. 419-423

Abstract Interpretation

• 
  Shuvendu K. Lahiri, Robert Nieuwenhuis, Albert Oliveras: SMT Techniques for Fast Predicate Abstraction. 424-437
• 
  Bernard Boigelot, Frédéric Herbreteau: The Power of Hybrid Acceleration. 438-451
• 
  Denis Gopan, Thomas W. Reps: Lookahead Widening. 452-466

Tool Papers

• 
  Kenneth Roe: The Heuristic Theorem Prover: Yet Another SMT Modulo Theorem Prover. 467-470
• 
  Abhay Vardhan, Mahesh Viswanathan: LEVER: A Tool for Learning Based Verification. 471-474

Memory Consistency

• 
  Robert Colvin, Lindsay Groves, Victor Luchangco, Mark Moir: Formal Verification of a Lazy Concurrent List-Based Set Algorithm. 475-488
• 
  Sebastian Burckhardt, Rajeev Alur, Milo M. K. Martin: Bounded Model Checking of Concurrent Data Types on Relaxed Memory Models: A Case Study. 489-502
• 
  Amitabha Roy, Stephan Zeisset, Charles J. Fleckenstein, John C. Huang: Fast and Generalized Polynomial Time Memory Consistency Verification. 503-516

Shape Analysis

• 
  Ahmed Bouajjani, Marius Bozga, Peter Habermehl, Radu Iosif, Pierre Moro, Tomás Vojnar: Programs with Lists Are Counter Automata. 517-531
• 
  Dirk Beyer, Thomas A. Henzinger, Grégory Théoduloz: Lazy Shape Analysis. 532-546
• 
  Tal Lev-Ami, Neil Immerman, Shmuel Sagiv: Abstraction for Shape Analysis with Fast and Precise Transformers. 547-561

last updated on Sat May 18 04:43:25 2013 by the dblp team
data released under the ODC-BY 1.0 license
see also our legal information page