default search action
19th CAV 2007: Berlin, Germany
- Werner Damm, Holger Hermanns
:
Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings. Lecture Notes in Computer Science 4590, Springer 2007, ISBN 978-3-540-73367-6
Invited Talks
- Byron Cook:
Automatically Proving Program Termination. 1 - David M. Russinoff:
A Mathematical Approach to RTL Verification. 2 - Thomas Kropf:
Software Bugs Seen from an Industrial Perspective or Can Formal Methods Help on Automotive Software Development? 3
Invited Tutorials
- Dirk Beyer
Algorithms for Interface Synthesis. 4-19 - Leonardo Mendonça de Moura, Bruno Dutertre, Natarajan Shankar:
A Tutorial on Satisfiability Modulo Theories. 20-36 - Gary T. Leavens, Joseph R. Kiniry, Erik Poll:
A JML Tutorial: Modular Specification and Verification of Functional Behavior for Java. 37 - Martin Fränzle
Verification of Hybrid Systems. 38
Session I: Compositionality
- Nishant Sinha, Edmund M. Clarke:
SAT-Based Compositional Verification Using Lazy Learning. 39-54 - Ariel Cohen, Kedar S. Namjoshi:
Local Proofs for Global Safety Properties. 55-67
Session II: Verification Process
- Denis Gopan, Thomas W. Reps:
Low-Level Library Analysis and Summarization. 68-81 - Sagar Chaki, Christian Schallhart, Helmut Veith:
Verification Across Intellectual Property Boundaries. 82-94
Session III: Timed Synthesis and Games
- Oded Maler, Dejan Nickovic, Amir Pnueli:
On Synthesizing Controllers from Bounded-Response Properties. 95-107 - Luca de Alfaro, Marco Faella:
An Accelerated Algorithm for 3-Color Parity Games with an Application to Timed Games. 108-120 - Gerd Behrmann, Agnès Cougnard, Alexandre David, Emmanuel Fleury, Kim Guldstrand Larsen, Didier Lime:
UPPAAL-Tiga: Time for Playing Games! 121-125 - Martin Ouimet, Kristina Lundqvist:
The TASM Toolset: Specification, Simulation, and Formal Verification of Real-Time Systems. 126-130
Session IV: Infinitive State Verification
- Bengt Jonsson, Mayank Saksena:
Systematic Acceleration in Regular Model Checking. 131-144 - Parosh Aziz Abdulla, Giorgio Delzanno, Ahmed Rezine:
Parameterized Verification of Infinite-State Processes with Global Conditions. 145-157
Session V: Tool Environment
- Hubert Garavel, Radu Mateescu, Frédéric Lang, Wendelin Serwe:
CADP 2006: A Toolbox for the Construction and Analysis of Distributed Processes. 158-163 - Dejvuth Suwimonteerabuth, Felix Berger, Stefan Schwoon, Javier Esparza
jMoped: A Test Environment for Java Programs. 164-167 - Nathaniel Charlton, Michael Huth:
Hector: Software Model Checking with Cooperating Analysis Plugins. 168-172 - Jean-Christophe Filliâtre, Claude Marché:
The Why/Krakatoa/Caduceus Platform for Deductive Program Verification. 173-177
Session VI: Shapes
- Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn, Thomas Wies, Hongseok Yang:
Shape Analysis for Composite Data Structures. 178-192 - Ranjit Jhala, Kenneth L. McMillan:
Array Abstractions from Proofs. 193-206 - Ahmed Bouajjani, Séverine Fratani, Shaz Qadeer:
Context-Bounded Analysis of Multithreaded Programs with Dynamic Linked Structures. 207-220 - Igor Bogudlov, Tal Lev-Ami, Thomas W. Reps, Mooly Sagiv:
Revamping TVLA: Making Parametric Shape Analysis Competitive. 221-225
Session VII: Concurrent Program Verification
- Vineet Kahlon, Yu Yang, Sriram Sankaranarayanan, Aarti Gupta:
Fast and Accurate Static Data-Race Detection for Concurrent Programs. 226-239 - Feng Chen, Grigore Rosu:
Parametric and Sliced Causality. 240-253 - Gaël Patin, Mihaela Sighireanu, Tayssir Touili:
Spade: Verification of Multithreaded Dynamic and Recursive Programs. 254-257
Session VIII: Reactive Designs
- Barbara Jobstmann, Stefan J. Galler, Martin Weiglhofer, Roderick Bloem:
Anzu: A Tool for Property Synthesis. 258-262 - Roderick Bloem
RAT: A Tool for the Formal Analysis of Requirements. 263-267
Session IX: Parallelisation
- Jonathan Ezekiel, Gerald Lüttgen, Gianfranco Ciardo
Parallelising Symbolic State-Space Generators. 268-280 - Jiri Barnat, Lubos Brim, Pavel Simecek:
I/O Efficient Accepting Cycle Detection. 281-293
Session X: Constraints and Decisions
- Robert Brummayer, Armin Biere:
C32SAT: Checking C Expressions. 294-297 - Clark W. Barrett, Cesare Tinelli
CVC3. 298-302 - Panagiotis Manolios
BAT: The Bit-Level Analysis Tool. 303-306 - Bernd Becker
LIRA: Handling Constraints of Linear Arithmetics over the Integers and the Reals. 307-310
Session XI: Probabilistic Verification
- Joost-Pieter Katoen, Daniel Klink, Martin Leucker
Three-Valued Abstraction for Continuous-Time Markov Chains. 311-324 - Luca de Alfaro, Pritam Roy:
Magnifying-Lens Abstraction for Markov Decision Processes. 325-338 - Arie Matsliah, Ofer Strichman
Underapproximation for Model-Checking Based on Random Cryptographic Constructions. 339-351
Session XII: Abstraction
- Chao Wang, Zijiang Yang, Aarti Gupta, Franjo Ivancic:
Using Counterexamples for Improving the Precision of Reachability Computation with Polyhedra. 352-365 - Domagoj Babic, Alan J. Hu:
Structural Abstraction of Software Verification Conditions. 366-378 - Sumit Gulwani, Ashish Tiwari:
An Abstract Domain for Analyzing Heap-Manipulating Low-Level Software. 379-392 - Thomas Wahl:
Adaptive Symmetry Reduction. 393-405
Session XIII: Assume-Guarantee Reasoning
- Orna Kupferman, Nir Piterman, Moshe Y. Vardi:
From Liveness to Promptness. 406-419 - Anubhav Gupta, Kenneth L. McMillan, Zhaohui Fu:
Automated Assumption Generation for Compositional Verification. 420-432
Session XIV: Hybrid Systems
- Marc Segelken:
Abstraction and Counterexample-Guided Construction of omega -Automata for Model Checking of Step-Discrete Linear Hybrid Models. 433-448 - Tarik Nahhal, Thao Dang:
Test Coverage for Continuous and Hybrid Systems. 449-462 - Erion Plaku
Hybrid Systems: From Verification to Falsification. 463-476
Session XV: Program Analysis
- Daphna Amit, Noam Rinetzky, Thomas W. Reps, Mooly Sagiv, Eran Yahav:
Comparison Under Abstraction for Verifying Linearizability. 477-490 - Thomas Ball, Orna Kupferman, Mooly Sagiv:
Leaping Loops in the Presence of Abstraction. 491-503 - Dirk Beyer
Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis. 504-518
Session XVI: SAT and Decision Procedures
- Vijay Ganesh
A Decision Procedure for Bit-Vectors and Arrays. 519-531 - Alessandro Cimatti
Boolean Abstraction for Temporal Logic Satisfiability. 532-546 - Roberto Bruttomesso, Alessandro Cimatti
A Lazy and Layered SMT($\mathcal{BV}$) Solver for Hard Industrial Verification Problems. 547-560
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 2024-11-19 20:33 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: