Automatic proof-search heuristics in the maude invariant analyzer tool
Resumen
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.Cómo citar
Rocha, C. (2013). Automatic proof-search heuristics in the maude invariant analyzer tool. Revista Colombiana De Computación, 14(2), 98–121. Recuperado a partir de https://revistas.unab.edu.co/rcc/article/view/2017
Descargas
Los datos de descargas todavía no están disponibles.
Descargas
Publicado
2013-12-01
Número
Sección
Artículo de investigación científica y tecnológica
Licencia
La publicación de un artículo en la Revista Colombiana de Computación, requiere la autorización por parte del autor, a través del formato de cesión de derechos, el cual autoriza al Editor de esta Revista, para la reproducción parcial o total, con fines académicos, no comerciales, ni lucrativos, de acuerdo a la filosofía Open Access en sitios Web y en Internet como en redes, bases de datos bibliográficas, índices, directorios o cualquier otro medio de reproducción electrónica, haciendo referencia siempre al autor(a) y a la revista en mención, de acuerdo a lo estipulado en la Licencia Creative Commons Atribución-NoComercial-CompartirIgual 4.0 Internacional.
Métricas
Escanea para compartir
| Estadísticas de artículo | |
|---|---|
| Vistas de resúmenes | 359 |
| Vistas de PDF | 289 |
| Descargas de PDF | 289 |
| Vistas de HTML | 0 |
| Otras vistas | 0 |
