15. CAV 2003: Boulder, Colorado, USA

Warren A. Hunt Jr., Fabio Somenzi (Eds.): Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings. Lecture Notes in Computer Science 2725 Springer 2003, ISBN 3-540-40524-0

Extending Bounded Model Checking

Kenneth L. McMillan:
Interpolation and SAT-Based Model Checking. 1-13
Leonardo Mendonça de Moura, Harald Rueß, Maria Sorea:
Bounded Model Checking and Induction: From Refutation to Verification (Extended Abstract, Category A). 14-26

Cindy Eisner, Dana Fisman, John Havlicek, Yoad Lustig, Anthony McIsaac, David Van Campenhout:
Reasoning with Temporal Logic on Truncated Paths. 27-39
Gianfranco Ciardo, Radu Siminiceanu:
Structural Symbolic CTL Model Checking of Asynchronous Systems. 40-53
Orna Grumberg, Tamir Heyman, Assaf Schuster:
A Work-Efficient Distributed Algorithm for Reachability Analysis. 54-66

Rajeev Alur, Salvatore La Torre, P. Madhusudan:
Modular Strategies for Infinite Games on Recursive Graphs. 67-79
Jan Obdrzálek:
Fast Mu-Calculus Model Checking when Tree-Width Is Bounded. 80-92
Gaoyan Xie, Zhe Dang, Oscar H. Ibarra, Pierluigi San Pietro:
Dense Counter Machines and Verification Problems. 93-105

Bikram Sengupta, Rance Cleaveland:
TRIM: A Tool for Triggered Message Sequence Charts. 106-109
Rafael H. Bordini, Michael Fisher, Carmen Pardavila, Willem Visser, Michael Wooldridge:
Model Checking Multi-Agent Programs with CASP. 110-113
Doron Drusinsky:
Monitoring Temporal Rules Combined with Time Series. 114-117
Sébastien Bardin, Alain Finkel, Jérôme Leroux, Laure Petrucci:
FAST: Fast Acceleration of Symbolikc Transition Systems. 118-121
Dirk Beyer, Claus Lewerentz, Andreas Noack:
Rabbit: A Tool for BDD-Based Verification of Real-Time Systems. 122-125

Edmund M. Clarke, Orna Grumberg, Muralidhar Talupur, Dong Wang:
Making Predicate Abstraction Efficient: How to Eliminate Redundant Predicates. 126-140
Shuvendu K. Lahiri, Randal E. Bryant, Byron Cook:
A Symbolic Approach to Predicate Abstraction. 141-153
Sanjit A. Seshia, Randal E. Bryant:
Unbounded, Fully Symbolic Model Checking of Timed Automata using Boolean Methods. 154-166

Gaurav Chakravorty, Paritosh K. Pandya:
Digitizing Interval Duration Logic. 167-179
Patricia Bouyer, Deepak D'Souza, P. Madhusudan, Antoine Petit:
Timed Control with Partial Observability. 180-192
Bernard Boigelot, Frédéric Herbreteau, Sébastien Jodogne:
Hybrid Acceleration Using Real Vector Automata (Extended Abstract). 193-205

Aarti Gupta, Malay K. Ganai, Chao Wang, Zijiang Yang, Pranav Ashar:
Abstraction and BDDs Complement SAT-Based BMC in DiVer. 206-209
Marsha Chechik, Arie Gurfinkel:
TLQSolver: A Temporal Logic Query Checker. 210-214
Yifei Dong, C. R. Ramakrishnan, Scott A. Smolka:
Evidence Explorer: A Tool for Exploring Model-Checking Proofs. 215-218
Liana Bozga, Yassine Lakhnech, Michaël Périn:
HERMES: An Automatic Tool for Verification of Secrecy in Security Protocols. 219-222

Bernard Boigelot, Axel Legay, Pierre Wolper:
Iterating Transducers in the Large (Extended Abstract). 223-235
Parosh Aziz Abdulla, Bengt Jonsson, Marcus Nilsson, Julien d'Orso:
Algorithmic Improvements in Regular Model Checking. 236-248
Constantinos Bartzis, Tevfik Bultan:
Efficient Image Computation in Infinite State Model Checking. 249-261

Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Shaz Qadeer:
Thread-Modular Abstraction Refinement. 262-274
Sharon Shoham, Orna Grumberg:
A Game-Based Framework for CTL Counterexamples and 3-Valued Abstraction-Refinement. 275-287
Kedar S. Namjoshi:
Abstraction for Branching Time Properties. 288-300

Grigore Rosu, Ram Prasad Venkatesan, Jon Whittle, Laurentiu Leustean:
Certifying Optimality of State Estimation Programs. 301-314
Hardi Hungar, Oliver Niese, Bernhard Steffen:
Domain-Specific Optimization in Automata Learning. 315-327
Marcelo Glusman, Shmuel Katz:
Model Checking Conformance with Scenario-Based Specifications. 328-340

Shuvendu K. Lahiri, Randal E. Bryant:
Deductive Verification of Advanced Out-of-Order Microprocessors. 341-353
Cormac Flanagan, Rajeev Joshi, Xinming Ou, James B. Saxe:
Theorem Proving Using Lazy Proof Explication. 355-367

Roy Armoni, Limor Fix, Alon Flaisher, Orna Grumberg, Nir Piterman, Andreas Tiemeyer, Moshe Y. Vardi:
Enhanced Vacuity Detection in Linear Temporal Logic. 368-380
Yonit Kesten, Nir Piterman, Amir Pnueli:
Bridging the Gap between Fair Simulation and Trace Inclusion. 381-393
Marc Geilen:
An Improved On-The-Fly Tableau Construction for a Real-Time Temporal Logic. 394-406

Husam Abu-Haimed, Sergey Berezin, David L. Dill:
Strengthening Invariants by Symbolic Consistency Testing. 407-419
Michael Colón, Sriram Sankaranarayanan, Henny Sipma:
Linear Invariant Generation Using Non-linear Constraint Solving. 420-432

Gerd Behrmann, Kim Guldstrand Larsen, Radek Pelánek:
To Store or Not to Store. 433-445
Gordon J. Pace, Frédéric Lang, Radu Mateescu:
Calculating-Confluence Compositionally. 446-459

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

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