default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID20th CAV 2008: Princeton, NJ, USA
- Aarti Gupta
, Sharad Malik:
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
Invited Talks
- James R. Larus:
Singularity: Designing Better Software (Invited Talk). 1-2 - Edward W. Felten:
Coping with Outside-the-Box Attacks. 3-4
Invited Tutorials
- Harry Foster:
Assertion-Based Verification: Industry Myths to Realities (Invited Tutorial). 5-10 - John Harrison:
Theorem Proving for Verification (Invited Tutorial). 11-18 - Peter W. O'Hearn:
Tutorial on Separation Logic (Invited Tutorial). 19-21 - Reinhard Wilhelm, Björn Wachter:
Abstract Interpretation with Applications to Timing Validation. 22-36
Concurrency
- Akash Lal, Thomas W. Reps:
Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis. 37-51 - Azadeh Farzan, P. Madhusudan:
Monitoring Atomicity in Concurrent Programs. 52-65 - Sarvani S. Vakkalanka, Ganesh Gopalakrishnan, Robert M. Kirby:
Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings. 66-79 - Naoki Kobayashi, Davide Sangiorgi:
A Hybrid Type System for Lock-Freedom of Mobile Processes. 80-93
Memory Consistency
- Surender Baswana, Shashank K. Mehta, Vishal Powar:
Implied Set Closure and Its Application to Memory Consistency Verification. 94-106 - Sebastian Burckhardt, Madanlal Musuvathi:
Effective Program Verification for Relaxed Memory Models. 107-120 - Ariel Cohen, Amir Pnueli, Lenore D. Zuck:
Mechanical Verification of Transactional Memories with Non-transactional Memory Accesses. 121-134
Abstraction/Refinement
- Mihaela Gheorghiu Bobaru, Corina S. Pasareanu, Dimitra Giannakopoulou:
Automated Assume-Guarantee Reasoning by Abstraction Refinement. 135-148 - Ariel Cohen, Kedar S. Namjoshi:
Local Proofs for Linear-Time Properties of Concurrent Programs. 149-161 - Holger Hermanns, Björn Wachter, Lijun Zhang:
Probabilistic CEGAR. 162-175
Hybrid Systems
- André Platzer, Edmund M. Clarke:
Computing Differential Invariants of Hybrid Systems as Fixedpoints. 176-189 - Sumit Gulwani, Ashish Tiwari:
Constraint-Based Approach for Analysis of Hybrid Systems. 190-203
Tools - Dynamic Verification
- Ambar A. Gadkari, Anand Yeolekar, J. Suresh, S. Ramesh, Swarup Mohalik, K. C. Shashidhar:
AutoMOTGen: Automatic Model Oriented Test Generator for Embedded Control Systems. 204-208 - Andreas Holzer, Christian Schallhart, Michael Tautschnig, Helmut Veith:
FShell: Systematic Test Case Generation for Dynamic Analysis and Measurement. 209-213
Modeling and Specification Formalisms
- Salil Joshi, Barbara König:
Applying the Graph Minor Theorem to the Verification of Graph Transformation Systems. 214-226 - Deepak D'Souza, Madhu Gopinathan:
Conflict-Tolerant Features. 227-239 - Rajeev Alur, Aditya Kanade, Gera Weiss:
Ranking Automata and Games for Prioritized Requirements. 240-253
Decision Procedures
- Himanshu Jain, Edmund M. Clarke, Orna Grumberg:
Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations. 254-267 - Ruzica Piskac, Viktor Kuncak:
Linear Arithmetic with Stars. 268-280 - Andy King, Harald Søndergaard:
Inferring Congruence Equations Using SAT. 281-293
Tools - Decision Procedures
- Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio:
The Barcelogic SMT Solver. 294-298 - Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani:
The MathSAT 4SMT Solver. 299-303 - Dirk Beyer, Damien Zufferey, Rupak Majumdar:
CSIsat: Interpolation for LA+EUF. 304-308 - Laura I. Meikle, Jacques D. Fleuriot:
Prover's Palette: A User-Centric Approach to Verification with Isabelle and QEPCAD-B. 309-313
Program Verification
- Andreas Podelski, Andrey Rybalchenko, Thomas Wies:
Heap Assumptions on Demand. 314-327 - Byron Cook, Sumit Gulwani, Tal Lev-Ami, Andrey Rybalchenko, Mooly Sagiv:
Proving Conditional Termination. 328-340 - Parosh Aziz Abdulla, Ahmed Bouajjani, Jonathan Cederberg, Frédéric Haziza, Ahmed Rezine:
Monotonic Abstraction for Programs with Dynamic Memory Heaps. 341-354 - Huu Hai Nguyen, Wei-Ngan Chin:
Enhancing Program Verification with Lemmas. 355-369
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 - Hongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn:
Scalable Shape Analysis for Systems Code. 385-398 - Josh Berdine, Tal Lev-Ami, Roman Manevich, G. Ramalingam, Shmuel Sagiv:
Thread Quantification for Concurrent Shape Analysis. 399-413
Tools - Security and Program Analysis
- Cas J. F. Cremers:
The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols. 414-418 - Michael Backes, Stefan Lorenz, Matteo Maffei, Kim Pecina:
The CASPA Tool: Causality-Based Abstraction for Security Protocol Analysis. 419-422 - Johannes Kinder, Helmut Veith:
Jakstab: A Static Analysis Platform for Binaries. 423-427 - Stephen Magill, Ming-Hsien Tsai, Peter Lee, Yih-Kuen Tsay:
THOR: A Tool for Reasoning about Shape and Arithmetic. 428-432
Hardware Verification I
- Cindy Eisner, Amir Nahir, Karen Yorav:
Functional Verification of Power Gated Designs by Compositional Reasoning. 433-445 - Per Bjesse:
A Practical Approach to Word Level Model Checking of Industrial Netlists. 446-458
Hardware Verification II
- Sudipta Kundu, Sorin Lerner, Rajesh Gupta:
Validating High-Level Synthesis. 459-472 - Oliver Wienand, Markus Wedler, Dominik Stoffel, Wolfgang Kunz, Gert-Martin Greuel:
An Algebraic Approach for Proving Data Correctness in Arithmetic Data Paths. 473-486 - 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
Model Checking
- Sujatha Kashyap, Vijay K. Garg:
Producing Short Counterexamples Using "Crucial Events". 491-503 - Peter Niebert, Doron A. Peled, Amir Pnueli:
Discriminative Model Checking. 504-516
Space Efficient Algorithms
- Rob J. van Glabbeek, Bas Ploeger:
Correcting a Space-Efficient Simulation Algorithm. 517-529 - Stefan Edelkamp, Peter Sanders, Pavel Simecek:
Semi-external LTL Model Checking. 530-542
Tools - Model Checking
- Simon J. Gay, Rajagopal Nagarajan, Nikolaos Papanikolaou:
QMC: A Model Checker for Quantum Systems. 543-547 - Axel Legay:
T(O)RMC: A Tool for (omega)-Regular Model Checking. 548-551 - Sebastian Kupferschmid, Martin Wehrle, Bernhard Nebel, Andreas Podelski:
Faster Than Uppaal? 552-555
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.
last updated on 2025-11-20 22:21 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
