default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID13th CAV 2001: Paris, France
- Gérard Berry, Hubert Comon, Alain Finkel:
Computer Aided Verification, 13th International Conference, CAV 2001, Paris, France, July 18-22, 2001, Proceedings. Lecture Notes in Computer Science 2102, Springer 2001, ISBN 3-540-42345-1
Invited Talk
- David Lorge Parnas:
Software Documentation and the Verification Process. 1
Model Checking and Theorem Proving
- Kedar S. Namjoshi:
Certifying Model Checkers. 2-13 - Yves Bertot:
Formalizing a JVML Verifier for Initialization in a Theorem Prover. 14-24 - Abhik Roychoudhury
, I. V. Ramakrishnan:
Automated Inductive Verification of Parameterized Protocols. 25-37
Automata Techniques
- Girish Bhat, Rance Cleaveland, Alex Groce:
Efficient Model Checking Via Büchi Tableau Automata. 38-52 - Paul Gastin, Denis Oddoux:
Fast LTL to Büchi Automata Translation. 53-65 - Hana Chockler, Orna Kupferman, Robert P. Kurshan, Moshe Y. Vardi:
A Practical Approach to Coverage in Model Checking. 66-78
Verification Core Technology
- Agostino Dovier, Carla Piazza, Alberto Policriti:
A Fast Bisimulation Algorithm. 79-90 - A. Prasad Sistla, Patrice Godefroid:
Symmetry and Reduced Symmetry in Model Checking. 91-103 - Andreas Kuehlmann, Jason Baumgartner:
Transformation-Based Verification Using Generalized Retiming. 104-117
BDD and Decision Procedures
- Gianpiero Cabodi:
Meta-BDDs: A Decomposed Representation for Layered Symbolic Manipulation of Boolean Functions. 118-130 - John Moondanos, Carl-Johan H. Seger, Ziyad Hanna, Daher Kaiss:
CLEVER: Divide and Conquer Combinational Logic Equivalence VERification with False Negative Elimination. 131-143 - Yoav Rodeh, Ofer Strichman:
Finite Instantiations in Equivalence Logic with Uninterpreted Functions. 144-154
Abstraction and Refinement
- Alexander Asteroth, Christel Baier, Ulrich Aßmann:
Model Checking with Formula-Dependent Abstract Models. 155-168 - Rajeev Alur, Bow-Yaw Wang:
Verifying Network Protocol Implementations by Symbolic Refinement Checking. 169-181 - Hao Zheng, Eric Mercer, Chris J. Myers:
Automatic Abstraction for Verification of Timed Circuits and Systems. 182-193
Combinations
- Marta Z. Kwiatkowska, Gethin Norman, Roberto Segala:
Automated Verification of a Randomized Distributed Consensus Protocol Using Cadence SMV and PRISM. 194-206 - Rajeev Alur, Kousha Etessami, Mihalis Yannakakis:
Analysis of Recursive State Machines. 207-220 - Tamarah Arons, Amir Pnueli, Sitvanit Ruah, Jiazhao Xu, Lenore D. Zuck:
Parameterized Verification with Automatically Computed Inductive Assertions. 221-234
Tool Presentations: Rewriting and Theorem-Proving Techniques
- Miroslav N. Velev, Randal E. Bryant:
EVC: A Validity Checker for the Logic of Equality with Uninterpreted Functions and Memories, Exploiting Positive Equality, and Conservative Transformations. 235-240 - Dawn Xiaodong Song, Adrian Perrig, Doantam Phan:
AGVI - Automatic Generation, Verification, and Implementation of Security Protocols. 241-245 - Jean-Christophe Filliâtre, Sam Owre, Harald Rueß, Natarajan Shankar:
ICS: Integrated Canonizer and Solver. 246-249 - Stefan Blom, Wan J. Fokkink, Jan Friso Groote, Izak van Langevelde, Bert Lisser, Jaco van de Pol:
µCRL: A Toolset for Analysing Algebraic Specifications. 250-254 - Martin Leucker, Thomas Noll:
Truth/SLC - A Parallel Verification Platform for Concurrent Systems. 255-259 - Thomas Ball, Sriram K. Rajamani:
The SLAM Toolkit. 260-264
Invited Talk
- Xavier Leroy:
Java Bytecode Verification: An Overview. 265-285
Infinite State Systems
- Dennis Dams, Yassine Lakhnech, Martin Steffen:
Iterating Transducers. 286-297 - Giorgio Delzanno, Jean-François Raskin, Laurent Van Begin:
Attacking Symbolic State Explosion. 298-310 - Monika Maidl:
A Unifying Model Checking Approach for Safety Properties of Parameterized Systems. 311-323 - Javier Esparza, Stefan Schwoon:
A BDD-Based Model Checker for Recursive Programs. 324-336
Temporal Logics and Verification
- Luca de Alfaro:
Model Checking the World Wide Web. 337-349 - Orna Grumberg, Tamir Heyman, Assaf Schuster:
Distributed Symbolic Model Checking for µ-Calculus. 350-362
Tool Presentations: Model-Checking and Automata Techniques
- Ilan Beer, Shoham Ben-David, Cindy Eisner, Dana Fisman, Anna Gringauze, Yoav Rodeh:
The Temporal Logic Sugar. 363-367 - Aurore Annichini, Ahmed Bouajjani, Mihaela Sighireanu:
TReX: A Tool for Reachability Analysis of Complex Systems. 368-372 - Peer Johannsen:
BooStER: Speeding Up RTL Property Checking of Digital Designs by Word-Level Abstarction. 373-377 - Vladimir Levin, Hüsnü Yenigün:
SDLcheck: A Model Checking Tool. 377 - Vivek K. Shanbhag, K. Gopinath, Markku Turunen, Ari Ahtiainen, Matti Luukkainen:
EASN: Integrating ASN.1 and Model Checking. 382-386 - Nina Amla, E. Allen Emerson, Robert P. Kurshan, Kedar S. Namjoshi:
Rtdt: A Front-End for Efficient Model Checking of Synchronous Timing Diagrams. 387-390 - Etienne Closse, Michel Poize, Jacques Pulou, Joseph Sifakis, Patrick Venier, Daniel Weil, Sergio Yovine:
TAXYS: A Tool for the Development and Verification of Real-Time Embedded Systems. 391-395
Microprocessor Verification, Cache Coherence
- Ranjit Jhala, Kenneth L. McMillan:
Microarchitecture Verification by Compositional Model Checking. 396-410 - J Strother Moore:
Rewriting for Symbolic Execution of State Machine Models. 411-422 - Tamarah Arons:
Using Timestamping and History Variables to Verify Sequential Consistency. 423-435
SAT, BDDs, and Applications
- Fady Copty, Limor Fix, Ranan Fraer, Enrico Giunchiglia, Gila Kamhi, Armando Tacchella, Moshe Y. Vardi:
Benefits of Bounded Model Checking at an Industrial Setting. 436-453 - Per Bjesse, Tim Leonard, Abdel Mokkedem:
Finding Bugs in an Alpha Microprocessor Using Satisfiability Solvers. 454-464 - Sumio Morioka, Yasunao Katayama, Toshiyuki Yamane:
Towards Efficient Verification of Arithmetic Algorithms over Galois Fields GF(2m). 465-477
Timed Automata
- Yasmina Abdeddaïm, Oded Maler:
Job-Shop Scheduling Using Timed Automata. 478-492 - Kim Guldstrand Larsen, Gerd Behrmann, Ed Brinksma, Ansgar Fehnker, Thomas Hune, Paul Pettersson, Judi Romijn:
As Cheap as Possible: Efficient Cost-Optimal Reachability for Priced Timed Automata. 493-505 - Zhe Dang:
Binary Reachability Analysis of Pushdown Timed Automata with Dense Clocks. 506-518
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-12 23:51 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:
