default search action
17th CAV 2005: Edinburgh, Scotland, UK
- Kousha Etessami, Sriram K. Rajamani:
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
Invited Talks
- George C. Necula, Sumit Gulwani:
Randomized Algorithms for Program Analysis and Verification. 1 - Bob Bentley:
Validating a Modern Microprocessor. 2-4 - Carla Piazza, Marco Antoniotti, Venkatesh Mysore, Alberto Policriti
, Franz Winkler, Bud Mishra:
Algorithmic Algebraic Model Checking I: Challenges from Systems Biology. 5-19
Tools Competition
- Clark W. Barrett, Leonardo Mendonça de Moura, Aaron Stump:
SMT-COMP: Satisfiability Modulo Theories Competition. 20-23
Abstraction and Refinement
- Shuvendu K. Lahiri, Thomas Ball, Byron Cook:
Predicate Abstraction via Symbolic Decision Procedures. 24-38 - Ranjit Jhala, Kenneth L. McMillan:
Interpolant-Based Transition Relation Approximation. 39-51 - Corina S. Pasareanu, Radek Pelánek, Willem Visser:
Concrete Model Checking with Abstract Matching and Refinement. 52-66 - Thomas Ball, Orna Kupferman, Greta Yorsh:
Abstraction for Falsification. 67-81
Bounded Model Checking
- Ishai Rabinovitz, Orna Grumberg:
Bounded Model Checking of Concurrent Programs. 82-97 - Keijo Heljanko, Tommi A. Junttila, Timo Latvala:
Incremental and Complete Bounded Model Checking for Full PLTL. 98-111 - Anubhav Gupta, Ofer Strichman
Abstraction Refinement for Bounded Model Checking. 112-124 - Daijue Tang, Sharad Malik, Aarti Gupta, C. Norris Ip:
Symmetry Reduction in SAT-Based Model Checking. 125-138
Tool Papers I
- Yichen Xie, Alex Aiken:
Saturn: A SAT-Based Tool for Bug Detection. 139-143 - Ajay Chander, David Espinosa, Nayeem Islam, Peter Lee, George C. Necula:
JVer: A Java Verifier. 144-147 - Matthew B. Dwyer, John Hatcliff, Matthew Hoosier, Robby:
Building Your Own Software Model Checker Using the Bogor Extensible Model Checking Framework. 148-152 - Sharon Barner, Ziv Glazberg, Ishai Rabinovitz:
Wolf - Bug Hunter for Concurrent Software Using Formal Methods. 153-157 - 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 - Sagar Chaki, James Ivers, Natasha Sharygina, Kurt C. Wallnau:
The ComFoRT Reasoning Framework. 164-169
Verification of Hardware, Microcode, and Synchronous Systems
- Roope Kaivola:
Formal Verification of Pentium® 4 Components with Symbolic Simulation and Inductive Invariants. 170-184 - 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 - David Monniaux
Compositional Analysis of Floating-Point Linear Numerical Filters. 199-212 - Eric Vecchié, Robert de Simone:
Syntax-Driven Reachable State Space Construction of Synchronous Reactive Programs. 213-225
Games and Probabilistic Verification
- Barbara Jobstmann, Andreas Griesmayer, Roderick Bloem
Program Repair as a Game. 226-238 - Amitabha Roy, K. Gopinath:
Improved Probabilistic Models for 802.11 Protocol Verification. 239-252 - Håkan L. S. Younes:
Probabilistic Verification for "Black-Box" Systems. 253-265 - Koushik Sen, Mahesh Viswanathan, Gul Agha:
On Statistical Model Checking of Stochastic Systems. 266-280
Tool Papers II
- Alessandro Armando, David A. Basin
The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications. 281-285 - Julien Olivain, Jean Goubault-Larrecq:
The Orchids Intrusion Detection Tool. 286-290 - Clark W. Barrett, Yi Fang, Benjamin Goldberg, Ying Hu, Amir Pnueli, Lenore D. Zuck:
TVOC: A Translation Validator for Optimizing Compilers. 291-295 - Byron Cook, Daniel Kroening, Natasha Sharygina:
Cogent: Accurate Theorem Proving for Program Verification. 296-300 - Franjo Ivancic, Zijiang Yang, Malay K. Ganai, Aarti Gupta, Ilya Shlyakhter, Pranav Ashar:
F-Soft: Software Verification Platform. 301-306
Decision Procedures and Applications
- Orly Meir, Ofer Strichman
Yet Another Decision Procedure for Equality Logic. 307-320 - Robert Nieuwenhuis, Albert Oliveras
DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic. 321-334 - Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti
Efficient Satisfiability Modulo Theories via Delayed Theory Combination. 335-349
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 - Marcelo d'Amorim
Efficient Monitoring of omega-Languages. 364-378 - Michael Benedikt, Angela Bonifati
Verification of Tree Updates for Optimization. 379-393 - Gilles Geeraerts, Jean-François Raskin, Laurent Van Begin:
Expand, Enlarge and Check... Made Efficient. 394-407
Tool Papers III
- Ittai Balaban, Yi Fang, Amir Pnueli, Lenore D. Zuck:
IIV: An Invisible Invariant Verifier. 408-412 - Tuba Yavuz-Kahveci, Constantinos Bartzis, Tevfik Bultan:
Action Language Verifier, Extended. 413-417 - Guillaume Gardey, Didier Lime, Morgan Magnin, Olivier H. Roux:
Romeo: A Tool for Analyzing Time Petri Nets. 418-423 - Enric Pastor, Marco A. Peña, Marc Solé:
TRANSYT: A Tool for the Verification of Asynchronous Concurrent Systems. 424-428 - Håkan L. S. Younes:
Ymer: A Statistical Model Checker. 429-433
Program Analysis and Verification I
- Akash Lal, Thomas W. Reps, Gogul Balakrishnan:
Extended Weighted Pushdown Systems. 434-448 - Christopher L. Conway, Kedar S. Namjoshi, Dennis Dams, Stephen A. Edwards:
Incremental Algorithms for Inter-procedural Analysis of Safety Properties. 449-461 - Alexandru Costan, Stephane Gaubert, Eric Goubault, Matthieu Martel, Sylvie Putot:
A Policy Iteration Algorithm for Computing Fixed Points in Static Analysis of Programs. 462-475
Program Analysis and Verification II
- Scott McPeak, George C. Necula:
Data Structure Specifications via Local Equality Axioms. 476-490 - Aaron R. Bradley, Zohar Manna, Henny B. Sipma:
Linear Ranking with Reachability. 491-504 - Vineet Kahlon, Franjo Ivancic, Aarti Gupta:
Reasoning About Threads Communicating via Locks. 505-518
Applications of Learning
- Alexey Loginov, Thomas W. Reps, Shmuel Sagiv:
Abstraction Refinement via Inductive Learning. 519-533 - Sagar Chaki, Edmund M. Clarke, Nishant Sinha, Prasanna Thati:
Automated Assume-Guarantee Reasoning for Simulation Conformance. 534-547 - Rajeev Alur, P. Madhusudan, Wonhong Nam:
Symbolic Compositional Verification by Learning Assumptions. 548-562
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 2024-12-23 19:18 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: