13. CAV 2001: Paris, France
Gérard Berry, Hubert Comon, Alain Finkel (Eds.): Computer Aided Verification, 13th International Conference, CAV 2001, Paris, France, July 18-22, 2001, Proceedings. Springer 2001 Lecture Notes in Computer Science 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
- Hana Chockler, Orna Kupferman, Robert P. Kurshan, Moshe Y. Vardi: A Practical Approach to Coverage in Model Checking. 66-78
Verification Core Technology
- 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
- 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 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
Invited Talk
- Xavier Leroy: Java Bytecode Verification: An Overview. 265-285
Infinite State Systems
- 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
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
- 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 Venter, 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
- 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
data released under the ODC-BY 1.0 license. See also our legal information page
last updated on 2013-06-17T203403 by the dblp team