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

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, Lucia Cloth:
  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, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani:
  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, Pierre-Yves Schobbens:
  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 Peled:
  Snapshot Verification. 510-525
  
• Tonglaga Bao, Michael 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, Radu Mateescu:
  BISIMULATOR: A Modular Tool for On-the-Fly Equivalence Checking. 581-585