4. FMCAD 2002: Portland, Oregon, USA

@proceedings{DBLP:conf/fmcad/2002,
  editor    = {Mark Aagaard and
               John W. O'Leary},
  title     = {Formal Methods in Computer-Aided Design, 4th International Conference,
               FMCAD 2002, Portland, OR, USA, November 6-8, 2002, Proceedings},
  booktitle = {FMCAD},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {2517},
  year      = {2002},
  isbn      = {3-540-00116-6},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

Abstraction

• Thomas F. Melham, Robert B. Jones:
  Abstraction by Symbolic Indexing Transformations. 1-18
  Electronic Edition (Springer LINK) BibTeX
• Satyaki Das, David L. Dill:
  Counter-Example Based Predicate Discovery in Predicate Abstraction. 19-32
  Electronic Edition (Springer LINK) BibTeX
• Pankaj Chauhan, Edmund M. Clarke, James H. Kukula, Samir Sapra, Helmut Veith, Dong Wang:
  Automated Abstraction Refinement for Model Checking Large State Spaces Using SAT Based Conflict Analysis. 33-51
  Electronic Edition (Springer LINK) BibTeX

Symbolic Simulation

• In-Ho Moon, Hee-Hwan Kwak, James H. Kukula, Thomas R. Shiple, Carl Pixley:
  Simplifying Circuits for Formal Verification Using Parametric Representation. 52-69
  Electronic Edition (Springer LINK) BibTeX
• Jin Yang, Carl-Johan H. Seger:
  Generalized Symbolic Trajectory Evaluation - Abstraction in Action. 70-87
  Electronic Edition (Springer LINK) BibTeX

Model Checking: Strongly-Connected Components

• Fabio Somenzi, Kavita Ravi, Roderick Bloem:
  Analysis of Symbolic SCC Hull Algorithms. 88-105
  Electronic Edition (Springer LINK) BibTeX
• Chao Wang, Gary D. Hachtel:
  Sharp Disjunctive Decomposition for Language Emptiness Checking. 106-122
  Electronic Edition (Springer LINK) BibTeX

Microprocessor Specification and Verification

• Mark Aagaard, Nancy A. Day, Meng Lou:
  Relating Multi-step and Single-Step Microprocessor Correctness Statements. 123-141
  Electronic Edition (Springer LINK) BibTeX
• Shuvendu K. Lahiri, Sanjit A. Seshia, Randal E. Bryant:
  Modeling and Verification of Out-of-Order Microprocessors in UCLID. 142-159
  Electronic Edition (Springer LINK) BibTeX

Decision Procedures

• Ofer Strichman:
  On Solving Presburger and Linear Arithmetic with SAT. 160-170
  Electronic Edition (Springer LINK) BibTeX
• Vijay Ganesh, Sergey Berezin, David L. Dill:
  Deciding Presburger Arithmetic by Model Checking and Comparisons with Other Methods. 171-186
  Electronic Edition (Springer LINK) BibTeX
• Abdelwaheb Ayari, David A. Basin:
  QUBOS: Deciding Quantified Boolean Logic Using Propositional Satisfiability Solvers. 187-201
  Electronic Edition (Springer LINK) BibTeX

Model Checking: Reachability Analysis

• Giuseppe Della Penna, Benedetto Intrigila, Enrico Tronci, Marisa Venturini Zilli:
  Exploiting Transition Locality in the Disk Based Mur phi Verifier. 202-219
  Electronic Edition (Springer LINK) BibTeX
• Marc Solé, Enric Pastor:
  Traversal Techniques for Concurrent Systems. 220-237
  Electronic Edition (Springer LINK) BibTeX

Model Checking: Fixed Points

• Alan M. Frisch, Daniel Sheridan, Toby Walsh:
  A Fixpoint Based Encoding for Bounded Model Checking. 238-255
  Electronic Edition (Springer LINK) BibTeX
• Gianfranco Ciardo, Radu Siminiceanu:
  Using Edge-Valued Decision Diagrams for Symbolic Generation of Shortest Paths. 256-273
  Electronic Edition (Springer LINK) BibTeX

Verification Techniques and Methodology

• Jun Sawada, Ruben Gamboa:
  Mechanical Verification of a Square Root Algorithm Using Taylor's Theorem. 274-291
  Electronic Edition (Springer LINK) BibTeX
• Prosenjit Chatterjee, Ganesh Gopalakrishnan:
  A Specification and Verification Framework for Developing Weak Shared Memory Consistency Protocols. 292-309
  Electronic Edition (Springer LINK) BibTeX
• Meine van der Meulen:
  Model Checking the Design of an Unrestricted, Stuck-at Fault Tolerant, Asynchronous Sequential Circuit Using SMV. 310-323
  Electronic Edition (Springer LINK) BibTeX

Hardware Description Languages

• Richard Sharp:
  Functional Design Using Behavioural and Structural Components. 324-341
  Electronic Edition (Springer LINK) BibTeX
• Steve McKeever, Wayne Luk, Arran Derbyshire:
  Compiling Hardware Descriptions with Relative Placement Information for Parametrised Libraries. 342-359
  Electronic Edition (Springer LINK) BibTeX

Prototyping and Synthesis

• Josep Carmona, Jordi Cortadella:
  Input/Output Compatibility of Reactive Systems. 360-377
  Electronic Edition (Springer LINK) BibTeX
• David Harel, Hillel Kugler, Rami Marelly, Amir Pnueli:
  Smart Play-out of Behavioral Requirements. 378-398
  Electronic Edition (Springer LINK) BibTeX