Automatic proof-search heuristics in the Maude invariant analyzer tool
Capítulo - Parte de Libro
2013
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
![Buscar en Repositorio UMECIT Buscar en Repositorio UMECIT](/themes/Mirage2/images/search.png)
concurrency control
![Buscar en Repositorio UMECIT Buscar en Repositorio UMECIT](/themes/Mirage2/images/search.png)
human computer interaction
![Buscar en Repositorio UMECIT Buscar en Repositorio UMECIT](/themes/Mirage2/images/search.png)
inference mechanisms
![Buscar en Repositorio UMECIT Buscar en Repositorio UMECIT](/themes/Mirage2/images/search.png)
interactive systems
![Buscar en Repositorio UMECIT Buscar en Repositorio UMECIT](/themes/Mirage2/images/search.png)
program verification
![Buscar en Repositorio UMECIT Buscar en Repositorio UMECIT](/themes/Mirage2/images/search.png)
rewriting systems
![Buscar en Repositorio UMECIT Buscar en Repositorio UMECIT](/themes/Mirage2/images/search.png)
theorem proving
![Buscar en Repositorio UMECIT Buscar en Repositorio UMECIT](/themes/Mirage2/images/search.png)
Modelos matemáticos
![Buscar en Repositorio UMECIT Buscar en Repositorio UMECIT](/themes/Mirage2/images/search.png)
Modelado orientado a objetos
![Buscar en Repositorio UMECIT Buscar en Repositorio UMECIT](/themes/Mirage2/images/search.png)
Sistemas interactivos (computadores)
![Buscar en Repositorio UMECIT Buscar en Repositorio UMECIT](/themes/Mirage2/images/search.png)
Sistemas de reescritura
![Buscar en Repositorio UMECIT Buscar en Repositorio UMECIT](/themes/Mirage2/images/search.png)
Maude Invariant Analyzer
![Buscar en Repositorio UMECIT Buscar en Repositorio UMECIT](/themes/Mirage2/images/search.png)
SMT
![Buscar en Repositorio UMECIT Buscar en Repositorio UMECIT](/themes/Mirage2/images/search.png)
Safety
![Buscar en Repositorio UMECIT Buscar en Repositorio UMECIT](/themes/Mirage2/images/search.png)
Equations
![Buscar en Repositorio UMECIT Buscar en Repositorio UMECIT](/themes/Mirage2/images/search.png)
Mathematical model
![Buscar en Repositorio UMECIT Buscar en Repositorio UMECIT](/themes/Mirage2/images/search.png)
Cognition
![Buscar en Repositorio UMECIT Buscar en Repositorio UMECIT](/themes/Mirage2/images/search.png)
Algebra
![Buscar en Repositorio UMECIT Buscar en Repositorio UMECIT](/themes/Mirage2/images/search.png)
Discharges (electric)
![Buscar en Repositorio UMECIT Buscar en Repositorio UMECIT](/themes/Mirage2/images/search.png)
Object oriented modeling
![Buscar en Repositorio UMECIT Buscar en Repositorio UMECIT](/themes/Mirage2/images/search.png)
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. La herramienta Invariant Analyzer es una herramienta interactiva que mecaniza un sistema de inferencia para probar las propiedades de seguridad de sistemas concurrentes, que pueden ser de estado infinito o cuyo conjunto de estados iniciales puede ser infinito. Este documento presenta las heurísticas de búsqueda automática de pruebas en el núcleo de la herramienta Maude Invariant Analyzer, que proporciona un grado sustancial de automatización y puede cumplir automáticamente muchas obligaciones de prueba sin la intervención del usuario. Estas heurísticas pueden aprovechar los predicados de igualdad definidos ecuacionalmente e incluyen técnicas de reescritura, estrechamiento y búsqueda de pruebas basadas en SMT.
9781479910564
Descripción:
Capítulo - Parte de Libro
Título: Automatic proof-search heuristics in the Maude invariant analyzer tool.pdf
Tamaño: 506.3Kb
PDF
Título: Automatic proof-search heuristics in the Maude invariant analyzer tool.pdf
Tamaño: 506.3Kb
![Unicordoba Logo](/themes/Mirage2/images/pdf-logo.png)
![Closed Access](/themes/Mirage2/images/closedaccess.png)