Abstract is missing.
- Esterel and Jazz: Two Synchronous Languages for Circuit Design (Abstract)Gérard Berry. 1 [doi]
- Design Process of Embedded Automotive Systems - Using Model Checking for Correct SpecificationPeter Jansen. 2-7 [doi]
- A Proof of Correctness of a Processor Implementing Tomasulo s Algorithm without a Reorder BufferRavi Hosabettu, Ganesh Gopalakrishnan, Mandayam K. Srivas. 8-22 [doi]
- Formal Verification of Explicitly Parallel MicroprocessorsByron Cook, John Launchbury, John Matthews, Richard B. Kieburtz. 23-36 [doi]
- Superscalar Processor Verification Using Efficient Reductions of the Logic of Equality with Uninterpreted Functions to Propositional LogicMiroslav N. Velev, Randal E. Bryant. 37-53 [doi]
- Model Checking TLA:::+::: SpecificationsYuan Yu, Panagiotis Manolios, Leslie Lamport. 54-66 [doi]
- Efficient Decompositional Model Checking for Regular Timing DiagramsNina Amla, E. Allen Emerson, Kedar S. Namjoshi. 67-81 [doi]
- Vacuity Detection in Temporal Model CheckingOrna Kupferman, Moshe Y. Vardi. 82-96 [doi]
- Using Symbolic Model Checking to Verify the Railway Stations of Hoorn-Kersenboogerd and HeerhugowaardCindy Eisner. 97-109 [doi]
- Practical Application of Formal Verification Techniques on a Frame Mux/Demux Chip from Nortel SemiconductorsYing Xu, Eduard Cerny, Allan Silburt, A. Coady, Ying Liu, Philip Pownall. 110-124 [doi]
- Efficient Verification of Timed Automata Using Dense and Discrete Time SemanticsMarius Bozga, Oded Maler, Stavros Tripakis. 125-141 [doi]
- From Asymmetry to Full Symmetry: New Techniques for Symmetry Reduction in Model CheckingE. Allen Emerson, Richard J. Trefler. 142-156 [doi]
- Automatic Error Correction of Large Circuits Using Boolean Decomposition and AbstractionDirk W. Hoffmann, Thomas Kropf. 157-171 [doi]
- Abstract BDDs: A Technque for Using Abstraction in Model CheckingEdmund M. Clarke, Somesh Jha, Yuan Lu, Dong Wang. 172-186 [doi]
- Formal Synthesis at the Algorithmic LevelChristian Blumenröhr, Viktor K. Sabelfeld. 187-201 [doi]
- Xs are for Trajectory Evaluation, Booleans are for Theorem ProvingMark Aagaard, Thomas F. Melham, John W. O Leary. 202-218 [doi]
- Verification of Infinite State Systems by Compositional Model CheckingKenneth L. McMillan. 219-234 [doi]
- Formal Verification of Designs with Complex Control by Symbolic SimulationGerd Ritter, Hans Eveking, Holger Hinrichsen. 234-249 [doi]
- Hints to accelerate Symbolic TraversalKavita Ravi, Fabio Somenzi. 250-264 [doi]
- Modleing and Checking Networks of Communicating Real-Time ProcessJürgen Ruf, Thomas Kropf. 265-279 [doi]
- Have I written enough Properties? - A Method of Comparison between Specification and ImplementationSagi Katz, Orna Grumberg, Daniel Geist. 280-297 [doi]
- Program Slicing of Hardware Description LanguagesEdmund M. Clarke, Masahiro Fujita, Sreeranga P. Rajan, Thomas W. Reps, Subash Shankar, Tim Teitelbaum. 298-312 [doi]
- Results of the Verification of a Complex Pipelined Machine ModelJun Sawada, Warren A. Hunt Jr.. 313-316 [doi]
- Hazard-Freedom Checking in Speed-Independent SystemsHüsnü Yenigün, Vladimir Levin, Doron Peled, Peter A. Beerel. 317-320 [doi]
- Yet another Look at the LTL Model CheckingKlaus Schneider. 321-325 [doi]
- Verification of Finite-State-Machine Refinements Using a Symbolic MethodologyStefan Hendricx, Luc J. M. Claesen. 326-329 [doi]
- Refinement and Property Checking in High-Level Synthesis using Attribute GrammarsGeorge Economakos, George K. Papakonstantinou. 330-333 [doi]
- A Systematic Incrementalization Technique and Its Application to Hardware DesignSteven D. Johnson, Yanhong A. Liu, Yuchen Zhang. 334-337 [doi]
- Bisimulation and Model CheckingKathi Fisler, Moshe Y. Vardi. 338-341 [doi]
- Circular Compositional Reasoning about LivenessKenneth L. McMillan. 342-345 [doi]
- Symbolic Simulation of Microprocessor Models using Type Classes in HaskellNancy A. Day, Jeffrey R. Lewis, Byron Cook. 346-349 [doi]
- Exploiting Retiming in a Guided Simulation Based Validation MethodologyAarti Gupta, Pranav Ashar, Sharad Malik. 350-353 [doi]
- Fault Models for Embedded Systems (Extended Abstract)Jens Chr. Godesken. 354-359 [doi]
- Validation of Object-Oriented Concurrent Designs by Model CheckingKlaus Schneider, Michaela Huhn, George Logothetis. 360-364 [doi]