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