Pre-requisites
CSCI.4430/6430 Programming Languages, or equivalent, or permission of instructor. Familiarity with formal operational semantics (for example, for the lambda calculus), first-order logic, and discrete math is expected. The student should also be comfortable with programming language concepts, in particular, with functional and concurrent (actor) programming.
Course Themes
Fundamental proof methods. Proving properties about data types and algorithms. Research topics in software verification. Abstract proofs and reuse. Proving correctness of concurrent (actor) programs.
Learning Outcomes
When the students have successfully completed this course, they will be able to:
| Date | Topic | Grade |
|---|---|---|
| 01/10 | Course overview. Introduction to Software Verification Part I -- Fundamental Proof Methods. Proof sample: eq-chaining.ath | |
| 01/13 | Fundamental proof methods: equality chaining, induction, case analysis, proof by contradiction, abstraction/specialization. Proof samples: induction.ath, cases.ath, contradiction.ath | |
| 01/17 | No lecture--Martin Luther King Jr. Day. | |
| 01/20 | Athena: domains and function symbols, terms, sentences, definitions, assumption bases, datatypes. | |
| 01/24 | Athena: polymorphism, meta-identifiers, expressions and deductions. Code samples: fact.ath, lists.ath. | |
| 01/27 | Proving equalities: numeric equations, equality chaining, terms and sentences as trees, mathematical induction. Proof samples: equalities.ath Proof Assignment 1 Due 02/09 |
10% |
| 01/31 | Proving equalities: list equations, polymorphic datatypes, ground terms, top-down proof development. Proof samples: list-equalities.ath | |
| 02/01 | Sentential logic: conjunctions, conditionals, disjunctions, negations, biconditionals. Proof samples: sentential-logic.ath | |
| 02/07 | Sentential logic: recursive proof methods, proof heuristics. Proof samples: recursive-methods.ath | |
| 02/10 | First-order logic: universal quantifiers, existential quantifiers, proof heuristics. Proof samples: first-order-logic.ath, neither.ath | |
| 02/14 | Implication chaining: implication chains, sentences as justifiers. Proof samples: implication-chaining.ath | |
| 02/17 | Implication chaining: chain-last, chain-first, equivalence chains, chain nesting. | |
| 02/21 | No lecture--President's Day. | |
| 02/22 | Part I Review | |
| 02/24 | Exam 1 | 20% |
| 02/28 | A correctness proof for a toy compiler. Proof: toy-compiler.ath | |
| 03/03 | Exam 1 Review. Introduction to Software Verification Part II -- Proofs about Fundamental Data Types and Algorithms. Athena modules for theory development. Proof samples: modules.ath | |
| 03/14 | Natural number orderings: transitive, irreflexive, and assymetric properties; trichotomy properties; less-equal properties; ordering and arithmetic. Proof samples: nat-ordering.ath | |
| 03/17 | Natural number substraction. Ordered lists. Binary search trees. Proof Assignment 2 Due 03/30. Proof samples: nat-subtraction.ath, ordered-lists.ath, binary-search-trees.ath |
10% |
| 03/21 | Fundamental discrete structures: ordered pairs, options, sets, relations, functions. Proof samples: sets-relations-functions.ath | |
| 03/24 | Fundamental discrete structures: maps operations and theorems. | |
| 03/28 | Fundamental discrete structures: default maps. Proof samples: maps.ath | |
| 03/31 | Binary search: algorithm definition, correctness properties, correctness of an optimized algorithm. Proof samples: binary-search.ath | |
| 04/04 | Fast exponentiation: algorithm definition, strong induction, properties of half, odd/even, power, fast-power, from strong to ordinary induction. Proof samples: fast-power.ath | |
| 04/07 | A correctness proof for a toy compiler: error handling. Proof: toy-compiler-error-handling.ath | |
| 04/11 | Part II Review | |
| 04/14 | Exam 2 | 20% |
| 04/18 | Introduction to Software Verification Part III -- Research Topics. Selected Paper Critiques and Presentations by Students -- Papers Selections Due 03/03 | 10% |
| 04/21 | ||
| 04/25 | Final Project/Paper Presentations-- Proposals Due 03/29 | 30% |
| Class Participation Extra Credit | 10% |
Please contact the instructor if there is any question about academic
(dis)honesty.