| 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 |
図書
