Welcome

Verifying Programs with 1-Selector-Linked Structures in Regular Model Checking
Ahmed Bouajjani, Peter Habermehl, Pierre Moro (Univ. Paris VII, France) and Tomáš Vojnar (Brno Univ. of Technology, Czech Republic)

Simulation-Based Iteration of Tree Transducers
Parosh Aziz Abdulla (Uppsala Univ., Sweden), Axel Legay (Univ. of Liège, Belgium), Julien d'Orso (CRCCyN-UMR CNRS, France) and Ahmed Rezine (Uppsala Univ., Sweden)

Using Language Inference to Verify Omega-regular Properties
Abhay Vardhan, Koushik Sen, Mahesh Viswanathan and Gul Agha (Univ. of Illinois, Urbana-Champaign, USA)

On-the-fly Reachability and Cycle Detection for Recursive State Machines Rajeev Alur, Swarat Chaudhuri (Univ. of Pennsylvania, Philadelphia, USA), Kousha Etessami (Univ. of Edinburgh, UK) and P. Madhusudan (Univ. of Pennsylvania, Philadelphia, USA)

Empirically Efficient Verification for a Class of Infinite-State Systems
Jesse Bingham and Alan J. Hu (Univ. of British Columbia, Vancouver, Canada)

Context-Bounded Model Checking of Concurrent Software
Shaz Qadeer and Jakob Rehof (Microsoft Research, Redmond, USA)

A Generic Theorem Prover of CSP Refinement
Yoshinao Isobe (AIST, Tsukuba, Japan) and Markus Roggenbach (Univ. of Wales, Swansea, UK)

Separating Fairness and Well-Foundedness for the Analysis of Fair Discrete Systems
Amir Pnueli (NYU, USA), Andreas Podelski and Andrey Rybalchenko (MPI, Saarbrücken, Germany)

An Abstract Interpretation-based Refinement Algorithm for Strong Preservation
Francesco Ranzato and Francesco Tapparo (Univ. of Padova, Italy)

Guarded Types for Program Understanding
Raghavan Komondoor (IBM T.J. Watson Research Center, Yorktown Heights, USA), G. Ramalingam (IBM India, Bangalore, India), Satish Chandra (IBM India Research Lab, New Delhi, India) and John Field (IBM T.J. Watson Research Center, Yorktown Heights, USA)

jMoped: A Java Bytecode Checker Based on Moped
Dejvuth Suwimonteerabuth, Stefan Schwoon and Javier Esparza (Univ. of Stuttgart, Germany)

Java-MOP: A Monitoring Oriented Programming Environment for Java
Feng Chen and Grigore Rosu (Univ. of Illinois, Urbana-Champaign, USA)

JML-Testing-Tools: A Symbolic Animator for JML Specifications using CLP
Frederic Dadeau, Fabrice Bouquet, Bruno Legeard and Mark Utting (LIFC, CNRS-INRIA, Besançon, France)

jETI: A Tool for Remote Tool Integration
Ralf Nagel, Tiziana Margaria (Univ. of Göttingen, Germany) and Bernhard Steffen (Univ. of Dortmund, Germany)

A Note on On-The-Fly Verification Algorithms
Stefan Schwoon and Javier Esparza (Univ. of Stuttgart, Germany)

Truly On-The-Fly LTL Model Checking
Stephan Merz, Moritz Hammer and Alexander Knapp (Ludwig-Maximilans Univ., Munich, Germany)

Complementation Constructions for Nondeterministic Automata on Infinite Words
Orna Kupferman (Hebrew Univ., Jerusalem, Israel) and Moshe Y. Vardi (Rice Univ., Houston, USA)

Using BDDs to Decide CTL
Will Marrero (DePaul Univ., Chicago, USA)

Model-checking Infinite-state Markov Chains
Anne Remke, Boudewijn Haverkort and Lucia Cloth (Univ. of Twente, Enschede, The Netherlands)

Algorithmic Verification of Recursive Probabilistic Systems
Kousha Etessami (Univ. of Edinburgh, UK) and Mihalis Yannakakis (Columbia Univ., New York, USA)

Monte Carlo Model Checking
Radu Grosu and Scott Smolka (State Univ. of New York, Stony Brook, USA)

Model Checking for Nominal Calculi
Ugo Montanari, Univ. Pisa, Italy

Esterel v7: From Verified Formal Specification to Efficient Industrial Designs
Gérard Berry, Esterel Technologies, Villeneuve-Loubet, France

Efficient Conflict Analysis for Finding All Satisfying Assignments of a Boolean Circuit
HoonSang Jin, HyoJung Han and Fabio Somenzi (Univ. of Colorado, Boulder, USA)

Bounded Validity Checking of Interval Duration Logic
Babita Sharma (IIT Bombay, India), Paritosh Pandya (Tata Institute, Mumbai, India) and Supratik Chakraborty (IIT Bombay, India)

An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic
Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti (ITC-IRST, Trento, Italy), Tommi Junttila (Helsinki Univ.of Technology, Finland), Peter van Rossum (ITC-IRST, Trento, Italy), Stephan Schulz (Univ. of Verona, Italy) and Roberto Sebastiani (Univ. of Trento, Italy)

A two-tier Technique for Supporting Quantifiers in a Lazily Proof-explicating Theorem Prover
Rustan Leino, Madan Musuvathi (Microsoft Research, Redmond, USA) and Xinming Ou (Princeton Univ., USA)

Applications of Craig Interpolation in Model Checking
Ken McMillan, Cadence Berkeley Labs, USA

Symbolic Test Selection Based on Approximate Analysis
Bertrand Jeannet, Thierry Jéron, Vlad Rusu and Elena Zinovieva (IRISA, Rennes, France)

Symstra: A Framework for Generating Object-oriented Unit Tests using Symbolic Execution
Tao Xie (Univ. of Washington, Seattle, USA), Darko Marinov (MIT, Cambridge, USA), Wolfram Schulte (Microsoft Research, Redmond, USA) and David Notkin (Univ. of Washington, Seattle, USA)

Dynamic Symmetry Reduction
E. Allen Emerson and Thomas Wahl (Univ. of Texas, Austin, USA)

Localization and Register Sharing for Predicate Abstraction
Franjo Ivancic, Himanshu Jain, Aarti Gupta and Malay K. Ganai (NEC Labs, Princeton, USA)

On Some Transformation Invariants under Retiming and Resynthesis
Jie-Hong Jiang (Univ. of California, Berkeley, USA)

Compositional Message Sequence Charts (CMSCs) are better to Implement than MSCs
Blaise Genest (Univ. Paris VII, France and Warwick Univ., UK)

Temporal Logic for Scenario-Based Specifications
Hillel Kugler (NYU, USA), David Harel (Weizmann Institute, Rehovot, Israel), Amir Pnueli (NYU, USA), Yuan Lu (Broadcom, San Jose, USA) and Yves Bontemps (Univ. of Namur, Belgium)

Mining Temporal Specifications for Error Detection
Westley Weimer and George C. Necula (Univ. of California, Berkeley, USA)

A New Algorithm for Strategy Synthesis in LTL Games
Aidan Harding, Mark Ryan (Univ. of Birmingham, UK) and Pierre-Yves Schobbens (Univ. of Namur, Belgium)

FocusCheck: A Tool for Model Checking and Debugging Sequential C Programs
Curtis W. Keller (Iowa State Univ., Ames, USA), Diptikalyan Saha (State Univ. of New York, Stony Brook, USA), Samik Basu (Iowa State Univ., Ames, USA) and Scott A. Smolka (State Univ. of New York, Stony Brook, USA)

SATABS: SAT-based Predicate Abstraction for ANSI-C
Edmund Clarke (Carnegie Mellon Univ., Pittsburgh, USA), Daniel Kroening (ETH Zürich, Switzerland), Natasha Sharygina and Karen Yorav (Carnegie Mellon Univ., Pittsburgh, USA)

DiVer: SAT-based Model Checking Platform for Verifying Large Scale Systems
Malay Ganai, Gupta Aarti and Ashar Pranav (NEC Labs, Princeton, USA)

BISIMULATOR: A Modular Tool for On-the-Fly Equivalence Checking
Damien Bergamini, Nicolas Descoubes, Christophe Joubert and Radu Mateescu (INRIA Rhône-Alpes, Saint Ismier, France)

Shortest Counterexamples for Symbolic Model Checking of LTL with Past
Viktor Schuppan (ETH Zürich, Switzerland) and Armin Biere (Johannes Kepler Univ., Linz, Austria)

Snapshot Verification
Blaise Genest (Univ. of Warwick, UK), Dietrich Kuske (TU Dresden, Germany), Anca Muscholl (Univ. Paris VII, France) and Doron Peled (Univ. of Warwick, UK)

Time-efficient Model Checking with Magnetic Disk
Tonglaga Bao and Michael Jones (Brigham Young Univ., Provo, USA)