Verifying Invariants by Deductive Model Checking

Kyungmin Bae, Santiago Escobar, Raúl López-Rueda, José Meseguer, Julia Sapiña

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish (US)
Title of host publicationRewriting Logic and Its Applications - 15th International Workshop, WRLA 2024, Revised Selected Papers
EditorsKazuhiro Ogata, Narciso Martí-Oliet
PublisherSpringer
Pages3-21
Number of pages19
ISBN (Print)9783031659409
DOIs
StatePublished - 2024
Event15th International Workshop on Rewriting Logic and Its Applications, WRLA 2024 - Luxembourg City, Luxembourg
Duration: Apr 6 2024Apr 7 2024

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume14953 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference15th International Workshop on Rewriting Logic and Its Applications, WRLA 2024
Country/TerritoryLuxembourg
CityLuxembourg City
Period4/6/244/7/24

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'Verifying Invariants by Deductive Model Checking'. Together they form a unique fingerprint.

Cite this