Abstract is missing.
- Abstraction by Symbolic Indexing TransformationsThomas F. Melham, Robert B. Jones. 1-18 [doi]
- Counter-Example Based Predicate Discovery in Predicate AbstractionSatyaki Das, David L. Dill. 19-32 [doi]
- Automated Abstraction Refinement for Model Checking Large State Spaces Using SAT Based Conflict AnalysisPankaj Chauhan, Edmund M. Clarke, James H. Kukula, Samir Sapra, Helmut Veith, Dong Wang. 33-51 [doi]
- Simplifying Circuits for Formal Verification Using Parametric RepresentationIn-Ho Moon, Hee-Hwan Kwak, James H. Kukula, Thomas R. Shiple, Carl Pixley. 52-69 [doi]
- Generalized Symbolic Trajectory Evaluation - Abstraction in ActionJin Yang, Carl-Johan H. Seger. 70-87 [doi]
- Analysis of Symbolic SCC Hull AlgorithmsFabio Somenzi, Kavita Ravi, Roderick Bloem. 88-105 [doi]
- Sharp Disjunctive Decomposition for Language Emptiness CheckingChao Wang, Gary D. Hachtel. 106-122 [doi]
- Relating Multi-step and Single-Step Microprocessor Correctness StatementsMark Aagaard, Nancy A. Day, Meng Lou. 123-141 [doi]
- Modeling and Verification of Out-of-Order Microprocessors in UCLIDShuvendu K. Lahiri, Sanjit A. Seshia, Randal E. Bryant. 142-159 [doi]
- On Solving Presburger and Linear Arithmetic with SATOfer Strichman. 160-170 [doi]
- Deciding Presburger Arithmetic by Model Checking and Comparisons with Other MethodsVijay Ganesh, Sergey Berezin, David L. Dill. 171-186 [doi]
- QUBOS: Deciding Quantified Boolean Logic Using Propositional Satisfiability SolversAbdelwaheb Ayari, David A. Basin. 187-201 [doi]
- Exploiting Transition Locality in the Disk Based Mur phi VerifierGiuseppe Della Penna, Benedetto Intrigila, Enrico Tronci, Marisa Venturini Zilli. 202-219 [doi]
- Traversal Techniques for Concurrent SystemsMarc Solé, Enric Pastor. 220-237 [doi]
- A Fixpoint Based Encoding for Bounded Model CheckingAlan M. Frisch, Daniel Sheridan, Toby Walsh. 238-255 [doi]
- Using Edge-Valued Decision Diagrams for Symbolic Generation of Shortest PathsGianfranco Ciardo, Radu Siminiceanu. 256-273 [doi]
- Mechanical Verification of a Square Root Algorithm Using Taylor s TheoremJun Sawada, Ruben Gamboa. 274-291 [doi]
- A Specification and Verification Framework for Developing Weak Shared Memory Consistency ProtocolsProsenjit Chatterjee, Ganesh Gopalakrishnan. 292-309 [doi]
- Model Checking the Design of an Unrestricted, Stuck-at Fault Tolerant, Asynchronous Sequential Circuit Using SMVMeine van der Meulen. 310-323 [doi]
- Functional Design Using Behavioural and Structural ComponentsRichard Sharp. 324-341 [doi]
- Compiling Hardware Descriptions with Relative Placement Information for Parametrised LibrariesSteve McKeever, Wayne Luk, Arran Derbyshire. 342-359 [doi]
- Input/Output Compatibility of Reactive SystemsJosep Carmona, Jordi Cortadella. 360-377 [doi]
- Smart Play-out of Behavioral RequirementsDavid Harel, Hillel Kugler, Rami Marelly, Amir Pnueli. 378-398 [doi]