TACAS 2000

36 papers

1. A Comparison of Two Verification Methods for Speculative Instruction Execution · Tamarah Arons, Amir Pnueli
2. A Formal Specification and Validation of a Critical System in Presence of Byzantine Errors · Stefania Gnesi, Diego Latella, Gabriele Lenzini, C. Abbaneo, Arturo M. Amendola, P. Marmo
3. A Markov Chain Model Checker · Holger Hermanns, Joost-Pieter Katoen, Joachim Meyer-Kayser, Markus Siegle
4. Abstracting WS1S Systems to Verify Parameterized Networks · Kai Baukus, Saddek Bensalem, Yassine Lakhnech, Karsten Stahl
5. An Architecture for Interactive Program Provers · Jörg Meyer, Arnd Poetzsch-Heffter
6. An Extensible Type System for Component-Based Design · Yuhong Xiong, Edward A. Lee
7. BDD vs. Constraint-Based Model Checking: An Experimental Evaluation for Asynchronous Concurrent Systems · Tevfik Bultan
8. CASL: From Semantics to Tools · Till Mossakowski
9. Checking for CFFD-Preorder with Tester Processes · Juhana Helovuo, Antti Valmari
10. Compositional State Space Generation with Partial Order Reductions for Asynchronous Communicating Systems · Jean-Pierre Krimm, Laurent Mounier
11. Consistent Integration of Formal Methods · Peter Braun, Heiko Lötzbeyer, Bernhard Schätz, Oscar Slotosch
12. Efficient Data Structure for Fully Symbolic Verification of Real-Time Software Systems · Farn Wang
13. Efficient Diagnostic Generation for Boolean Equation Systems · Radu Mateescu
14. FMona: A Tool for Expressing Validation Techniques over Infinite State Systems · Jean-Paul Bodeveix, Mamoun Filali
15. Fair Bisimulation · Thomas A. Henzinger, Sriram K. Rajamani
16. Integrating Low Level Symmetries into Reachability Analysis · Karsten Schmidt
17. Model Checking SDL with Spin · Dragan Bosnacki, Dennis Dams, Leszek Holenderski, Natalia Sidorova
18. Model Checking Security Protocols Using a Logic of Belief · Massimo Benerecetti, Fausto Giunchiglia
19. Model Checking Support for the ASM High-Level Language · Giuseppe Del Castillo, Kirsten Winter
20. On Memory-Block Traversal Problems in Model-Checking Timed-Systems · Fredrik Larsson, Paul Pettersson, Wang Yi
21. On the Construction of Automata from Linear Arithmetic Constraints · Pierre Wolper, Bernard Boigelot
22. On the Construction of Live Timed Systems · Sébastien Bornot, Gregor Gößler, Joseph Sifakis
23. Partial Order Reductions for Security Protocol Verification · Edmund M. Clarke, Somesh Jha, Wilfredo R. Marrero
24. Proof General: A Generic Tool for Proof Development · David Aspinall
25. Salsa: Combining Constraint Solvers with BDDs for Automatic Invariant Checking · Ramesh Bharadwaj, Steve Sims
26. Symbolic Model Checking for Rectangular Hybrid Systems · Thomas A. Henzinger, Rupak Majumdar
27. Symbolic Model Checking of Probabilistic Processes Using MTBDDs and the Kronecker Representation · Luca de Alfaro, Marta Z. Kwiatkowska, Gethin Norman, David Parker, Roberto Segala
28. Symbolic Reachability Analysis Based on SAT-Solvers · Parosh Aziz Abdulla, Per Bjesse, Niklas Eén
29. Symbolic Representation of Upward-Closed Sets · Giorgio Delzanno, Jean-François Raskin
30. The PROSPER Toolkit · Louise A. Dennis, Graham Collins, Michael Norrish, Richard J. Boulton, Konrad Slind, Graham Robinson + 2 more
31. Tool-Based Specification of Visual Languages and Graphic Editors · Magnus Niemann, Roswitha Bardohl
32. Transitive Closures of Regular Relations for Verifying Infinite-State Systems · Bengt Jonsson, Marcus Nilsson
33. Using Static Analysis to Improve Automatic Test Generation · Marius Bozga, Jean-Claude Fernandez, Lucian Ghirvu
34. VIP: A Visual Editor and Compiler for v-Promela · Moataz Kamel, Stefan Leue
35. Verification of Parameterized Systems Using Logic Program Transformations · Abhik Roychoudhury, K. Narayan Kumar, C. R. Ramakrishnan, I. V. Ramakrishnan, Scott A. Smolka
36. ViewPoint-Oriented Software Development: Tool Support for Integrating Multiple Perspectives by Distributed Graph Transformation · Michael Goedicke, Bettina Enders, Torsten Meyer, Gabriele Taentzer