Catálogo de publicaciones - libros
Título de Acceso Abierto
Foundations of Software Science and Computation Structures: Foundations of Software Science and Computation Structures
Parte de: Theoretical Computer Science and General Issues
En conferencia: 21º International Conference on Foundations of Software Science and Computation Structures (FoSSaCS) . Thessaloniki, Greece . April 16, 2018 - April 19, 2018
Resumen/Descripción – provisto por la editorial
No disponible.
Palabras clave – provistas por la editorial
artificial intelligence; computer software; selection and evaluation; formal logic; graph theory; modal logic; petri nets; program compilers; programming language; semantics; separation logic; software engineering; theorem proving; type systems; verification
Disponibilidad
| Institución detectada | Año de publicación | Navegá | Descargá | Solicitá |
|---|---|---|---|---|
| No requiere | 2018 | Directory of Open access Books |
| |
| No requiere | 2018 | SpringerLink |
|
Información
Tipo de recurso:
libros
ISBN impreso
978-3-319-89365-5
ISBN electrónico
978-3-319-89366-2
Editor responsable
Springer Nature
País de edición
Reino Unido
Fecha de publicación
2018
Cobertura temática
Tabla de contenidos
Verifying Higher-Order Functions with Tree Automata
Thomas Genet; Timothée Haudebourg; Thomas Jensen
This paper describes a fully automatic technique for verifying safety properties of higher-order functional programs. Tree automata are used to represent sets of reachable states and functional programs are modeled using term rewriting systems. From a tree automaton representing the initial state, a completion algorithm iteratively computes an automaton which over-approximates the output set of the program to verify. We identify a subclass of higher-order functional programs for which the completion is guaranteed to terminate. Precision and termination are obtained conjointly by a careful choice of equations between terms. The verification objective can be used to generate sets of equations automatically. Our experiments show that tree automata are sufficiently expressive to prove intricate safety properties and sufficiently simple for the verification result to be certified in Coq.
- Graphs and Automata | Pp. 565-582