17. CAV 2005:
Edinburgh,
Scotland,
UK
Kousha Etessami, Sriram K. Rajamani (Eds.):
Computer Aided Verification, 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005, Proceedings.
Lecture Notes in Computer Science 3576 Springer 2005, ISBN 3-540-27231-3 BibTeX
Invited Talks
Tools Competition
Abstraction and Refinement
Bounded Model Checking
Tool Papers I
- Yichen Xie, Alexander Aiken:
Saturn: A SAT-Based Tool for Bug Detection.
139-143
Electronic Edition (link) BibTeX
- Ajay Chander, David Espinosa, Nayeem Islam, Peter Lee, George C. Necula:
JVer: A Java Verifier.
144-147
Electronic Edition (link) BibTeX
- Matthew B. Dwyer, John Hatcliff, Matthew Hoosier, Robby:
Building Your Own Software Model Checker Using the Bogor Extensible Model Checking Framework.
148-152
Electronic Edition (link) BibTeX
- Sharon Barner, Ziv Glazberg, Ishai Rabinovitz:
Wolf - Bug Hunter for Concurrent Software Using Formal Methods.
153-157
Electronic Edition (link) BibTeX
- Gogul Balakrishnan, Thomas W. Reps, Nicholas Kidd, Akash Lal, Junghee Lim, David Melski, Radu Gruian, Suan Hsi Yong, Chi-Hua Chen, Tim Teitelbaum:
Model Checking x86 Executables with CodeSurfer/x86 and WPDS++.
158-163
Electronic Edition (link) BibTeX
- Sagar Chaki, James Ivers, Natasha Sharygina, Kurt C. Wallnau:
The ComFoRT Reasoning Framework.
164-169
Electronic Edition (link) BibTeX
Verification of Hardware,
Microcode,
and Synchronous Systems
- Roope Kaivola:
Formal Verification of Pentium® 4 Components with Symbolic Simulation and Inductive Invariants.
170-184
Electronic Edition (link) BibTeX
- Tamarah Arons, Elad Elster, Limor Fix, Sela Mador-Haim, Michael Mishaeli, Jonathan Shalev, Eli Singerman, Andreas Tiemeyer, Moshe Y. Vardi, Lenore D. Zuck:
Formal Verification of Backward Compatibility of Microcode.
185-198
Electronic Edition (link) BibTeX
- David Monniaux:
Compositional Analysis of Floating-Point Linear Numerical Filters.
199-212
Electronic Edition (link) BibTeX
- Eric Vecchié, Robert de Simone:
Syntax-Driven Reachable State Space Construction of Synchronous Reactive Programs.
213-225
Electronic Edition (link) BibTeX
Games and Probabilistic Verification
Tool Papers II
- Alessandro Armando, David A. Basin, Yohan Boichut, Yannick Chevalier, Luca Compagna, Jorge Cuéllar, Paul Hankes Drielsma, Pierre-Cyrille Héam, Olga Kouchnarenko, Jacopo Mantovani, Sebastian Mödersheim, David von Oheimb, Michaël Rusinowitch, Judson Santiago, Mathieu Turuani, Luca Viganò, Laurent Vigneron:
The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications.
281-285
Electronic Edition (link) BibTeX
- Julien Olivain, Jean Goubault-Larrecq:
The Orchids Intrusion Detection Tool.
286-290
Electronic Edition (link) BibTeX
- Clark W. Barrett, Yi Fang, Benjamin Goldberg, Ying Hu, Amir Pnueli, Lenore D. Zuck:
TVOC: A Translation Validator for Optimizing Compilers.
291-295
Electronic Edition (link) BibTeX
- Byron Cook, Daniel Kroening, Natasha Sharygina:
Cogent: Accurate Theorem Proving for Program Verification.
296-300
Electronic Edition (link) BibTeX
- Franjo Ivancic, Zijiang Yang, Malay K. Ganai, Aarti Gupta, Ilya Shlyakhter, Pranav Ashar:
F-Soft: Software Verification Platform.
301-306
Electronic Edition (link) BibTeX
Decision Procedures and Applications
Automata and Transition Systems
- Roberto Sebastiani, Stefano Tonetta, Moshe Y. Vardi:
Symbolic Systems, Explicit Properties: On Hybrid Approaches for LTL Symbolic Model Checking.
350-363
Electronic Edition (link) BibTeX
- Marcelo d'Amorim, Grigore Rosu:
Efficient Monitoring of omega-Languages.
364-378
Electronic Edition (link) BibTeX
- Michael Benedikt, Angela Bonifati, Sergio Flesca, Avinash Vyas:
Verification of Tree Updates for Optimization.
379-393
Electronic Edition (link) BibTeX
- Gilles Geeraerts, Jean-François Raskin, Laurent Van Begin:
Expand, Enlarge and Check... Made Efficient.
394-407
Electronic Edition (link) BibTeX
Tool Papers III
- Ittai Balaban, Yi Fang, Amir Pnueli, Lenore D. Zuck:
IIV: An Invisible Invariant Verifier.
408-412
Electronic Edition (link) BibTeX
- Tuba Yavuz-Kahveci, Constantinos Bartzis, Tevfik Bultan:
Action Language Verifier, Extended.
413-417
Electronic Edition (link) BibTeX
- Guillaume Gardey, Didier Lime, Morgan Magnin, Olivier H. Roux:
Romeo: A Tool for Analyzing Time Petri Nets.
418-423
Electronic Edition (link) BibTeX
- Enric Pastor, Marco A. Peña, Marc Solé:
TRANSYT: A Tool for the Verification of Asynchronous Concurrent Systems.
424-428
Electronic Edition (link) BibTeX
- Håkan L. S. Younes:
Ymer: A Statistical Model Checker.
429-433
Electronic Edition (link) BibTeX
Program Analysis and Verification I
Program Analysis and Verification II
Applications of Learning
Copyright © Sat May 16 23:00:37 2009
by Michael Ley (ley@uni-trier.de)
