- Instructor: José Meseguer
- TA: Stephen Skeirik (use my netid
`skeirik2`

for email) - Time: Tuesday/Thursday 3:30PM - 4:45PM
- Location: Siebel Center Room 1131
- Office Hours: TBD
- Course Piazza Forum

- A Constructor-Based Reachability Logic for Rewrite Theories (CBRL)
- CS476 Lecture 2 Slides
- CS476 Lecture 3 Slides
- CS476 Lecture 9 Slides
- CS476 Lecture 4 Slides
- CS476 Lecture 5 Slides
- CS476 Lecture 7 Slides
- CS476 Lecture 14 Slides
- CS476 Lecture 15 Slides
- CS476 Lecture 16 Slides

In every lecture, we will discuss a particular topic (see the list below for a rough overview). For some lectures, there will be assigned reading materials. Unless otherwise specified, assigned readings should be completed BEFORE attending the given lecture.

The lecture overview list has the following format:

Date - Topic

Optional comment.

- First assigned reading
- Second assigned reading
- Etc…

Here is the command listing from `rltool-lib.maude`

in the tool archive.

```
sort @QFForm@ @QFCTerm@ @NeQFCTermSet@ @Term@ @TermSet@ @ReachFormEx@ @LabelReachFormEx@ .
subsort @QFCTerm@ < @NeQFCTermSet@ .
subsort @Term@ < @TermSet@ .
op ((_)) : @Bubble@ -> @Term@ [ctor] .
op _U_ : @TermSet@ @TermSet@ -> @TermSet@ [assoc comm ctor] .
op true : -> @QFForm@ [ctor] .
op (_)=(_) : @Bubble@ @Bubble@ -> @QFForm@ [ctor] .
op (_)=/=(_) : @Bubble@ @Bubble@ -> @QFForm@ [ctor] .
op _/\_ : @QFForm@ @QFForm@ -> @QFForm@ [prec 58 assoc comm ctor] .
op _\/_ : @QFForm@ @QFForm@ -> @QFForm@ [prec 59 assoc comm ctor] .
op (_)|_ : @Bubble@ @QFForm@ -> @QFCTerm@ [prec 60 ctor] .
op _\/_ : @NeQFCTermSet@ @NeQFCTermSet@ -> @NeQFCTermSet@ [prec 61 assoc comm ctor] .
op _=>_ : @NeQFCTermSet@ @NeQFCTermSet@ -> @ReachFormEx@ [prec 62 ctor] .
op _:_ : @Token@ @ReachFormEx@ -> @LabelReachFormEx@ [prec 63 ctor] .
sort MetaRLTLCommand .
--- module/var/backend setup
op select_. : @Token@ -> MetaRLTLCommand [ctor] .
op select-rls_. : @NeTokenList@ -> MetaRLTLCommand [ctor] .
op declare-vars_. : @TermSet@ -> MetaRLTLCommand [ctor] .
op use`tool_for_on_. : @Token@ @Token@ @Token@ -> MetaRLTLCommand [ctor] .
op use`tool_for_on_with_. : @Token@ @Token@ @Token@ @NeTokenList@ -> MetaRLTLCommand [ctor] .
--- goal/term state setup
op def-term-set_. : @NeQFCTermSet@ -> MetaRLTLCommand [ctor] .
op add-goal_. : @LabelReachFormEx@ -> MetaRLTLCommand [ctor] . --- add as goal and axiom
op add-goal!_. : @LabelReachFormEx@ -> MetaRLTLCommand [ctor] . --- add as goal
op add-axiom_. : @LabelReachFormEx@ -> MetaRLTLCommand [ctor] . --- add as axiom TODO: revisit this command
op inv_to_with_on_. : @Token@ Qid @TermSet@ @NeQFCTermSet@ -> MetaRLTLCommand [ctor] .
op inv_to_on_. : @Token@ Qid @NeQFCTermSet@ -> MetaRLTLCommand [ctor] .
--- finish setup
op start-proof`. : -> MetaRLTLCommand [ctor] .
--- proof manipulation
--- apply basic proof strategy
op auto_. : Nat -> MetaRLTLCommand [ctor] .
op auto*`. : -> MetaRLTLCommand [ctor] .
op auto`. : -> MetaRLTLCommand [ctor] .
--- delete unwanted goals
op focus_. : NeSet{Nat} -> MetaRLTLCommand [ctor] .
op focus_. : @Term@ -> MetaRLTLCommand [ctor] .
op focus_. : @QFCTerm@ -> MetaRLTLCommand [ctor] .
op focus_/_. : @QFCTerm@ @QFCTerm@ -> MetaRLTLCommand [ctor] .
--- change axioms used
op use-axioms_on_. : @NeTokenList@ Nat -> MetaRLTLCommand [ctor] . --- modify goal to use circularities
op use-axioms_._on_. : @NeTokenList@ @NeTokenList@ Nat -> MetaRLTLCommand [ctor] . --- modify goal to use axioms/circularities
--- do case analysis a variable
op case_on_by_. : Nat @Token@ @TermSet@ -> MetaRLTLCommand [ctor] .
op case_on_by_. : @Term@ @Token@ @TermSet@ -> MetaRLTLCommand [ctor] .
op case_on_by_. : @QFCTerm@ @Token@ @TermSet@ -> MetaRLTLCommand [ctor] .
--- split on a formula
op split_by_. : Nat @QFForm@ -> MetaRLTLCommand [ctor] .
op split_by_. : @Term@ @QFForm@ -> MetaRLTLCommand [ctor] .
op split_by_. : @QFCTerm@ @QFForm@ -> MetaRLTLCommand [ctor] .
op replace_by_. : Nat @QFForm@ -> MetaRLTLCommand [ctor] .
op replace_by_. : @Term@ @QFForm@ -> MetaRLTLCommand [ctor] .
op replace_by_. : @QFCTerm@ @QFForm@ -> MetaRLTLCommand [ctor] .
op split_by_and_. : Nat @QFForm@ @QFForm@ -> MetaRLTLCommand [ctor] .
op split_by_and_. : @Term@ @QFForm@ @QFForm@ -> MetaRLTLCommand [ctor] .
op split_by_and_. : @QFCTerm@ @QFForm@ @QFForm@ -> MetaRLTLCommand [ctor] .
--- try to close a set of goals with default strategy---but do nothing if this process fails
op try-finish_. : NeSet{Nat} -> MetaRLTLCommand [ctor] .
op try-finish_. : @QFCTerm@ -> MetaRLTLCommand [ctor] .
op try-finish_/_. : @QFCTerm@ @QFCTerm@ -> MetaRLTLCommand [ctor] .
--- try to subsume a goal by another
op subsume_by_. : Nat Nat -> MetaRLTLCommand [ctor] .
--- resume from a debugging output pause
op continue`. : -> MetaRLTLCommand [ctor] .
--- delete inactive goals
op delete-inactive`. : -> MetaRLTLCommand [ctor] .
--- output commands
op show-goal-table`. : -> MetaRLTLCommand [ctor] .
op show-goal-ids`. : -> MetaRLTLCommand [ctor] .
op show-all-goal-ids`. : -> MetaRLTLCommand [ctor] .
op show-goals_. : NeSet{Nat} -> MetaRLTLCommand [ctor] .
op show-goals`. : -> MetaRLTLCommand [ctor] .
op show-level_. : Nat -> MetaRLTLCommand [ctor] .
op show-levels`. : -> MetaRLTLCommand [ctor] .
op show-ancestors_generation_. : NeSet{Nat} Bound -> MetaRLTLCommand [ctor] .
op show-narrowings_. : Nat -> MetaRLTLCommand [ctor] .
op show-maude-cmd_on_. : @Token@ Nat -> MetaRLTLCommand [ctor] .
```

08/27 - Course Introduction

08/29 - CBRL Preliminaries

Readings cover material in CBRL Preliminaries upto and including Theorem 1 on pg. 7.

- Many-sorted/Order-sorted Signatures, Equational Theories, Maude Modules: pgs. 2-19 in CS476 Lecture 2 Slides
- Many-sorted/Order-sorted Algebras: pgs. 2-16 in CS 476 Lecture 3 Slides
- Term Algebras, Substitutions, Equations: pgs. 17-30 in CS476 Lecture 3 Slides
- Many-sorted/Order-sorted Homomorphisms: pgs. 2-9 in CS476 Lecture 9 Slides
- The Initiality Theorem (Theorem 1 in CBRL): pgs. 10-12 in CS476 Lecture 9 Slides

09/03 - CBRL Preliminaries

Readings cover material in CBRL Preliminaries upto middle of pg. 10 (excluding the defn. of rewrite theories).

- Term Rewriting, Equational Logic, Rewriting Modulo Axioms: all of CS476 Lecture 4 Slides
- Executability Conditions, Canonical Term Algebras, Sufficient Completeness: all of CS 476 Lecture 5 Slides
- Unification: pgs. 3-18 in CS476 Lecture 7 Slides

09/05 - CBRL Preliminaries

Readings cover material in CBRL Preliminaries upto end of pg. 11.

- Rewrite Theory and Examples: pgs. 5-37 of CS476 Lecture 14 Slides and pgs. 2-17 of CS476 Lecture 15 Slides
- Coherence of Rules w.r.t. Oriented Equations Modulo Axioms: pgs. 10-14 of CS476 Lecture 16 Slides

09/10 - CBRL Preliminaries

Since the reading for this lecture is quite dense, please complete the following exercise BEFORE the lecture:

In subsection

*Variants in a Nutshell*, several examples of variants are presented. Check that these examples are indeed variants according to the definition. Then, develop some other examples of variants for yourself using some other set of convergent equations of your choice.This lecture will provide additional examples and go into greater depth on the topcis: narrowing, variant narrowing, variant unification, and variant satisfiability of quantifier-free formulas.

- Variants: section
*Variants in a Nutshell*of CBRL on pg. 12 excluding*A Running Example*

- Variants: section
09/12 - Constrained Constructor Pattern Predicates

Readings from now on are based on a revised version of CBRL available for download now; please redownload if you have an older copy.

- Constrained Constructor Pattern Predicates - Section 3 of CBRL upto but excluding
*Parameterized Intersections*on pg. 17

- Constrained Constructor Pattern Predicates - Section 3 of CBRL upto but excluding
09/17 - Constrained Constructor Pattern Predicates/Reachability Logic

09/19 - Reachability Logic

- Specifying (Co-)Invariants/Relationship to other logics - From pg. 22, after Lemma 3 upto end of pg. 28 excluding Section 5 in CBRL

09/24 - Reachability Logic Inference System

- RL Inference System - Starting from Section 5 on pg. 28 upto but excluding Section 5.2 on pg. 37 in CBRL

09/26 - Reachability Logic Inference System & Examples

Note that we will cover the first assigned reading quickly since it was already assigned previously.

10/01 - Reachability Logic Tool Tutorial

No readings, but see tool download link. In the tool archive, there are two parital proofs or you to complete:

`tests/systems/bank-account.maude`

and`tests/systems/imp-mul.maude`

. They correspond to two rewrite systems:`systems/bank-account.maude`

and`systems/imp.maude`

. They both require either case or split commands.10/03 - Reachability Logic Tool Tutorial (Continued)

No readings.

10/08 - Reachability Logic Tool Tutorial (Continued) and Project Discussions

Please begin to consider if you would like to work on verifying the ABP or else verify simple programs in an imperative programming language like the one in the reading.

- Sections 4 and 5 on verifying the Alternating Bit Protocol (ABP) in this paper
- Chapter 5, also on verifying the ABP, in Camilo Rocha’s Thesis
- The programming language semantics specified in
`systems/imp.maude`

in the tool archive