


default search action
14th CAV 2002: Copenhagen, Denmark
- Ed Brinksma, Kim Guldstrand Larsen:

Computer Aided Verification, 14th International Conference, CAV 2002,Copenhagen, Denmark, July 27-31, 2002, Proceedings. Lecture Notes in Computer Science 2404, Springer 2002, ISBN 3-540-43997-8
Invited Talks
- Gerard J. Holzmann:

Software Analysis and Model Checking. 1-16 - Lintao Zhang, Sharad Malik:

The Quest for Efficient Boolean Satisfiability Solvers. 17-36
Invited Tutorials
- Patrick Cousot, Radhia Cousot:

On Abstraction in Software Verification. 37-56 - Thomas A. Henzinger:

The Symbolic Approach to Hybrid Systems. 57 - Wolfgang Thomas:

Infinite Games and Verification (Extended Abstract of a Tutorial). 58-64
Symbolic Model Checking
- Sharon Barner, Daniel Geist, Anna Gringauze:

Symbolic Localization Reduction with Reconstruction Layering and Backtracking. 65-77 - Randal E. Bryant, Shuvendu K. Lahiri, Sanjit A. Seshia:

Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions. 78-92 - Sharon Barner, Orna Grumberg:

Combining Symmetry Reduction and Under-Approximation for Symbolic Model Checking. 93-106
Abstraction/Refinement and Model Checking
- Amir Pnueli, Jessie Xu, Lenore D. Zuck:

Liveness with (0, 1, infty)-Counter Abstraction. 107-122 - Prosenjit Chatterjee, Hemanthkumar Sivaraj, Ganesh Gopalakrishnan:

Shared Memory Consistency Protocol Verification Against Weak Memory Models: Refinement via Model-Checking. 123-136 - Patrice Godefroid, Radha Jagadeesan:

Automatic Abstraction Using Generalized Model Checking. 137-150
Compositional/Structural Verification
- Jason Baumgartner, Andreas Kuehlmann, Jacob A. Abraham:

Property Checking via Structural Analysis. 151-165 - Sriram K. Rajamani, Jakob Rehof:

Conformance Checking for Models of Asynchronous Message Passing Software. 166-179 - Cormac Flanagan, Shaz Qadeer, Sanjit A. Seshia:

A Modular Checker for Multithreaded Programs. 180-194
Timing Analysis
- Tomohiro Yoneda, Tomoya Kitai, Chris J. Myers:

Automatic Derivation of Timing Constraints by Failure Analysis. 195-208 - Ofer Strichman

, Sanjit A. Seshia, Randal E. Bryant:
Deciding Separation Formulas with SAT. 209-222 - Håkan L. S. Younes, Reid G. Simmons:

Probabilistic Verification of Discrete Event Systems Using Acceptance Sampling. 223-235
SAT Based Methods
- Clark W. Barrett, David L. Dill, Aaron Stump:

Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT. 236-249 - Kenneth L. McMillan:

Applying SAT Methods in Unbounded Symbolic Model Checking. 250-264 - Edmund M. Clarke, Anubhav Gupta, James H. Kukula, Ofer Strichman:

SAT Based Abstraction-Refinement Using ILP and Machine Learning Techniques. 265-279 - Jesse D. Bingham, Alan J. Hu:

Semi-formal Bounded Model Checking. 280-294
Symbolic Model Checking
- Marco Bozzano, Giorgio Delzanno:

Algorithmic Verification of Invalidation-Based Protocols. 295-308 - Christian Jacobi:

Formal Verification of Complex Out-of-Order Pipelines by Combining Model-Checking and Theorem-Proving. 309-323 - Yannick Chevalier, Laurent Vigneron:

Automated Unbounded Verification of Security Protocols. 324-337
Tool Presentations
- Rajeev Alur, Michael McDougall, Zijiang Yang:

Exploiting Behavioral Hierarchy for Efficient Model Checking. 338-342 - Marius Bozga, Susanne Graf, Laurent Mounier:

IF-2.0: A Validation Environment for Component-Based Real-Time Systems. 343-348 - Alessandro Armando, David A. Basin, Mehdi Bouallagui, Yannick Chevalier, Luca Compagna, Sebastian Mödersheim

, Michaël Rusinowitch, Mathieu Turuani, Luca Viganò, Laurent Vigneron:
The AVISS Security Protocol Analysis Tool. 349-353 - Eugene Asarin

, Gordon J. Pace, Gerardo Schneider, Sergio Yovine
:
SPeeDI - A Verification Tool for Polygonal Hybrid Systems. 354-358 - Alessandro Cimatti

, Edmund M. Clarke, Enrico Giunchiglia, Fausto Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, Armando Tacchella
:
NuSMV 2: An OpenSource Tool for Symbolic Model Checking. 359-364 - Eugene Asarin

, Thao Dang, Oded Maler:
The d/dt Tool for Verification of Hybrid Systems. 365-370
Infinite State Model Checking
- Orna Kupferman, Nir Piterman, Moshe Y. Vardi:

Model Checking Linear Properties of Prefix-Recognizable Systems. 371-385 - Tatiana Rybina, Andrei Voronkov:

Using Canonical Representations of Solutions to Speed Up Infinite-State Model Checking. 386-400 - Walter Hartong, Lars Hedrich, Erich Barke:

On Discrete Modeling and Model Checking for Nonlinear Analog Systems. 401-413
Compositional/Structural Verification
- Arindam Chakrabarti, Luca de Alfaro, Thomas A. Henzinger, Freddy Y. C. Mang:

Synchronous and Bidirectional Component Interfaces. 414-427 - Arindam Chakrabarti, Luca de Alfaro, Thomas A. Henzinger, Marcin Jurdzinski, Freddy Y. C. Mang:

Interface Compatibility Checking for Software Modules. 428-441 - Michael Colón, Henny Sipma:

Practical Methods for Proving Program Termination. 442-454
Extended Model Checking
- Li Tan, Rance Cleaveland:

Evidence-Based Model Checking. 455-470 - Gianpiero Cabodi, Sergio Nocco, Stefano Quer

:
Mixing Forward and Backward Traversals in Guided-Prioritized BDD-Based Verification. 471-484 - Mitra Purandare, Fabio Somenzi:

Vacuum Cleaning CTL Formulae. 485-499
Tool Presentations
- Aaron Stump, Clark W. Barrett, David L. Dill:

CVC: A Cooperating Validity Checker. 500-504 - Marsha Chechik, Arie Gurfinkel

, Benet Devereux:
chi-Chek: A Multi-valued Model-Checker. 505-509 - Shoham Ben-David, Anna Gringauze, Baruch Sterin, Yaron Wolfsthal:

PathFinder: A Tool for Design Exploration. 510-514 - Dennis Dams, William Hesse, Gerard J. Holzmann:

Abstracting C with abC. 515-520 - Alex Groce, Doron A. Peled, Mihalis Yannakakis:

AMC: An Adaptive Model Checker. 521-525
Code Verification
- Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, George C. Necula, Grégoire Sutre, Westley Weimer:

Temporal-Safety Proofs for Systems Code. 526-538
Regular Model Checking and Acceleration
- Ahmed Bouajjani, Tayssir Touili:

Extrapolating Tree Transformations. 539-554 - Parosh Aziz Abdulla, Bengt Jonsson, Pritha Mahata, Julien d'Orso:

Regular Tree Model Checking. 555-568 - Robert P. Kurshan, Vladimir Levin, Hüsnü Yenigün:

Compressing Transitions for Model Checking. 569-581
Model Reduction
- Victor Khomenko, Maciej Koutny, Walter Vogler:

Canonical Prefixes of Petri Net Unfoldings. 582-595 - Stefan Blom, Jaco van de Pol:

State Space Reduction by Proving Confluence. 596-609 - Sankar Gurumurthy, Roderick Bloem, Fabio Somenzi:

Fair Simulation Minimization. 610-624

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.


Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID














