Automatic proof-search heuristics in the maude invariant analyzer tool

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...

Full description

Bibliographic Details
Main Author: Camilo Rocha
Format: Article
Language:English
Published: Universidad Autónoma de Bucaramanga 2013-12-01
Series:Revista Colombiana de Computación
Online Access:https://revistas.unab.edu.co/index.php/rcc/article/view/2017
id doaj-7deaf2f2b9b3480aacad2f6dd17c0472
record_format Article
spelling doaj-7deaf2f2b9b3480aacad2f6dd17c04722020-11-25T03:33:17ZengUniversidad Autónoma de BucaramangaRevista Colombiana de Computación1657-28312539-21152013-12-01142Automatic proof-search heuristics in the maude invariant analyzer toolCamilo Rocha0Assistant Professor at Escuela Colombiana de Ingeniería Julio Garavito.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.https://revistas.unab.edu.co/index.php/rcc/article/view/2017
collection DOAJ
language English
format Article
sources DOAJ
author Camilo Rocha
spellingShingle Camilo Rocha
Automatic proof-search heuristics in the maude invariant analyzer tool
Revista Colombiana de Computación
author_facet Camilo Rocha
author_sort Camilo Rocha
title Automatic proof-search heuristics in the maude invariant analyzer tool
title_short Automatic proof-search heuristics in the maude invariant analyzer tool
title_full Automatic proof-search heuristics in the maude invariant analyzer tool
title_fullStr Automatic proof-search heuristics in the maude invariant analyzer tool
title_full_unstemmed Automatic proof-search heuristics in the maude invariant analyzer tool
title_sort automatic proof-search heuristics in the maude invariant analyzer tool
publisher Universidad Autónoma de Bucaramanga
series Revista Colombiana de Computación
issn 1657-2831
2539-2115
publishDate 2013-12-01
description 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.
url https://revistas.unab.edu.co/index.php/rcc/article/view/2017
work_keys_str_mv AT camilorocha automaticproofsearchheuristicsinthemaudeinvariantanalyzertool
_version_ 1724563494589693952

Similar Items