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.