We propose a new deductive model checking methodology where narrowing-based logical model checking of symbolic states specified as disjunctions of constrained patterns is combined with inductive theorem proving to discharge inductive verification conditions that ensure useful symbolic state space reductions. An obvious combination 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 combination. 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 . Inductive verification conditions not discharged automatically by the oracle are dealt with by commands that refine some constrained patterns by useful semantic equivalences, and by using an inductive theorem prover in interactive mode. This methodology is demonstrated by means of concurrent system examples using two Maude tools working in tandem: the DM-Check narrowing-based symbolic model checker, and the NuITP inductive theorem prover.

Folding Narrowing is a symbolic analysis technique used in various areas of computer science. Maude-NPA has already demonstrated the effectiveness and potential of this technique in protocol analysis, particularly in the cryptographic domain. However, a thorough investigation into how protocols should be specified to make folding narrowing effective has not yet been conducted. The key to enabling this technique lies in ensuring the finiteness of the search space, which requires the search graph to collapse onto itself. Achieving this demands a careful design of the sorts and rules of the specified system. In many cases, such a design even allows for proving properties without relying on lemmas that other techniques typically require. In this work, we show how to prove the mutex property for the Test-and-Set (TAS), Qlock, and Anderson protocols, providing a detailed explanation of the reasoning needed to ensure the folding of the search space—without the use of lemmas.

Narrowing and unification are very useful tools for symbolic analysis of rewrite theories, and thus for any model that can be specified in that way. A very clear example of their application is the field of formal cryptographic protocol analysis, which is why narrowing and unification are used in tools such as Maude-NPA, Tamarin and Akiss. In this work we present the implementation of a canonical narrowing algorithm, which improves the standard narrowing algorithm, extended to be able to process rewrite theories with conditional rules. The conditions of the rules will contain SMT constraints, which will be carried throughout the execution of the algorithm to determine if the solutions have associated satisfiable or unsatisfiable constraints, and in the latter case, discard them.