default search action
4th FMCAD 2002: Portland, Oregon, USA
- Mark D. Aagaard, John W. O'Leary:
Formal Methods in Computer-Aided Design, 4th International Conference, FMCAD 2002, Portland, OR, USA, November 6-8, 2002, Proceedings. Lecture Notes in Computer Science 2517, Springer 2002, ISBN 3-540-00116-6
Abstraction
- Thomas F. Melham, Robert B. Jones:
Abstraction by Symbolic Indexing Transformations. 1-18 - Satyaki Das, David L. Dill:
Counter-Example Based Predicate Discovery in Predicate Abstraction. 19-32 - 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
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 - Jin Yang, Carl-Johan H. Seger:
Generalized Symbolic Trajectory Evaluation - Abstraction in Action. 70-87
Model Checking: Strongly-Connected Components
- Fabio Somenzi, Kavita Ravi, Roderick Bloem:
Analysis of Symbolic SCC Hull Algorithms. 88-105 - Chao Wang, Gary D. Hachtel:
Sharp Disjunctive Decomposition for Language Emptiness Checking. 106-122
Microprocessor Specification and Verification
- Mark D. Aagaard, Nancy A. Day, Meng Lou:
Relating Multi-step and Single-Step Microprocessor Correctness Statements. 123-141 - Shuvendu K. Lahiri, Sanjit A. Seshia, Randal E. Bryant:
Modeling and Verification of Out-of-Order Microprocessors in UCLID. 142-159
Decision Procedures
- Ofer Strichman:
On Solving Presburger and Linear Arithmetic with SAT. 160-170 - Vijay Ganesh, Sergey Berezin, David L. Dill:
Deciding Presburger Arithmetic by Model Checking and Comparisons with Other Methods. 171-186 - Abdelwaheb Ayari, David A. Basin:
QUBOS: Deciding Quantified Boolean Logic Using Propositional Satisfiability Solvers. 187-201
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 - Marc Solé, Enric Pastor:
Traversal Techniques for Concurrent Systems. 220-237
Model Checking: Fixed Points
- Alan M. Frisch, Daniel Sheridan, Toby Walsh:
A Fixpoint Based Encoding for Bounded Model Checking. 238-255 - Gianfranco Ciardo, Radu Siminiceanu:
Using Edge-Valued Decision Diagrams for Symbolic Generation of Shortest Paths. 256-273
Verification Techniques and Methodology
- Jun Sawada, Ruben Gamboa:
Mechanical Verification of a Square Root Algorithm Using Taylor's Theorem. 274-291 - Prosenjit Chatterjee, Ganesh Gopalakrishnan:
A Specification and Verification Framework for Developing Weak Shared Memory Consistency Protocols. 292-309 - Meine van der Meulen:
Model Checking the Design of an Unrestricted, Stuck-at Fault Tolerant, Asynchronous Sequential Circuit Using SMV. 310-323
Hardware Description Languages
- Richard Sharp:
Functional Design Using Behavioural and Structural Components. 324-341 - Steve McKeever, Wayne Luk, Arran Derbyshire:
Compiling Hardware Descriptions with Relative Placement Information for Parametrised Libraries. 342-359
Prototyping and Synthesis
- Josep Carmona, Jordi Cortadella:
Input/Output Compatibility of Reactive Systems. 360-377 - David Harel, Hillel Kugler, Rami Marelly, Amir Pnueli:
Smart Play-out of Behavioral Requirements. 378-398
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.