| Contents |
Interpolation and SAT-Based Model Checking / K.L. McMillan -- Bounded Model Checking and Induction: From Refutation to Verification / Leonardo de Moura, Harald Ruess and Maria Sorea -- Reasoning with Temporal Logic on Truncated Paths / Cindy Eisner, Dana Fisman, John Havlicek, Yoad Lustig, Anthony McIsaac and David Van Campenhout -- Structural Symbolic CTL Model Checking of Asynchronous Systems / Gianfranco Ciardo and Radu Siminiceanu -- A Work-Efficient Distributed Algorithm for Reachability Analysis / Orna Grumberg, Tamir Heyman and Assaf Schuster -- Modular Strategies for Infinite Games on Recursive Graphs / Rajeev Alur, Salvatore La Torre and P. Madhusudan -- Fast Mu-Calculus Model Checking when Tree-Width Is Bounded / Jan Obdrzalek -- Dense Counter Machines and Verification Problems / Gaoyan Xie, Zhe Dang, Oscar H. lbarra and Pierluigi San Pietro -- TRIM: A Tool for Triggered Message Sequence Charts / Bikram Sengupta and Rance Cleaveland -- Model Checking Multi-Agent Programs with CASP / Rafael H. Bordini, Michael Fisher, Carmen Pardavila, Willem Visser and Michael Wooldridge -- Monitoring Temporal Rules Combined with Time Series / Doron Drusinsky -- FAST: Fast Acceleration of Symbolic Transition Systems / Sebastien Bardin, Alain Finkel, Jerome Leroux and Laure Petrucci -- Rabbit: A Tool for BDD-Based Verification of Real-Time Systems / Dirk Beyer, Claus Lawerentz and Andreas Noack -- Making Predicate Abstraction Efficient: How to Eliminate Redundant Predicates / Edmund Clarke, Orna Grumberg, Muralidhar Talupur and Dong Wang -- A Symbolic Approach to Predicate Abstraction / Shuvendu K. Lahiri, Randel E. Bryant and Byron Cook -- Unbounded, Fully Symbolic Model Checking of Timed Automata Using Boolean Methods / Sanjit A. Seshia and Randal E. Bryant -- Digitizing Interval Duration Logic / Gaurav Chakravorty and Pritosh K. Pandya -- Timed Control with Partial Observability / Patricia Bouyer, Deepak D'Souza, P. Modhusudan and Antoine Petit -- Hybrid Acceleration Using Real Vector Automata / Bernard Boigelot, Frederic Herbreteau and Sebastien Jodogne -- Abstraction and BDDs Complement SAT-Based BMC in Di Ver / Aarti Gupta, Malay Ganai, Chao Wang, Zijiang Yang and Pranav Ashar -- TLQSolver: A Temporal Logic Query Checker / Marsha Chechik and Arie Gurfinkel -- Evidence Explorer: A Tool for Exploring Model-Checking Proofs / Yifei Dong, C.R. Ramakrishnan and Scott A. Smolka -- HERMES: An Automatic Tool for Verification of Secrecy in Security Protocols / Liana Bozga, Yassine Lakhnech and Michael Perin -- lterating Transducers in the Large / Bernard Boigelot, Axel Legay and Pierre Wolper -- Algorithmic Improvements in Regular Model Checking / Parosh Aziz Abdulla, Bengt Jonsson, Marcus Nilsson and Julien d'Orso -- Efficient Image Computation in Infinite State Model Checking / Constantinos Bartzis and Teufik Bultan -- Thread-Modular Abstraction Refinement / Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar and Shaz Qadeer -- A Game-Based Framework for CTL Counterexamples and 3-Valued Abstraction-Refinement / Sharon Shoham and Orna Grumberg -- Abstraction for Branching Time Properties / Kedar S. Namjoshi -- Certifying Optimality of State Estimation Programs / Grigore Rosu, Ram Prasad Venkatesan, Jon Whittle and Laurentiu Leustean -- Domain-Specific Optimization in Automata Learning / Hardi Hungar, Oliver Niese and Bernhard Steffen -- Model Checking Conformance with Scenario-Based Specifications / Marcelo Glusman and Shmuel Katz -- Deductive Verification of Advanced Out-of-Order Microprocessors / Shuvendu K. Lahiri and Randal E. Bryant -- Theorem Proving Using Lazy Proof Explication / Cormac Flanagan, Rajeev Joshi, Xinming Ou and James B. Saxe -- Enhanced Vacuity Detection in Linear Temporal Logic / Roy Armoni, Limor Fix, Alon Flaisher, Orna Grumberg, Nir Piterman, Andreas Tiemeyer and Moshe Y. Vardi -- Bridging the Gap between Fair Simulation and Trace Inclusion / Yonit Kesten, Nir Piterman and Amir Pnueli -- An Improved On-the-Fly Tableau Construction for a Real-Time Temporal Logic / Marc Geilen -- Strengthening Invariants by Symbolic Consistency Testing / Husam Abu-Haimed, Sergey Berezin and David L. Dill -- Linear Invariant Generation Using Non-Linear Constraint Solving / Michael A. Colon, Sriram Sankaranarayanan and Henny B. Sipma -- To Store or Not to Store / Gerd Behrmann, Kim G. Larsen and Rudek Pelanek -- Calculating [toe]-Confluence Compositionally / Gordon J. Pace, Frederic Lang and Rada Mateescu. |
