SPIN经典论文集-第11届SPIN workshop论文集

Invited Paper Formal Analysis of Processor Timing Models Reinhard Wilhelm 1 Heuristics and Probabilities Typical Structural Properties of State Spaces Radek Pelánek 5 State Caching Reconsidered Jaco Geldenhuys 23 Directed Error Detection in C++ with the Assembly-Level Model Checker StEAM Peter Leven, Tilman Mehler, Stefan Edelkamp 39 Fast and Accurate Bitstate Verification for SPIN Peter C. Dillinger, Panagiotis Manolios 57 Improvements of SPIN Model-Driven Software Verification Gerard J. Holzmann, Rajeev Joshi 76 Minimization of Counterexamples in SPIN Paul Gastin, Pierre Moro, Marc Zeitoun 92 Validation of Timed Systems Black-Box Conformance Testing for Real-Time Systems Moez Krichen, Stavros Tripakis 109 Validation of UML Models via a Mapping to Communicating Extended Timed Automata Iulian Ober, Susanne Graf, Ileana Ober 127 Tool Papers Explicit State Model Checking with Hopper Michael Jones, Eric Mercer 146 SEQ.OPEN: A Tool for Efficient Trace-Based Verification Hubert Garavel, Radu Mateescu 151 X Table of Contents Model Checking Genetic Regulatory Networks Using GNA and CADP Grégory Batt, Damien Bergamini, Hidde de Jong, Hubert Garavel, Radu Mateescu 158 Abstraction and Symbolic Methods Verification of Java Programs Using Symbolic Execution and Invariant Generation Willem Visser Polynomial Time Image Computation with Interval-Definable Counters Systems Alain Finkel, Jérôme Leroux 182 Using Fairness to Make Abstractions Work Natalia Ioustinova, Natalia Sidorova 198 A Scalable Incomplete Test for Message Buffer Overflow in Promela Models Stefan Leue, Richard Mayr, Wei Wei 216 Applications Translation from Adapted UML to Promela for CORBA-Based Applications J. Chen, H. Cui 234 Verifying Commit-Atomicity Using Model-Checking Cormac Flanagan 252 Analysis of Distributed Spin Applied to Industrial-Scale Models Murali Rangarajan, Samar Dajani-Brown, Kirk Schloegel, Darren Cofer 267 Verification of MPI-Based Software for Scientific Computation Stephen F. Siegel, George S. Avrunin 286 Tutorials Advanced SPIN Tutorial Theo C. Ruys, Gerard J. Holzmann 304 IF Validation Environment Tutorial Marius Bozga, Susanne Graf, Laurent Mounier, Iulian Ober