TACAS 2003

43 papers

1. A Generic On-the-Fly Solver for Alternation-Free Boolean Equation Systems · Radu Mateescu
2. A New Knowledge Representation Strategy for Cryptographic Protocol Analysis · Ivan Cibrario Bertolotti, Luca Durante, Riccardo Sisto, Adriano Valenzano
3. A Set of Performance and Dependability Analysis Components for CADP · Holger Hermanns, Christophe Joubert
4. An Online Proof-Producing Decision Procedure for Mixed-Integer Linear Arithmetic · Sergey Berezin, Vijay Ganesh, David L. Dill
5. Automated Module Composition · Stavros Tripakis
6. Automatic Abstraction without Counterexamples · Kenneth L. McMillan, Nina Amla
7. Automatic Test Generation with AGATHA · Céline Bigot, Alain Faivre, Jean-Pierre Gallois, Arnault Lapitre, David Lugato, Jean-Yves Pierron + 1 more
8. BANANA - A Tool for Boundary Ambients Nesting ANAlysis · Chiara Braghin, Agostino Cortesi, Stefano Filippone, Riccardo Focardi, Flaminia L. Luccio, Carla Piazza
9. Bounded Model Checking for Past LTL · Marco Benedetti, Alessandro Cimatti
10. Branching Processes of High-Level Petri Nets · Victor Khomenko, Maciej Koutny
11. Checking Properties of Heap-Manipulating Procedures with a Constraint Solver · Mandana Vaziri, Daniel Jackson
12. Code-Based Test Generation for Validation of Functional Processor Descriptions · Fabrice Baray, Philippe Codognet, Daniel Diaz, Henri Michel
13. Compositional Analysis for Verification of Parameterized Systems · Samik Basu, C. R. Ramakrishnan
14. Construction of Efficient BDDs for Bounded Arithmetic Constraints · Constantinos Bartzis, Tevfik Bultan
15. Counter-Example Guided Predicate Abstraction of Hybrid Systems · Rajeev Alur, Thao Dang, Franjo Ivancic
16. Decidability of Invariant Validation for Paramaterized Systems · Pascal Fontaine, E. Pascal Gribomont
17. Experimental Analysis of Different Techniques for Bounded Model Checking · Nina Amla, Robert P. Kurshan, Kenneth L. McMillan, Ricardo H. Medel
18. Generalized Symbolic Execution for Model Checking and Testing · Sarfraz Khurshid, Corina S. Pasareanu, Willem Visser
19. LTSA-MSC: Tool Support for Behaviour Model Elaboration Using Implied Scenarios · Sebastián Uchitel, Robert Chatley, Jeff Kramer, Jeff Magee
20. Large State Space Visualization · Jan Friso Groote, Frank van Ham
21. Learning Assumptions for Compositional Verification · Jamieson M. Cobleigh, Dimitra Giannakopoulou, Corina S. Pasareanu
22. Modeling and Analysis of Power-Aware Systems · Oleg Sokolsky, Anna Philippou, Insup Lee, Kyriakos Christou
23. Modular Strategies for Recursive Game Graphs · Rajeev Alur, Salvatore La Torre, P. Madhusudan
24. Multiple-Counterexample Guided Iterative Abstraction Refinement: An Industrial Evaluation · Marcelo Glusman, Gila Kamhi, Sela Mador-Haim, Ranan Fraer, Moshe Y. Vardi
25. On Optimal Scheduling under Uncertainty · Yasmina Abdeddaïm, Eugene Asarin, Oded Maler
26. On the Universal and Existential Fragments of the µ-Calculus · Thomas A. Henzinger, Orna Kupferman, Rupak Majumdar
27. Optimistic Synchronization-Based State-Space Reduction · Scott D. Stoller, Ernie Cohen
28. Pattern-Based Abstraction for Verifying Secrecy in Protocols · Liana Bozga, Yassine Lakhnech, Michaël Périn
29. Proof-Like Counter-Examples · Arie Gurfinkel, Marsha Chechik
30. Rapid Parameterized Model Checking of Snoopy Cache Coherence Protocols · E. Allen Emerson, Vineet Kahlon
31. Resets vs. Aborts in Linear Temporal Logic · Roy Armoni, Doron Bustan, Orna Kupferman, Moshe Y. Vardi
32. Saturation Unbound · Gianfranco Ciardo, Robert M. Marmorstein, Radu Siminiceanu
33. Schedulability Analysis Using Two Clocks · Elena Fersman, Leonid Mokrushin, Paul Pettersson, Wang Yi
34. Simple Representative Instantiations for Multicast Protocols · Javier Esparza, Monika Maidl
35. State Class Constructions for Branching Analysis of Time Petri Nets · Bernard Berthomieu, François Vernadat
36. Static Guard Analysis in Timed Automata Verification · Gerd Behrmann, Patricia Bouyer, Emmanuel Fleury, Kim Guldstrand Larsen
37. Strategies for Combining Decision Procedures · Sylvain Conchon, Sava Krstic
38. The Integrated CWB-NC/PIOATool for Functional Verification and Performance Analysis of Concurrent Systems · Dezhuang Zhang, Rance Cleaveland, Eugene W. Stark
39. Using Petri Net Invariants in State Space Construction · Karsten Schmidt
40. Verics: A Tool for Verifying Timed Automata and Estelle Specifications · Piotr Dembinski, Agata Janowska, Pawel Janowski, Wojciech Penczek, Agata Pólrola, Maciej Szreter + 2 more
41. Verification and Improvement of the Sliding Window Protocol · Dmitri Chkliaev, Jozef Hooman, Erik P. de Vink
42. Verification of Hybrid Systems Based on Counterexample-Guided Abstraction Refinement · Edmund M. Clarke, Ansgar Fehnker, Zhi Han, Bruce H. Krogh, Olaf Stursberg, Michael Theobald
43. What Are We Trying to Prove? Reflections on Experiences with Proof-Carrying Code · Peter Lee