TY - GEN
T1 - Automatic proof-search heuristics in the Maude invariant analyzer tool
AU - Rocha, Camilo
PY - 2013
Y1 - 2013
N2 - 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.
AB - 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.
KW - Maude Invariant Analyzer
KW - Software engineering
KW - human-computer interaction
KW - narrowing
KW - proof-search heuristics
KW - rewriting
KW - rewriting logic
KW - satisfiability modulo theories (SMT)
UR - http://www.scopus.com/inward/record.url?scp=84890825039&partnerID=8YFLogxK
U2 - 10.1109/ColombianCC.2013.6637512
DO - 10.1109/ColombianCC.2013.6637512
M3 - Conference contribution
AN - SCOPUS:84890825039
SN - 9781479910564
T3 - 2013 8th Computing Colombian Conference, 8CCC 2013
BT - 2013 8th Computing Colombian Conference, 8CCC 2013
PB - IEEE Computer Society
T2 - 2013 8th Computing Colombian Conference, 8CCC 2013
Y2 - 21 August 2013 through 23 August 2013
ER -