Front matter
1-18
Modeling for Mere Mortals
Jeff Kramer and Jeff Magee
19-33
Scheduling System Verification
Pao-Ann Hsiung, Farn Wang and Yue-Sun Kuo
34-43
A Period Assignment Algorithm for Real-Time System Design
Minsoo Ryu and Seongsoo Hong
44-58
Analyzing Stochastic Fixed-Priority Real-Time Systems
Mark K. Gardner and Jane W. S. Liu
59-73
Timed Diagnostics for Reachability Properties
Stavros Tripakis
74-88
Fighting Livelock in the i-Protocol: A Comparative Study of Verification Tools
A Comparative Study of Verification Tools
Yifei Dong, Xiaoqun Du, Y. S. Ramakrishna, C. R. Ramakrishnan and I. V. Ramakrishnan, et al.
89-103
Proving the Soundness of a Java Bytecode Verifier Specification in Isabelle/HOL
Cornelia Pusch
104-118
Automated Fast-Track Reconfiguration of Group Communication Systems
Christoph Kreitz
119-134
Specifications and Proofs for Ensemble Layers
Jason Hickey, Nancy Lynch and Robbert van Renesse
134-147
An Automated Analysis of Ping-Pong Interactions in E-Mail Services
Anne Bergeron and Jean-Christophe Manzoni
148-162
Automatic Verification of Cryptographic Protocols through Compositional Analysis Techniques
Davide Marchignoli and Fabio Martinelli
163-177
Verification of Hierarchical State/Event Systems Using Reusability and Compositionality
Gerd Behrmann, Kim G. Larsen, Henrik R. Andersen, Henrik Hulgaard and Jørn Lind-Nielsen
178-192
On Proving Safety Properties by Integrating Static Analysis, Theorem Proving and Abstraction
Vlad Rusu and Eli Singerman
193-207
Symbolic Model Checking without BDDs
Armin Biere, Alessandro Cimatti, Edmund Clarke and Yunshan Zhu
208-222
Symbolic Verification of Lossy Channel Systems: Application to the Bounded Retransmission Protocol
Parosh Abdulla, Aurore Annichini and Ahmed Bouajjani
223-239
Model Checking in CLP
Giorgio Delzanno and Andreas Podelski
240-254
Using Logic Programs with Stable Model Semantics to Solve Deadlock and Reachability Problems for 1-Safe Petri Nets
Keijo Heljanko
255-269
Finite State Verification for the Asynchronous π-Calculus
Ugo Montanari and Marco Pistore
270-284
Process Algebra in PVS
Twan Basten and Jozef Hooman
285-299
On the Benefits of Using the Up-To Techniques for Bisimulation Verification
Daniel Hirschkoff
300-314
Computing Strong/Weak Bisimulation Equivalences and Observation Congruence for Value-Passing Processes
Zhoujun Li and Huowang Chen
315-329
Hardware Testing Using a Communication Protocol Conformance Testing Tool
Hakim Kahlouche, César Viho and Massimo Zendri
330-344
A Light-Weight Framework for Hardware Verification
Christoph Kern, Tarik Ono-Tesfaye and Mark R. Greenstreet
345-359
An Easily Extensible Toolset for Tabular Mathematical Expressions
David Lorge Parnas and Dennis K. Peters
360-374
From DFA-Frameworks to DFA-Generators: A Unifying Multiparadigm Approach
Jens Knoop
375-389
A Theorem Prover-Based Analysis Tool for Object-Oriented Databases
David Spelt and Susan Even
390-404
DYANA: An Environment for Embedded System Design and Analysis
A. G. Bakhmurov, A. P. Kapitonova and R. L. Smeliansky
405-419
Path Exploration Tool
Elsa L. Gunter and Doron Peled
420-434
Modular State Level Analysis of Distributed Systems Techniques and Tool Support
Peter Buchholz and Peter Kemper
435-438
Some Issues in the Software Engineering of Verification Tools
Perdita Stevens
439-443
The ETI Online Service in Action
Volker Braun, Jürgen Kreileder, Tiziana Margaria and Bernhard Steffen
Back matter