Automatic proof-search heuristics in the Maude invariant analyzer tool
The Invariant Analyzer Tool is an interactive tool that mechanizes an inference system for proving safety properties of concurrent systems, which may be infinite-state or whose set of initial states may be infinite. This paper presents the automatic proof-search heuristics at the core of the Maude I...
- Autores:
-
Rocha, Camilo
- Tipo de recurso:
- Part of book
- Fecha de publicación:
- 2013
- Institución:
- Escuela Colombiana de Ingeniería Julio Garavito
- Repositorio:
- Repositorio Institucional ECI
- Idioma:
- eng
- OAI Identifier:
- oai:repositorio.escuelaing.edu.co:001/1837
- Acceso en línea:
- https://repositorio.escuelaing.edu.co/handle/001/1837
- Palabra clave:
- computability
concurrency control
human computer interaction
inference mechanisms
interactive systems
program verification
rewriting systems
theorem proving
Modelos matemáticos
Modelado orientado a objetos
Sistemas interactivos (computadores)
Sistemas de reescritura
Maude Invariant Analyzer
SMT
Safety
Equations
Mathematical model
Cognition
Algebra
Discharges (electric)
Object oriented modeling
- Rights
- closedAccess
- License
- © Copyright 2021 IEEE
| Summary: | The Invariant Analyzer Tool is an interactive tool that mechanizes an inference system for proving safety properties of concurrent systems, which may be infinite-state or whose set of initial states may be infinite. This paper presents the automatic proof-search heuristics at the core of the Maude Invariant Analyzer Tool, which provide a substantial degree of automation and can automatically discharge many proof obligations without user intervention. These heuristics can take advantage of equationally defined equality predicates and include rewriting, narrowing, and SMT-based proof-search techniques. |
|---|