Model checking software : 11th International SPIN Workshop, Barcelona, Spain, April 1-3, 2004 : proceedings
Since 1995, when the SPIN workshop series was instigated, SPIN workshops have been held on an annual basis in Montr eal (1995), New Brunswick (1996), Enschede (1997), Paris (1998), Trento (1999), Toulouse (1999), Stanford (2000), Toronto (2001), Grenoble (2002) and Portland (2003). All but the ?rst...
Enregistré dans:
| Collectivité auteur: | |
|---|---|
| Autres auteurs: | , |
| Format: | Livre numérique |
| Langue: | Anglais |
| Publié: |
Berlin [etc.] :
Springer
[20..].
Cham : Springer Nature |
| Collection: | Lecture notes in computer science
2989 |
| Sujets: | |
| Accès en ligne: | Accès sur la plateforme de l'éditeur Accès sur la plateforme Istex Accès Université d'Orléans Accès INSA CVL |
| Note: |
Archives Springer e-books (Licence nationale) Archives Springer e-books (Licence nationale) |
| Autres localisations: | Voir dans le Sudoc |
| Edition sous un autre format: | • Model checking software, 11th International SPIN Workshop, Barcelona, Spain, April 1-3, 2004, proceedings, Susanne Graf, Laurent Mounier, eds, Berlin, Springer, 2004, 1 vol. (X-307 p.), Lecture notes in computer science, 3-540-21314-7 • Model Checking Software, Texte imprimé, 9783662184110 |
Table des matières:
- Invited Paper
- Formal Analysis of Processor Timing Models
- Heuristics and Probabilities
- Typical Structural Properties of State Spaces
- State Caching Reconsidered
- Directed Error Detection in C++ with the Assembly-Level Model Checker StEAM
- Fast and Accurate Bitstate Verification for SPIN
- Improvements of SPIN
- Model-Driven Software Verification
- Minimization of Counterexamples in SPIN
- Validation of Timed Systems
- Black-Box Conformance Testing for Real-Time Systems
- Validation of UML Models via a Mapping to Communicating Extended Timed Automata
- Tool Papers
- Explicit State Model Checking with Hopper
- SEQ.OPEN: A Tool for Efficient Trace-Based Verification
- Model Checking Genetic Regulatory Networks Using GNA and CADP
- Abstraction and Symbolic Methods
- Verification of Java Programs Using Symbolic Execution and Invariant Generation
- Polynomial Time Image Computation with Interval-Definable Counters Systems
- Using Fairness to Make Abstractions Work
- A Scalable Incomplete Test for Message Buffer Overflow in Promela Models
- Applications
- Translation from Adapted UML to Promela for CORBA-Based Applications
- Verifying Commit-Atomicity Using Model-Checking
- Analysis of Distributed Spin Applied to Industrial-Scale Models
- Verification of MPI-Based Software for Scientific Computation
- Tutorials
- Advanced SPIN Tutorial
- IF Validation Environment Tutorial.