TY - GEN
T1 - Guarded terms for rewriting modulo SMT
AU - Bae, Kyungmin
AU - Rocha, Camilo
N1 - Publisher Copyright:
© 2017, Springer International Publishing AG.
PY - 2017
Y1 - 2017
N2 - Rewriting modulo SMT is a novel symbolic technique to model and analyze infinite-state systems that interact with a nondeterministic environment. It seamlessly combines rewriting modulo equational theories, SMT solving, and model checking. One of the main challenges of this technique is to cope with the symbolic state-space explosion problem. This paper presents guarded terms, an approach to deal with this problem for rewriting modulo SMT. Guarded terms can encode many symbolic states into one by using SMT constraints as part of the term structure. This approach enables the reduction of the symbolic state space by limiting branching due to concurrent computation, and the complexity and size of constraints by distributing them in the term structure. A case study of an unbounded and symbolic priority queue illustrates the approach.
AB - Rewriting modulo SMT is a novel symbolic technique to model and analyze infinite-state systems that interact with a nondeterministic environment. It seamlessly combines rewriting modulo equational theories, SMT solving, and model checking. One of the main challenges of this technique is to cope with the symbolic state-space explosion problem. This paper presents guarded terms, an approach to deal with this problem for rewriting modulo SMT. Guarded terms can encode many symbolic states into one by using SMT constraints as part of the term structure. This approach enables the reduction of the symbolic state space by limiting branching due to concurrent computation, and the complexity and size of constraints by distributing them in the term structure. A case study of an unbounded and symbolic priority queue illustrates the approach.
UR - http://www.scopus.com/inward/record.url?scp=85030686813&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-68034-7_5
DO - 10.1007/978-3-319-68034-7_5
M3 - Conference contribution
AN - SCOPUS:85030686813
SN - 9783319680330
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 78
EP - 97
BT - Formal Aspects of Component Software - 14th International Conference, FACS 2017, Proceedings
A2 - Lumpe, Markus
A2 - Proenca, Jose
PB - Springer Verlag
T2 - 14th International Conference on Formal Aspects of Component Software, FACS 2017
Y2 - 10 October 2017 through 13 October 2017
ER -