TACAS 2001

41 papers

1. A Library for Composite Symbolic Representations · Tuba Yavuz-Kahveci, Murat Tuncer, Tevfik Bultan
2. A Sweep-Line Method for State Space Exploration · Søren Christensen, Lars Michael Kristensen, Thomas Mailund
3. A Technique for Invariant Generation · Ashish Tiwari, Harald Rueß, Hassen Saïdi, Natarajan Shankar
4. Abstraction in Probabilistic Process Algebra · Suzana Andova, Jos C. M. Baeten
5. An Automata Based Interpretation of Live Sequence Charts · Jochen Klose, Hartmut Wittke
6. Assume-Guarantee Based Compositional Reasoning for Synchronous Timing Diagrams · Nina Amla, E. Allen Emerson, Kedar S. Namjoshi, Richard J. Trefler
7. Automated Test Generation from Timed Automata · Brian Nielsen, Arne Skou
8. Automatic Abstraction of Memories in the Formal Verification of Superscalar Microprocessors · Miroslav N. Velev
9. Automatic Deductive Verification with Invisible Invariants · Amir Pnueli, Sitvanit Ruah, Lenore D. Zuck
10. Boolean and Cartesian Abstraction for Model Checking C Programs · Thomas Ball, Andreas Podelski, Sriram K. Rajamani
11. Branching vs. Linear Time: Final Showdown · Moshe Y. Vardi
12. Building a Tool for the Analysis and Testing of Web Applications: Problems and Solutions · Filippo Ricca, Paolo Tonella
13. CPN/Tools: A Tool for Editing and Simulating Coloured Petri Nets ETAPS Tool Demonstration Related to TACAS · Michel Beaudouin-Lafon, Wendy E. Mackay, Mads Jensen, Peter Andersen, Paul Janecek, Henry Michael Lassen + 7 more
14. Combining Structural and Enumerative Techniques for the Validation of Bounded Petri Nets · Rubén Carvajal-Schiaffino, Giorgio Delzanno, Giovanni Chiola
15. Compositional Message Sequence Charts · Elsa L. Gunter, Anca Muscholl, Doron A. Peled
16. Coverage Metrics for Temporal Logic Model Checking · Hana Chockler, Orna Kupferman, Moshe Y. Vardi
17. Efficient Guiding Towards Cost-Optimality in UPPAAL · Gerd Behrmann, Ansgar Fehnker, Thomas Hune, Kim G. Larsen, Paul Pettersson, Judi Romijn
18. Finding Feasible Counter-examples when Model Checking Abstracted Java Programs · Corina S. Pasareanu, Matthew B. Dwyer, Willem Visser
19. First Passage Time Analysis of Stochastic Process Algebra Using Partial Orders · Theo C. Ruys, Rom Langerak, Joost-Pieter Katoen, Diego Latella, Mieke Massink
20. Hardware/Software Co-Design Using Functional Languages · Alan Mycroft, Richard Sharp
21. Implementing a Multi-valued Symbolic Model Checker · Marsha Chechik, Benet Devereux, Steve M. Easterbrook
22. Incremental Verification by Abstraction · Yassine Lakhnech, Saddek Bensalem, Sergey Berezin, Sam Owre
23. Is There a Best Symbolic Cycle-Detection Algorithm? · Kathi Fisler, Ranan Fraer, Gila Kamhi, Moshe Y. Vardi, Zijiang Yang
24. Language Containment Checking with Nondeterministic BDDs · Bernd Finkbeiner
25. Linear Parametric Model Checking of Timed Automata · Thomas Hune, Judi Romijn, Mariëlle Stoelinga, Frits W. Vaandrager
26. Model Checking CTL*[DC] · Paritosh K. Pandya
27. Model Checking Syllabi and Student Carreers · Roberto Sebastiani, Alessandro Tomasi, Fausto Giunchiglia
28. Parallel Model Checking for the Alternation Free µ-Calculus · Benedikt Bollig, Martin Leucker, Michael Weber
29. Parameterized Verification of Multithreaded Software Libraries · Thomas Ball, Sagar Chaki, Sriram K. Rajamani
30. Propositional Reasoning · Michael P. Fourman
31. Satisfiability Checking Using Boolean Expression Diagrams · Poul Frederick Williams, Henrik Reif Andersen, Henrik Hulgaard
32. Saturation: An Efficient Iteration Strategy for Symbolic State-Space Generation · Gianfranco Ciardo, Gerald Lüttgen, Radu Siminiceanu
33. Searching Powerset Automata by Combining Explicit-State and Symbolic Model Checking · Alessandro Cimatti, Marco Roveri, Piergiorgio Bertoli
34. Simulation Revisited · Li Tan, Rance Cleaveland
35. Synthesis of Linear Ranking Functions · Michael Colón, Henny Sipma
36. TATOO: Testing and Analysis Tool for Object- Oriented Software · Amie L. Souter, Tiffany M. Wong, Stacey A. Shindo, Lori L. Pollock
37. Testing an Intentional Naming Scheme Using Genetic Algorithms · Sarfraz Khurshid
38. The ASM Workbench - A Tool Environment for Computer-Aided Analysis and Validation of Abstract State Machine Models Tool Demonstration · Giuseppe Del Castillo
39. The Erlang Verification Tool · Thomas Noll, Lars-Åke Fredlund, Dilian Gurov
40. The LOOP Compiler for Java and JML · Joachim van den Berg, Bart Jacobs
41. Verification of Vortex Workflows · Xiang Fu, Tevfik Bultan, Richard Hull, Jianwen Su