TY - GEN
T1 - Verifying Invariants by Deductive Model Checking
AU - Bae, Kyungmin
AU - Escobar, Santiago
AU - López-Rueda, Raúl
AU - Meseguer, José
AU - Sapiña, Julia
N1 - Publisher Copyright:
© The Author(s), under exclusive license to Springer Nature Switzerland AG 2024.
PY - 2024
Y1 - 2024
N2 - We propose a new deductive model checking methodology where narrowing-based logical model checking of symbolic states specified as disjunctions of constrained patterns is synergistically combined with inductive theorem proving to discharge inductive verification conditions. An obvious synergy is to use an inductive theorem prover in automated mode as an oracle to help logical model checking reach a fixpoint. But this is not the only possible synergy. In this paper we focus instead on a new deductive model checking methodology to verify invariants—including inductive invariants—of infinite-state systems, where logical model checking automates large parts of the verification effort with the help of an inductive theorem prover as an oracle, and the remaining tasks are left to the inductive theorem prover used in interactive mode. We demonstrate this methodology by means of Maude examples using two tools working in tandem: the DM-Check symbolic model checker, and the NuITP inductive theorem prover.
AB - We propose a new deductive model checking methodology where narrowing-based logical model checking of symbolic states specified as disjunctions of constrained patterns is synergistically combined with inductive theorem proving to discharge inductive verification conditions. An obvious synergy is to use an inductive theorem prover in automated mode as an oracle to help logical model checking reach a fixpoint. But this is not the only possible synergy. In this paper we focus instead on a new deductive model checking methodology to verify invariants—including inductive invariants—of infinite-state systems, where logical model checking automates large parts of the verification effort with the help of an inductive theorem prover as an oracle, and the remaining tasks are left to the inductive theorem prover used in interactive mode. We demonstrate this methodology by means of Maude examples using two tools working in tandem: the DM-Check symbolic model checker, and the NuITP inductive theorem prover.
UR - http://www.scopus.com/inward/record.url?scp=85201096762&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85201096762&partnerID=8YFLogxK
U2 - 10.1007/978-3-031-65941-6_1
DO - 10.1007/978-3-031-65941-6_1
M3 - Conference contribution
AN - SCOPUS:85201096762
SN - 9783031659409
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 3
EP - 21
BT - Rewriting Logic and Its Applications - 15th International Workshop, WRLA 2024, Revised Selected Papers
A2 - Ogata, Kazuhiro
A2 - Martí-Oliet, Narciso
PB - Springer
T2 - 15th International Workshop on Rewriting Logic and Its Applications, WRLA 2024
Y2 - 6 April 2024 through 7 April 2024
ER -