default search action
6th TACAS 2000: Berlin, Germany (Part of ETAPS 2000)
- Susanne Graf, Michael I. Schwartzbach:
Tools and Algorithms for Construction and Analysis of Systems, 6th International Conference, TACAS 2000, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, Berlin, Germany, March 25 - April 2, 2000, Proceedings. Lecture Notes in Computer Science 1785, Springer 2000, ISBN 3-540-67282-6
Invited Contribution
- Pierre Wolper, Bernard Boigelot:
On the Construction of Automata from Linear Arithmetic Constraints. 1-19
Software and Formal Methods Tools
- Yuhong Xiong, Edward A. Lee:
An Extensible Type System for Component-Based Design. 20-37 - David Aspinall:
Proof General: A Generic Tool for Proof Development. 38-42 - Michael Goedicke, Bettina Enders, Torsten Meyer, Gabriele Taentzer:
ViewPoint-Oriented Software Development: Tool Support for Integrating Multiple Perspectives by Distributed Graph Transformation. 43-47
Formal Methods Tools
- Peter Braun, Heiko Lötzbeyer, Bernhard Schätz, Oscar Slotosch:
Consistent Integration of Formal Methods. 48-62 - Jörg Meyer, Arnd Poetzsch-Heffter:
An Architecture for Interactive Program Provers. 63-77 - Louise A. Dennis, Graham Collins, Michael Norrish, Richard J. Boulton, Konrad Slind, Graham Robinson, Michael J. C. Gordon, Thomas F. Melham:
The PROSPER Toolkit. 78-92 - Till Mossakowski:
CASL: From Semantics to Tools. 93-108
Timed and Hybrid Systems
- Sébastien Bornot, Gregor Gößler, Joseph Sifakis:
On the Construction of Live Timed Systems. 109-126 - Fredrik Larsson, Paul Pettersson, Wang Yi:
On Memory-Block Traversal Problems in Model-Checking Timed-Systems. 127-141 - Thomas A. Henzinger, Rupak Majumdar:
Symbolic Model Checking for Rectangular Hybrid Systems. 142-156 - Farn Wang:
Efficient Data Structure for Fully Symbolic Verification of Real-Time Software Systems. 157-171
Infinite and Parameterized Systems
- Abhik Roychoudhury, K. Narayan Kumar, C. R. Ramakrishnan, I. V. Ramakrishnan, Scott A. Smolka:
Verification of Parameterized Systems Using Logic Program Transformations. 172-187 - Kai Baukus, Saddek Bensalem, Yassine Lakhnech, Karsten Stahl:
Abstracting WS1S Systems to Verify Parameterized Networks. 188-203 - Jean-Paul Bodeveix, Mamoun Filali:
FMona: A Tool for Expressing Validation Techniques over Infinite State Systems. 204-219 - Bengt Jonsson, Marcus Nilsson:
Transitive Closures of Regular Relations for Verifying Infinite-State Systems. 220-234
Diagnostic and Test Generation
- Marius Bozga, Jean-Claude Fernandez, Lucian Ghirvu:
Using Static Analysis to Improve Automatic Test Generation. 235-250 - Radu Mateescu:
Efficient Diagnostic Generation for Boolean Equation Systems. 251-265
Efficient Model-Checking
- Jean-Pierre Krimm, Laurent Mounier:
Compositional State Space Generation with Partial Order Reductions for Asynchronous Communicating Systems. 266-282 - Juhana Helovuo, Antti Valmari:
Checking for CFFD-Preorder with Tester Processes. 283-298 - Thomas A. Henzinger, Sriram K. Rajamani:
Fair Bisimulation. 299-314 - Karsten Schmidt:
Integrating Low Level Symmetries into Reachability Analysis. 315-330
Model-Checking Tools
- Giuseppe Del Castillo, Kirsten Winter:
Model Checking Support for the ASM High-Level Language. 331-346 - Holger Hermanns, Joost-Pieter Katoen, Joachim Meyer-Kayser, Markus Siegle:
A Markov Chain Model Checker. 347-362 - Dragan Bosnacki, Dennis Dams, Leszek Holenderski, Natalia Sidorova:
Model Checking SDL with Spin. 363-377 - Ramesh Bharadwaj, Steve Sims:
Salsa: Combining Constraint Solvers with BDDs for Automatic Invariant Checking. 378-394
Symbolic Model-Checking
- Luca de Alfaro, Marta Z. Kwiatkowska, Gethin Norman, David Parker, Roberto Segala:
Symbolic Model Checking of Probabilistic Processes Using MTBDDs and the Kronecker Representation. 395-410 - Parosh Aziz Abdulla, Per Bjesse, Niklas Eén:
Symbolic Reachability Analysis Based on SAT-Solvers. 411-425 - Giorgio Delzanno, Jean-François Raskin:
Symbolic Representation of Upward-Closed Sets. 426-440 - Tevfik Bultan:
BDD vs. Constraint-Based Model Checking: An Experimental Evaluation for Asynchronous Concurrent Systems. 441-455
Visual Tools
- Magnus Niemann, Roswitha Bardohl:
Tool-Based Specification of Visual Languages and Graphic Editors. 456-470 - Moataz Kamel, Stefan Leue:
VIP: A Visual Editor and Compiler for v-Promela. 471-486
Verification of Critical Systems
- Tamarah Arons, Amir Pnueli:
A Comparison of Two Verification Methods for Speculative Instruction Execution. 487-502 - Edmund M. Clarke, Somesh Jha, Wilfredo R. Marrero:
Partial Order Reductions for Security Protocol Verification. 503-518 - Massimo Benerecetti, Fausto Giunchiglia:
Model Checking Security Protocols Using a Logic of Belief. 519-534 - Stefania Gnesi, Diego Latella, Gabriele Lenzini, C. Abbaneo, Arturo M. Amendola, P. Marmo:
A Formal Specification and Validation of a Critical System in Presence of Byzantine Errors. 535-549
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.