Catálogo de publicaciones - libros
Model Checking Software: 14th International SPIN Workshop, Berlin, Germany, July 1-3, 2007. Proceedings
Dragan Bošnački ; Stefan Edelkamp (eds.)
En conferencia: 14º International SPIN Workshop on Model Checking of Software (SPIN) . Berlin, Germany . July 1, 2007 - July 3, 2007
Resumen/Descripción – provisto por la editorial
No disponible.
Palabras clave – provistas por la editorial
No disponibles.
Disponibilidad
| Institución detectada | Año de publicación | Navegá | Descargá | Solicitá |
|---|---|---|---|---|
| No detectada | 2007 | SpringerLink |
Información
Tipo de recurso:
libros
ISBN impreso
978-3-540-73369-0
ISBN electrónico
978-3-540-73370-6
Editor responsable
Springer Nature
País de edición
Reino Unido
Fecha de publicación
2007
Información sobre derechos de publicación
© Springer-Verlag Berlin Heidelberg 2007
Cobertura temática
Tabla de contenidos
Instrumenting C Programs with Nested Word Monitors
Swarat Chaudhuri; Rajeev Alur
In classical automata-theoretic model checking of safety properties [6], a system model generates a language of words modeling system executions, and verification involves checking if ∩ ′ = ∅, ′ being the language of words deemed “unsafe” by the specification. This view is also used in recent program analyzers like [5] and [2], where a specification is a word automaton (or monitor) with finite-state control-flow that accepts all “unsafe” program executions. Typical analysis constructs the “product” of a program and a monitor, in effect the program with extra commands and assertions, so that the input program fails its specification if and only if the product program fails an assertion. The latter is then checked for possible assertion failures. Monitors also find use in testing and runtime verification, where we try finding assertion violations in the product program at runtime.
Pp. 279-283