Front matter
1-18
Abstraction by Symbolic Indexing Transformations
Thomas F. Melham and Robert B. Jones
19-32
Counter-Example Based Predicate Discovery in Predicate Abstraction
Satyaki Das and David L. Dill
33-51
Automated Abstraction Refinement for Model Checking Large State Spaces Using SAT Based Conflict Analysis
Pankaj Chauhan, Edmund Clarke, James Kukula, Samir Sapra and Helmut Veith, et al.
52-69
Simplifying Circuits for Formal Verification Using Parametric Representation
In-Ho Moon, Hee Hwan Kwak, James Kukula, Thomas Shiple and Carl Pixley
70-87
Generalized Symbolic Trajectory Evaluation — Abstraction in Action
Jin Yang and Carl-Johan H. Seger
88-105
Analysis of Symbolic SCC Hull Algorithms
Fabio Somenzi, Kavita Ravi and Roderick Bloem
106-122
Sharp Disjunctive Decomposition for Language Emptiness Checking
Chao Wang and Gary D. Hachtel
123-141
Relating Multi-step and Single-Step Microprocessor Correctness Statements
Mark D. Aagaard, Nancy A. Day and Meng Lou
142-159
Modeling and Verification of Out-of-Order Microprocessors in UCLID
Shuvendu K. Lahiri, Sanjit A. Seshia and Randal E. Bryant
160-170
On Solving Presburger and Linear Arithmetic with SAT
Ofer Strichman
171-186
Deciding Presburger Arithmetic by Model Checking and Comparisons with Other Methods
Vijay Ganesh, Sergey Berezin and David L. Dill
187-201
Qubos
: Deciding Quantified Boolean Logic Using Propositional Satisfiability Solvers
Abdelwaheb Ayari and David Basin
202-219
Exploiting Transition Locality in the Disk Based Murϕ Verifier
Giuseppe Della Penna, Benedetto Intrigila, Enrico Tronci and Marisa Venturini Zilli
220-237
Traversal Techniques for Concurrent Systems
Marc Solé and Enric Pastor
238-255
A Fixpoint Based Encoding for Bounded Model Checking
Alan Frisch, Daniel Sheridan and Toby Walsh
256-273
Using Edge-Valued Decision Diagrams for Symbolic Generation of Shortest Paths
Gianfranco Ciardo and Radu Siminiceanu
274-291
Mechanical Verification of a Square Root Algorithm Using Taylor’s Theorem
Jun Sawada and Ruben Gamboa
292-309
A Specification and Verification Framework for Developing Weak Shared Memory Consistency Protocols
Prosenjit Chatterjee and Ganesh Gopalakrishnan
310-323
Model Checking the Design of an Unrestricted, Stuck-at Fault Tolerant, Asynchronous Sequential Circuit Using SMV
Meine van der Meulen
324-341
Functional Design Using Behavioural and Structural Components
Richard Sharp
342-359
Compiling Hardware Descriptions with Relative Placement Information for Parametrised Libraries
Steve McKeever, Wayne Luk and Arran Derbyshire
360-377
Input/Output Compatibility of Reactive Systems
Josep Carmona and Jordi Cortadella
378-398
Smart Play-out of Behavioral Requirements
David Harel, Hillel Kugler, Rami Marelly and Amir Pnueli
Back matter