TACAS 2005

42 papers

1. A Generic Theorem Prover of CSP Refinement · Yoshinao Isobe, Markus Roggenbach
2. A New Algorithm for Strategy Synthesis in LTL Games · Aidan Harding, Mark Ryan, Pierre-Yves Schobbens
3. A Note on On-the-Fly Verification Algorithms · Stefan Schwoon, Javier Esparza
4. A Two-Tier Technique for Supporting Quantifiers in a Lazily Proof-Explicating Theorem Prover · K. Rustan M. Leino, Madan Musuvathi, Xinming Ou
5. Algorithmic Verification of Recursive Probabilistic State Machines · Kousha Etessami, Mihalis Yannakakis
6. An Abstract Interpretation-Based Refinement Algorithm for Strong Preservation · Francesco Ranzato, Francesco Tapparo
7. An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic · Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz + 1 more
8. Applications of Craig Interpolants in Model Checking · Kenneth L. McMillan
9. BISIMULATOR: A Modular Tool for On-the-Fly Equivalence Checking · Damien Bergamini, Nicolas Descoubes, Christophe Joubert, Radu Mateescu
10. Bounded Validity Checking of Interval Duration Logic · Babita Sharma, Paritosh K. Pandya, Supratik Chakraborty
11. Complementation Constructions for Nondeterministic Automata on Infinite Words · Orna Kupferman, Moshe Y. Vardi
12. Compositional Message Sequence Charts (CMSCs) Are Better to Implement Than MSCs · Blaise Genest
13. Context-Bounded Model Checking of Concurrent Software · Shaz Qadeer, Jakob Rehof
14. Dependent Types for Program Understanding · Raghavan Komondoor, Ganesan Ramalingam, Satish Chandra, John Field
15. DiVer: SAT-Based Model Checking Platform for Verifying Large Scale Systems · Malay K. Ganai, Aarti Gupta, Pranav Ashar
16. Dynamic Symmetry Reduction · E. Allen Emerson, Thomas Wahl
17. Efficient Conflict Analysis for Finding All Satisfying Assignments of a Boolean Circuit · HoonSang Jin, HyoJung Han, Fabio Somenzi
18. Empirically Efficient Verification for a Class of Infinite-State Systems · Jesse D. Bingham, Alan J. Hu
19. FocusCheck: A Tool for Model Checking and Debugging Sequential C Programs · Curtis W. Keller, Diptikalyan Saha, Samik Basu, Scott A. Smolka
20. JML-Testing-Tools: A Symbolic Animator for JML Specifications Using CLP · Fabrice Bouquet, Frédéric Dadeau, Bruno Legeard, Mark Utting
21. Java-MOP: A Monitoring Oriented Programming Environment for Java · Feng Chen, Grigore Rosu
22. Localization and Register Sharing for Predicate Abstraction · Himanshu Jain, Franjo Ivancic, Aarti Gupta, Malay K. Ganai
23. Mining Temporal Specifications for Error Detection · Westley Weimer, George C. Necula
24. Model Checking Infinite-State Markov Chains · Anne Remke, Boudewijn R. Haverkort, Lucia Cloth
25. Monte Carlo Model Checking · Radu Grosu, Scott A. Smolka
26. On Some Transformation Invariants Under Retiming and Resynthesis · Jie-Hong Roland Jiang
27. On-the-Fly Reachability and Cycle Detection for Recursive State Machines · Rajeev Alur, Swarat Chaudhuri, Kousha Etessami, P. Madhusudan
28. SATABS: SAT-Based Predicate Abstraction for ANSI-C · Edmund M. Clarke, Daniel Kroening, Natasha Sharygina, Karen Yorav
29. Separating Fairness and Well-Foundedness for the Analysis of Fair Discrete Systems · Amir Pnueli, Andreas Podelski, Andrey Rybalchenko
30. Shortest Counterexamples for Symbolic Model Checking of LTL with Past · Viktor Schuppan, Armin Biere
31. Simulation-Based Iteration of Tree Transducers · Parosh Aziz Abdulla, Axel Legay, Julien d'Orso, Ahmed Rezine
32. Snapshot Verification · Blaise Genest, Dietrich Kuske, Anca Muscholl, Doron A. Peled
33. Symbolic Test Selection Based on Approximate Analysis · Bertrand Jeannet, Thierry Jéron, Vlad Rusu, Elena Zinovieva
34. Symstra: A Framework for Generating Object-Oriented Unit Tests Using Symbolic Execution · Tao Xie, Darko Marinov, Wolfram Schulte, David Notkin
35. Temporal Logic for Scenario-Based Specifications · Hillel Kugler, David Harel, Amir Pnueli, Yuan Lu, Yves Bontemps
36. Time-Efficient Model Checking with Magnetic Disk · Tonglaga Bao, Michael D. Jones
37. Truly On-the-Fly LTL Model Checking · Moritz Hammer, Alexander Knapp, Stephan Merz
38. Using BDDs to Decide CTL · Will Marrero
39. Using Language Inference to Verify Omega-Regular Properties · Abhay Vardhan, Koushik Sen, Mahesh Viswanathan, Gul Agha
40. Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking · Ahmed Bouajjani, Peter Habermehl, Pierre Moro, Tomás Vojnar
41. jETI: A Tool for Remote Tool Integration · Tiziana Margaria, Ralf Nagel, Bernhard Steffen
42. jMoped: A Java Bytecode Checker Based on Moped · Dejvuth Suwimonteerabuth, Stefan Schwoon, Javier Esparza