CAV 2008
53 papers
- A Hybrid Type System for Lock-Freedom of Mobile Processes
- A Numerical Abstract Domain Based on Expression Abstraction and Max Operator with Application in Timing Analysis
- A Practical Approach to Word Level Model Checking of Industrial Netlists
- Abstract Interpretation with Applications to Timing Validation
- An Algebraic Approach for Proving Data Correctness in Arithmetic Data Paths
- Application of Formal Word-Level Analysis to Constrained Random Simulation
- Applying the Graph Minor Theorem to the Verification of Graph Transformation Systems
- Assertion-Based Verification: Industry Myths to Realities (Invited Tutorial)
- AutoMOTGen: Automatic Model Oriented Test Generator for Embedded Control Systems
- Automated Assume-Guarantee Reasoning by Abstraction Refinement
- CSIsat: Interpolation for LA+EUF
- Computing Differential Invariants of Hybrid Systems as Fixedpoints
- Conflict-Tolerant Features
- Constraint-Based Approach for Analysis of Hybrid Systems
- Coping with Outside-the-Box Attacks
- Correcting a Space-Efficient Simulation Algorithm
- Discriminative Model Checking
- Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings
- Effective Program Verification for Relaxed Memory Models
- Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations
- Enhancing Program Verification with Lemmas
- FShell: Systematic Test Case Generation for Dynamic Analysis and Measurement
- Faster Than Uppaal?
- Functional Verification of Power Gated Designs by Compositional Reasoning
- Heap Assumptions on Demand
- Implied Set Closure and Its Application to Memory Consistency Verification
- Inferring Congruence Equations Using SAT
- Jakstab: A Static Analysis Platform for Binaries
- Linear Arithmetic with Stars
- Local Proofs for Linear-Time Properties of Concurrent Programs
- Mechanical Verification of Transactional Memories with Non-transactional Memory Accesses
- Monitoring Atomicity in Concurrent Programs
- Monotonic Abstraction for Programs with Dynamic Memory Heaps
- Probabilistic CEGAR
- Producing Short Counterexamples Using "Crucial Events"
- Prover's Palette: A User-Centric Approach to Verification with Isabelle and QEPCAD-B
- Proving Conditional Termination
- QMC: A Model Checker for Quantum Systems
- Ranking Automata and Games for Prioritized Requirements
- Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis
- Scalable Shape Analysis for Systems Code
- Semi-external LTL Model Checking
- Singularity: Designing Better Software (Invited Talk)
- T(O)RMC: A Tool for (omega)-Regular Model Checking
- THOR: A Tool for Reasoning about Shape and Arithmetic
- The Barcelogic SMT Solver
- The CASPA Tool: Causality-Based Abstraction for Security Protocol Analysis
- The MathSAT 4SMT Solver
- The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols
- Theorem Proving for Verification (Invited Tutorial)
- Thread Quantification for Concurrent Shape Analysis
- Tutorial on Separation Logic (Invited Tutorial)
- Validating High-Level Synthesis