Date |
Topics, slides, code, other material |
Readings |
| 4 Sep 2019 |
- Introductions; Software science; Slides
|
|
| 5 Sep 2019 |
- Introduction and motivation continued; Class web pages; Programming review; Intro to ACL2s;
Slides
|
Start reading lecture notes, Chapters 1 and 2
|
| 9 Sep 2019 |
- Invariants; Contracts;
Slides
|
Read lecture notes, up to the end of section 2.6
|
| 11 Sep 2019 |
- The ACL2s Universe; Expressions; Syntax and Semantics;
Slides
|
Read lecture notes, up to the end of section 2.8
|
| 12 Sep 2019 |
- Conses; Lists; True lists;
Slides
|
Read lecture notes, up to the end of section 2.8
|
| 16 Sep 2019 |
- A function that rotates lists; quote; let and let*;
Slides: 06-acl2s-rl-quote-let.pdf;
Code: 06-acl2s.lisp
|
Read lecture notes, up to the end of section 2.11
|
| 18 Sep 2019 |
- Data definitions;
Code: 07-defdata.lisp
|
Read lecture notes, up to the end of Chapter 2
|
| 19 Sep 2019 |
- Property-based testing;
Slides: 08-property-testing.pdf;
|
Finish Chapter 2 of the lecture notes.
Start reading Chapter 3.
|
| 23 Sep 2019 |
- Property-based testing continued;
Slides: 09-property-testing.pdf;
|
Start reading Chapter 3 of the lecture notes.
|
| 25 Sep 2019 |
- Propositional logic: A brief history of logic;
Syntax and Semantics of PL; Truth tables;
Satisfiability and validity;
Slides: 10-propositional-logic.pdf;
|
Chapter 3 of the lecture notes, up to and including Section 3.6.
|
| 26 Sep 2019 |
- Propositional logic continued: The SAT problem; P vs NP;
SAT solvers; The power of XOR;
Slides: 11-sat-xor.pdf;
|
Read to the end of Chapter 3 of the lecture notes.
Highly recommended:
"Boolean Satisfiability" by Malik and Zhang
|
| 30 Sep 2019 |
- Propositional logic continued:
CNF and DNF; Complete Boolean bases;
Slides: 12-cnf-dnf.pdf;
|
Read the entire Chapter 3 of the lecture notes.
|
| 2 Oct 2019 |
- Boolean formula simplification; Equational proofs;
Slides: 13-simplification.pdf;
|
Read the entire Chapter 3 of the lecture notes.
Start reading Chapter 4 of the lecture notes.
|
| 3 Oct 2019 |
- Introduction to equational reasoning; Lemmas; Axioms; Equality;
Slides: 14-equational-reasoning.pdf;
|
Read Chapter 4 of the lecture notes up to 4.1.
|
| 7 Oct 2019 |
- Definitional axioms; Instantiation; Substitutions; Proof structure; Context; Examples;
Slides: 15-definitional-axiom.pdf;
|
Read Chapter 4 of the lecture notes up to 4.4.
|
| 9 Oct 2019 |
- Propositional skeleton; Exportation; More examples;
Slides: 16-exportation.pdf;
|
Read Chapter 4 of the lecture notes.
|
| 10 Oct 2019 |
- The automated proof checker; More proofs;
Slides: 17-more-proofs.pdf;
Code: 17-example3-proofchecker.lisp;
|
Read the entire Chapter 4 of the lecture notes.
|
| 16 Oct 2019 |
- More equational reasoning examples; More proof strategies; The del example and subtleties;
Slides: 18-context-theorems.pdf;
|
|
| 17 Oct 2019 |
- Review of topics for Exam 1;
|
|
| 21 Oct 2019 |
- The definitional principle;
Slides: 20-definitional-principle.pdf;
|
Read Chapter 5 of the lecture notes.
|
| 23 Oct 2019 |
- The hardness of proving theorems; The hardness of proving termination; Measure functions;
Slides: 21-measure-functions.pdf;
|
Read Chapter 5 of the lecture notes.
|
| 24 Oct 2019 |
- Measure functions: more examples and proof obligations;
Slides: 22-measure-functions.pdf;
|
Read the entire Chapter 5 of the lecture notes.
|
| 28 Oct 2019 |
- Guest lecture by Prof. Pete Manolios;
Slides;
C code;
ACL2s code;
|
|
| 30 Oct 2019 |
- Measure functions: more examples and proof obligations;
Alan Turing; Undecidability; Complexity vs Termination;
Slides: 24-undecidability.pdf;
|
A simple way to explain undecidability (proudly rejected by arxiv.org).
|
| 31 Oct 2019 |
- Induction;
Slides: 25-induction.pdf;
|
Read Chapter 6 of the lecture notes.
|
| 4 Nov 2019 |
- Induction;
Slides: 26-induction.pdf;
|
Read Chapter 6 of the lecture notes.
|
| 6 Nov 2019 |
- Induction;
Slides: 27-induction.pdf;
|
Read Chapter 6 of the lecture notes.
|
| 7 Nov 2019 |
- Induction;
Slides: 28-induction.pdf;
|
Read Chapter 6 of the lecture notes.
|
| 13 Nov 2019 |
- Induction;
Slides: 29-induction.pdf;
|
Read Chapter 6 of the lecture notes.
|
| 14 Nov 2019 |
- Reasoning about accumulators and tail recursion;
Slides: 30-accumulators.pdf;
|
|
| 18 Nov 2019 |
- Reasoning about accumulators and tail recursion;
Slides: 31-accumulators.pdf;
|
|
| 20 Nov 2019 |
- Reasoning about accumulators and tail recursion;
Code: 32-accumulators.lisp;
|
|
| 21 Nov 2019 |
- Test on Chapters 5 and 6! Note room: SN 108
Practice: the complete isort ordered proof.
|
|
| 25 Nov 2019 |
- Reasoning about imperative code; The invariant game;
Slides: 34-invariants.pdf;
|
|
| 2 Dec 2019 |
- Abstract data types and observational equivalence;
Code: 35-stacks.lisp;
|
|
| 4 Dec 2019 |
- In-class test on tail-recursion! Note room: WVF 020;
Parting thoughts:
Slides: 36-bye.pdf;
|
|