CAV 1998
54 papers
- A Comparison of Presburger Engines for EFSM Reachability
- A Formal Method Experience at Secure Computing Corporation
- A General Approach to Partial Order Reductions in Symbolic Verification (Extended Abstract)
- A Machine-Checked Proof of the Optimality of a Real-Time Scheduling Policy
- A Role for Theorem Proving in Multi-Processor Design
- A Toolset for Message Sequence Charts
- An ACL2 Proof of Write Invalidate Cache Coherence
- An Experiment in Parallelizing an Application Using Formal Methods
- BDD Based Procedures for a Theory of Equality with Uninterpreted Functions
- Computing Abstractions of Infinite State Systems Compositionally and Automatically
- Computing Reachable Control States of Systems Modeled with Uninterpreted Functions and Infinite Memory
- Correctness of the Concurrent Approach to Symbolic Verification of Interleaved Models
- Decomposing the Proof of Correctness of pipelined Microprocessors
- Design Constraints in Symbolic Model Checking
- Efficient Symbolic Detection of Global Properties in Distributed Systems
- Finite-State Analysis of Security Protocols
- Formal Methods in an Industrial Environment
- Formal Verification of Out-of-Order Execution Using Incremental Flushing
- From Pre-historic to Post-modern Symbolic Model Checking
- Generating Finite-State Abstractions of Reactive Systems Using Decision Procedures
- InVeST: A Tool for the Verification of Invariants
- Integrating Proof-Based and Model-Checking Techniques for the Formal Verification of Cryptographic Protocols
- Kronos: A Model-Checking Tool for Real-Time Systems
- MOCHA: Modularity in Model Checking
- MONA 1.x: New Techniques for WS1S and WS2S
- Mechanising BAN Kerberos by the Inductive Method
- Model Checking LTL Using Net Unforldings
- Model Checking for a First-Order Temporal Logic Using Multiway Decision Graphs
- Multiple Counters Automata, Safety Analysis and Presburger Arithmetic
- Normed Simulations
- On Checking Model Checkers
- On the Limitations of Ordered Representations of Functions
- On-the-Fly Analysis of Systems with Unbounded, Lossy FIFO Channels
- On-the-Fly Model Checking of RCTL Formulas
- Optikron: A Tool Suite for Enhancing Model-Checking of Real-Time Systems
- Processor Verification with Precise Exeptions and Speculative Execution
- Protocol Verification in Nuprl
- Real-Time Verification of Statemate Designs
- SCR*: A Toolset for Specifying and Analyzing Software Requirements
- Structural Symmetry and Model Checking
- Symmetry Reductions in Model Checking
- Synchronous Programming of Reactive Systems
- Ten Years of Partial Order Reduction
- The 'Test Model-Checking' Approach to the Verification of Formal Memory Models of Multiprocessors
- Transforming the Theorem Prover into a Digital Design Tool: From Concept Car to Off-Road Vehicle
- Using Magnatic Disk Instead of Main Memory in the Murphi Verifier
- Verification of Floating-Point Adders
- Verification of Parameterized Bus Arbitration Protocol
- Verification of Timed Systems Using POSETs
- Verification of an Implementation of Tomasulo's Algorithm by Compositional Model Checking
- Verifying Mobile Processes in the HAL Environment
- Verifying Systems with Infinite but Regular State Spaces
- XEVE, an ESTEREL Verification Environment
- You Assume, We Guarantee: Methodology and Case Studies