default search action
11th TACAS 2005: Edinburgh, UK (Part of ETAPS 2005)
- Nicolas Halbwachs, Lenore D. Zuck:
Tools and Algorithms for the Construction and Analysis of Systems, 11th International Conference, TACAS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings. Lecture Notes in Computer Science 3440, Springer 2005, ISBN 3-540-25333-5
Invited Paper
- Kenneth L. McMillan:
Applications of Craig Interpolants in Model Checking. 1-12
Regular Model-Checking
- Ahmed Bouajjani, Peter Habermehl, Pierre Moro, Tomás Vojnar:
Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking. 13-29 - Parosh Aziz Abdulla, Axel Legay, Julien d'Orso, Ahmed Rezine:
Simulation-Based Iteration of Tree Transducers. 30-44 - Abhay Vardhan, Koushik Sen, Mahesh Viswanathan, Gul Agha:
Using Language Inference to Verify Omega-Regular Properties. 45-60
Infinite State Systems
- Rajeev Alur, Swarat Chaudhuri, Kousha Etessami, P. Madhusudan:
On-the-Fly Reachability and Cycle Detection for Recursive State Machines. 61-76 - Jesse D. Bingham, Alan J. Hu:
Empirically Efficient Verification for a Class of Infinite-State Systems. 77-92 - Shaz Qadeer, Jakob Rehof:
Context-Bounded Model Checking of Concurrent Software. 93-107 - Yoshinao Isobe, Markus Roggenbach
:
A Generic Theorem Prover of CSP Refinement. 108-123
Abstract Interpretation
- Amir Pnueli, Andreas Podelski, Andrey Rybalchenko:
Separating Fairness and Well-Foundedness for the Analysis of Fair Discrete Systems. 124-139 - Francesco Ranzato, Francesco Tapparo:
An Abstract Interpretation-Based Refinement Algorithm for Strong Preservation. 140-156 - Raghavan Komondoor, Ganesan Ramalingam, Satish Chandra, John Field:
Dependent Types for Program Understanding. 157-173
Automata and Logics
- Stefan Schwoon, Javier Esparza
A Note on On-the-Fly Verification Algorithms. 174-190 - Moritz Hammer, Alexander Knapp, Stephan Merz:
Truly On-the-Fly LTL Model Checking. 191-205 - Orna Kupferman, Moshe Y. Vardi:
Complementation Constructions for Nondeterministic Automata on Infinite Words. 206-221 - Will Marrero:
Using BDDs to Decide CTL. 222-236
Probabilistic Systems, Probabilistic Model-Checking
- Anne Remke, Boudewijn R. Haverkort
Model Checking Infinite-State Markov Chains. 237-252 - Kousha Etessami, Mihalis Yannakakis:
Algorithmic Verification of Recursive Probabilistic State Machines. 253-270 - Radu Grosu, Scott A. Smolka:
Monte Carlo Model Checking. 271-286
Satisfiability
- HoonSang Jin, HyoJung Han, Fabio Somenzi:
Efficient Conflict Analysis for Finding All Satisfying Assignments of a Boolean Circuit. 287-300 - Babita Sharma, Paritosh K. Pandya, Supratik Chakraborty
Bounded Validity Checking of Interval Duration Logic. 301-316 - Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti
An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic. 317-333 - K. Rustan M. Leino, Madan Musuvathi, Xinming Ou:
A Two-Tier Technique for Supporting Quantifiers in a Lazily Proof-Explicating Theorem Prover. 334-348
Testing
- Bertrand Jeannet, Thierry Jéron, Vlad Rusu, Elena Zinovieva:
Symbolic Test Selection Based on Approximate Analysis. 349-364 - Tao Xie, Darko Marinov, Wolfram Schulte, David Notkin:
Symstra: A Framework for Generating Object-Oriented Unit Tests Using Symbolic Execution. 365-381
Abstraction and Reduction
- E. Allen Emerson, Thomas Wahl:
Dynamic Symmetry Reduction. 382-396 - Himanshu Jain, Franjo Ivancic, Aarti Gupta, Malay K. Ganai:
Localization and Register Sharing for Predicate Abstraction. 397-412 - Jie-Hong Roland Jiang:
On Some Transformation Invariants Under Retiming and Resynthesis. 413-428
Specification, Program Synthesis
- Blaise Genest:
Compositional Message Sequence Charts (CMSCs) Are Better to Implement Than MSCs. 429-444 - Hillel Kugler, David Harel, Amir Pnueli, Yuan Lu, Yves Bontemps:
Temporal Logic for Scenario-Based Specifications. 445-460 - Westley Weimer, George C. Necula:
Mining Temporal Specifications for Error Detection. 461-476 - Aidan Harding, Mark Ryan
A New Algorithm for Strategy Synthesis in LTL Games. 477-492
Model-Checking
- Viktor Schuppan, Armin Biere:
Shortest Counterexamples for Symbolic Model Checking of LTL with Past. 493-509 - Blaise Genest, Dietrich Kuske, Anca Muscholl, Doron A. Peled:
Snapshot Verification. 510-525 - Tonglaga Bao, Michael D. Jones:
Time-Efficient Model Checking with Magnetic Disk. 526-540
Tool Presentations
- Dejvuth Suwimonteerabuth, Stefan Schwoon, Javier Esparza
jMoped: A Java Bytecode Checker Based on Moped. 541-545 - Feng Chen, Grigore Rosu:
Java-MOP: A Monitoring Oriented Programming Environment for Java. 546-550 - Fabrice Bouquet, Frédéric Dadeau, Bruno Legeard, Mark Utting
JML-Testing-Tools: A Symbolic Animator for JML Specifications Using CLP. 551-556 - Tiziana Margaria, Ralf Nagel, Bernhard Steffen:
jETI: A Tool for Remote Tool Integration. 557-562 - Curtis W. Keller, Diptikalyan Saha, Samik Basu, Scott A. Smolka:
FocusCheck: A Tool for Model Checking and Debugging Sequential C Programs. 563-569 - Edmund M. Clarke, Daniel Kroening, Natasha Sharygina, Karen Yorav:
SATABS: SAT-Based Predicate Abstraction for ANSI-C. 570-574 - Malay K. Ganai, Aarti Gupta, Pranav Ashar:
DiVer: SAT-Based Model Checking Platform for Verifying Large Scale Systems. 575-580 - Damien Bergamini, Nicolas Descoubes, Christophe Joubert
BISIMULATOR: A Modular Tool for On-the-Fly Equivalence Checking. 581-585
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:17 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: