14. CAV 2002: Copenhagen, Denmark

Ed Brinksma, Kim Guldstrand Larsen (Eds.): 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

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

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

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

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

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

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

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

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

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

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

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

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 Peled, Mihalis Yannakakis:
AMC: An Adaptive Model Checker. 521-525

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

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

Last update Tue May 22 23:23:21 2012 CET by the DBLP Team —

Data released under the ODC-BY 1.0 license — See also our legal information page