- Instructor: Jose Mesegue
- Time: Tuesday/Thursday 3:30PM - 4:45PM
- Online Course (see Zoom links below)
- Location: Students on campus can use Siebel Center Room 1131 to attend the lectures if so desired.
- Office Hours: Right after lectures, or by appointment.
- contact email: cs576-staff@illinois.edu

**Zoom Links for Lectures**

**Tuesday Lectures:**https://illinois.zoom.us/j/86291410450?pwd=RjV5YW0rVUdMaEJrSGZXMFEySUJadz09**Thursday Lectures:**https://illinois.zoom.us/j/83901415066?pwd=TWVtMVJRR05PS1VoOXpMcGN3eFJsZz09

**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**

- CS 476, Lecture 9 (pages 1-9)
- F. Baader and T. Nipkow on RPO
- A. Rubio, A Fully Syntactic AC-RPO
- A. Rubio, Theorem Proving Modulo Associativity

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

- G. Huet, A Complete Proof of Correctness of the Knuth-Bendix Completion Algorithm (pages 11-13)
- D. Plaisted and A. Sattler-Klein, Proof Lengths for Equational Completion (pages 154-162)
- P. Narendran and M. Rusinovitch, Any ground associative-commutative theory has a finite canonical system
- J. Meseguer, Order-Sorted Rewriting and Congruence Closure

**Ordered Rewriting**

- J. Meseguer and S. Skeirik on Ordered Rewriting: Section 2.9 of IR paper

**Contextual Rewriting and Inductive Contextual Rewriting**

- H. Zhang, Contextual Rewriting in Automated Reasoning
- J. Meseguer and S. Skeirik on Inductive Contextual Rewriting: (Section 2.5, and ICC rule in pages 25-26) in IR paper

**Variants, Variant Unification, and Variant Satisfiability**

- H. Comon and S. Delaune, The Finite Variant Property: How to Get Rid of Some Algebraic Properties
- S. Escobar, R. Sasse, J. Meseguer, Folding variant narrowing and optimal variant termination
- J. Meseguer, Variant-based satisfiability in initial algebras
- S. Skeirik and J. Meseguer, Metalevel algorithms for variant satisfiability
- J. Meseguer, Variants and Satisfiability in the Infinitary UnificationWonderland

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

- Definition and MC Apps: J. Meseguer, Generalized rewrite theories, coherence completion, and symbolic methods
- Theorem Proving Apps: S. Skeirik, A. Stefanescu, J. Meseguer, A Constructor-Based Reachability Logic for Rewrite Theories
- Theorem Proving Apps: S. Skeirik, J. Meseguer, C. Rocha, Verification of the IBOS Browser Security Properties in Reachability Logic

**A Symbolic-Based Inductive Theorem Proving Inference System**

- (IR paper) J. Meseguer, S. Skeirik, Inductive Reasoning with Equality Predicates, Contextual Rewriting and Variant-Based Simplification

**Lectures**