11. TACAS 2005: Edinburgh, UK (Part of ETAPS 2005)

Nicolas Halbwachs, Lenore D. Zuck (Eds.): 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 BibTeX

Invited Paper

Kenneth L. McMillan:
Applications of Craig Interpolants in Model Checking. 1-12
Electronic Edition (link) BibTeX

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
Electronic Edition (link) BibTeX
Parosh Aziz Abdulla, Axel Legay, Julien d'Orso, Ahmed Rezine:
Simulation-Based Iteration of Tree Transducers. 30-44
Electronic Edition (link) BibTeX
Abhay Vardhan, Koushik Sen, Mahesh Viswanathan, Gul Agha:
Using Language Inference to Verify Omega-Regular Properties. 45-60
Electronic Edition (link) BibTeX

Infinite State Systems

Rajeev Alur, Swarat Chaudhuri, Kousha Etessami, P. Madhusudan:
On-the-Fly Reachability and Cycle Detection for Recursive State Machines. 61-76
Electronic Edition (link) BibTeX
Jesse D. Bingham, Alan J. Hu:
Empirically Efficient Verification for a Class of Infinite-State Systems. 77-92
Electronic Edition (link) BibTeX
Shaz Qadeer, Jakob Rehof:
Context-Bounded Model Checking of Concurrent Software. 93-107
Electronic Edition (link) BibTeX
Yoshinao Isobe, Markus Roggenbach:
A Generic Theorem Prover of CSP Refinement. 108-123
Electronic Edition (link) BibTeX

Abstract Interpretation

Amir Pnueli, Andreas Podelski, Andrey Rybalchenko:
Separating Fairness and Well-Foundedness for the Analysis of Fair Discrete Systems. 124-139
Electronic Edition (link) BibTeX
Francesco Ranzato, Francesco Tapparo:
An Abstract Interpretation-Based Refinement Algorithm for Strong Preservation. 140-156
Electronic Edition (link) BibTeX
Raghavan Komondoor, Ganesan Ramalingam, Satish Chandra, John Field:
Dependent Types for Program Understanding. 157-173
Electronic Edition (link) BibTeX

Automata and Logics

Stefan Schwoon, Javier Esparza:
A Note on On-the-Fly Verification Algorithms. 174-190
Electronic Edition (link) BibTeX
Moritz Hammer, Alexander Knapp, Stephan Merz:
Truly On-the-Fly LTL Model Checking. 191-205
Electronic Edition (link) BibTeX
Orna Kupferman, Moshe Y. Vardi:
Complementation Constructions for Nondeterministic Automata on Infinite Words. 206-221
Electronic Edition (link) BibTeX
Will Marrero:
Using BDDs to Decide CTL. 222-236
Electronic Edition (link) BibTeX

Probabilistic Systems, Probabilistic Model-Checking

Anne Remke, Boudewijn R. Haverkort, Lucia Cloth:
Model Checking Infinite-State Markov Chains. 237-252
Electronic Edition (link) BibTeX
Kousha Etessami, Mihalis Yannakakis:
Algorithmic Verification of Recursive Probabilistic State Machines. 253-270
Electronic Edition (link) BibTeX
Radu Grosu, Scott A. Smolka:
Monte Carlo Model Checking. 271-286
Electronic Edition (link) BibTeX

Satisfiability

HoonSang Jin, HyoJung Han, Fabio Somenzi:
Efficient Conflict Analysis for Finding All Satisfying Assignments of a Boolean Circuit. 287-300
Electronic Edition (link) BibTeX
Babita Sharma, Paritosh K. Pandya, Supratik Chakraborty:
Bounded Validity Checking of Interval Duration Logic. 301-316
Electronic Edition (link) BibTeX
Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani:
An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic. 317-333
Electronic Edition (link) BibTeX
K. Rustan M. Leino, Madan Musuvathi, Xinming Ou:
A Two-Tier Technique for Supporting Quantifiers in a Lazily Proof-Explicating Theorem Prover. 334-348
Electronic Edition (link) BibTeX

Testing

Bertrand Jeannet, Thierry Jéron, Vlad Rusu, Elena Zinovieva:
Symbolic Test Selection Based on Approximate Analysis. 349-364
Electronic Edition (link) BibTeX
Tao Xie, Darko Marinov, Wolfram Schulte, David Notkin:
Symstra: A Framework for Generating Object-Oriented Unit Tests Using Symbolic Execution. 365-381
Electronic Edition (link) BibTeX

Abstraction and Reduction

E. Allen Emerson, Thomas Wahl:
Dynamic Symmetry Reduction. 382-396
Electronic Edition (link) BibTeX
Himanshu Jain, Franjo Ivancic, Aarti Gupta, Malay K. Ganai:
Localization and Register Sharing for Predicate Abstraction. 397-412
Electronic Edition (link) BibTeX
Jie-Hong Roland Jiang:
On Some Transformation Invariants Under Retiming and Resynthesis. 413-428
Electronic Edition (link) BibTeX

Specification, Program Synthesis

Blaise Genest:
Compositional Message Sequence Charts (CMSCs) Are Better to Implement Than MSCs. 429-444
Electronic Edition (link) BibTeX
Hillel Kugler, David Harel, Amir Pnueli, Yuan Lu, Yves Bontemps:
Temporal Logic for Scenario-Based Specifications. 445-460
Electronic Edition (link) BibTeX
Westley Weimer, George C. Necula:
Mining Temporal Specifications for Error Detection. 461-476
Electronic Edition (link) BibTeX
Aidan Harding, Mark Ryan, Pierre-Yves Schobbens:
A New Algorithm for Strategy Synthesis in LTL Games. 477-492
Electronic Edition (link) BibTeX

Model-Checking

Viktor Schuppan, Armin Biere:
Shortest Counterexamples for Symbolic Model Checking of LTL with Past. 493-509
Electronic Edition (link) BibTeX
Blaise Genest, Dietrich Kuske, Anca Muscholl, Doron Peled:
Snapshot Verification. 510-525
Electronic Edition (link) BibTeX
Tonglaga Bao, Michael Jones:
Time-Efficient Model Checking with Magnetic Disk. 526-540
Electronic Edition (link) BibTeX

Tool Presentations

Dejvuth Suwimonteerabuth, Stefan Schwoon, Javier Esparza:
jMoped: A Java Bytecode Checker Based on Moped. 541-545
Electronic Edition (link) BibTeX
Feng Chen, Grigore Rosu:
Java-MOP: A Monitoring Oriented Programming Environment for Java. 546-550
Electronic Edition (link) BibTeX
Fabrice Bouquet, Frédéric Dadeau, Bruno Legeard, Mark Utting:
JML-Testing-Tools: A Symbolic Animator for JML Specifications Using CLP. 551-556
Electronic Edition (link) BibTeX
Tiziana Margaria, Ralf Nagel, Bernhard Steffen:
jETI: A Tool for Remote Tool Integration. 557-562
Electronic Edition (link) BibTeX
Curtis W. Keller, Diptikalyan Saha, Samik Basu, Scott A. Smolka:
FocusCheck: A Tool for Model Checking and Debugging Sequential C Programs. 563-569
Electronic Edition (link) BibTeX
Edmund M. Clarke, Daniel Kroening, Natasha Sharygina, Karen Yorav:
SATABS: SAT-Based Predicate Abstraction for ANSI-C. 570-574
Electronic Edition (link) BibTeX
Malay K. Ganai, Aarti Gupta, Pranav Ashar:
DiVer: SAT-Based Model Checking Platform for Verifying Large Scale Systems. 575-580
Electronic Edition (link) BibTeX
Damien Bergamini, Nicolas Descoubes, Christophe Joubert, Radu Mateescu:
BISIMULATOR: A Modular Tool for On-the-Fly Equivalence Checking. 581-585
Electronic Edition (link) BibTeX