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.
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
Lectures