20. CAV 2008:
Princeton,
NJ,
USA
Aarti Gupta, Sharad Malik (Eds.):
Computer Aided Verification, 20th International Conference, CAV 2008, Princeton, NJ, USA, July 7-14, 2008, Proceedings.
Lecture Notes in Computer Science 5123 Springer 2008, ISBN 978-3-540-70543-7 BibTeX
Invited Talks
Invited Tutorials
Concurrency
Memory Consistency
Abstraction/Refinement
Hybrid Systems
Tools - Dynamic Verification
Modeling and Specification Formalisms
Decision Procedures
Tools - Decision Procedures
- Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio:
The Barcelogic SMT Solver.
294-298
Electronic Edition (link) BibTeX
- Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani:
The MathSAT 4SMT Solver.
299-303
Electronic Edition (link) BibTeX
- Dirk Beyer, Damien Zufferey, Rupak Majumdar:
CSIsat: Interpolation for LA+EUF.
304-308
Electronic Edition (link) BibTeX
- Laura I. Meikle, Jacques D. Fleuriot:
Prover's Palette: A User-Centric Approach to Verification with Isabelle and QEPCAD-B.
309-313
Electronic Edition (link) BibTeX
Program Verification
- Andreas Podelski, Andrey Rybalchenko, Thomas Wies:
Heap Assumptions on Demand.
314-327
Electronic Edition (link) BibTeX
- Byron Cook, Sumit Gulwani, Tal Lev-Ami, Andrey Rybalchenko, Mooly Sagiv:
Proving Conditional Termination.
328-340
Electronic Edition (link) BibTeX
- Parosh Aziz Abdulla, Ahmed Bouajjani, Jonathan Cederberg, Frédéric Haziza, Ahmed Rezine:
Monotonic Abstraction for Programs with Dynamic Memory Heaps.
341-354
Electronic Edition (link) BibTeX
- Huu Hai Nguyen, Wei-Ngan Chin:
Enhancing Program Verification with Lemmas.
355-369
Electronic Edition (link) BibTeX
Program and Shape Analysis
- Bhargav S. Gulavani, Sumit Gulwani:
A Numerical Abstract Domain Based on Expression Abstraction and Max Operator with Application in Timing Analysis.
370-384
Electronic Edition (link) BibTeX
- Hongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn:
Scalable Shape Analysis for Systems Code.
385-398
Electronic Edition (link) BibTeX
- Josh Berdine, Tal Lev-Ami, Roman Manevich, G. Ramalingam, Shmuel Sagiv:
Thread Quantification for Concurrent Shape Analysis.
399-413
Electronic Edition (link) BibTeX
Tools - Security and Program Analysis
Hardware Verification I
Hardware Verification II
- Sudipta Kundu, Sorin Lerner, Rajesh Gupta:
Validating High-Level Synthesis.
459-472
Electronic Edition (link) BibTeX
- Oliver Wienand, Markus Wedler, Dominik Stoffel, Wolfgang Kunz, Gert-Martin Greuel:
An Algebraic Approach for Proving Data Correctness in Arithmetic Data Paths.
473-486
Electronic Edition (link) BibTeX
- Hyondeuk Kim, HoonSang Jin, Kavita Ravi, Petr Spacek, John Pierce, Robert P. Kurshan, Fabio Somenzi:
Application of Formal Word-Level Analysis to Constrained Random Simulation.
487-490
Electronic Edition (link) BibTeX
Model Checking
Space Efficient Algorithms
Tools - Model Checking
Copyright © Sat May 16 23:00:38 2009
by Michael Ley (ley@uni-trier.de)