default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID15th CAV 2003: Boulder, Colorado, USA
- Warren A. Hunt Jr., Fabio Somenzi:
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
Symbolic Model Checking
- 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
Games, Trees, and Counters
- 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
Tool Presentations I
- Bikram Sengupta, Rance Cleaveland:
TRIM: A Tool for Triggered Message Sequence Charts. 106-109 - Rafael H. Bordini, Michael Fisher, Carmen Pardavila, Willem Visser, Michael J. 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
Abstraction I
- 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
Dense Time
- 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
Tool Presentations (II)
- 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
Infinite State Systems
- 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
Abstraction II
- 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
Applications
- 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
Theorem Proving
- 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
Automata-Based Verification
- 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
Invariants
- 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
Explicit Model Checking
- 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
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-01 22:07 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:
