Automatic proof-search heuristics in the maude invariant analyzer tool

  • Camilo Rocha Assistant Professor at Escuela Colombiana de Ingeniería Julio Garavito.

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/index.php/rcc/article/view/2017

Descargas

La descarga de datos todavía no está disponible.
Publicado
2013-12-01
Sección
Artículo de investigación científica y tecnológica