CS576 - Fall 2021 - Topics in Automated Deduction

Course Information

Zoom Links for Lectures


Course Description

Symbolic Techniques for Deductive and Model Checking Verification

Symbolic techniques are crucial to scale up formal verification
of system properties.  This is because such techniques can automate
large portions of the verification process.  Such verification can
be either by model checking, where symbolic techniques allow verification
of infinite-state concurrent systems, or by theorem proving.  

The course will cover symbolic techniques that can be very useful
for these two types of formal verification, including:

1. Equality predicates as a formula simplification method.
2. Congruence closure and termination orders modulo axioms.
3. Ordered rewriting.
4. Contextual rewriting and inductive congruence closure.
5. Narrowing for both equational theories and rewrite theories.
6. Variants and variant unification.
7. Variant satisfiability as a theory-generic SMT solving technique.

After these symbolic techniques have been explained, their application
to both model checking and theorem proving verification will also
be discussed.  More specifically:

A.  Narrowing-based model checking verification of concurrent systems
    and the use of symbolic techniques for this purpose will be explained.

B.  Inductive theorem proving of deterministic system verification and
    the use of symbolic techniques for this purpose will likewise be explained.

Course  Organization and Requirements

Students taking the course will be expected to: (i) participate
actively in it; (ii) study and discuss recent research papers;
and (iii) develop a term project, possibly jointly with
other students in the course.  Evaluation will be based on (i)-(iii) above.

Course Reading Materials

Introductory paper on symbolic methods in Maude

Equationally-Defined Equality Predicates

Recursive Path Orderings (RPO) and RPO Modulo Axioms

Knuth-Bendix Completion, Congruence Closure, and Congruence Closure Modulo Axioms

Ordered Rewriting

Contextual Rewriting and Inductive Contextual Rewriting

Variants, Variant Unification, and Variant Satisfiability

Narrowing with a Rewrite Theory's Rules: Model Checking and Theorem Proving Applications

A Symbolic-Based Inductive Theorem Proving Inference System

Maude Web Page