Pre-requisites
CSCI.4430/6430 Programming Languages, or equivalent, or permission of instructor. Familiarity with formal operational semantics (for example, 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/16 | Course overview. Introduction to Software Verification Part I -- Fundamental Proof Methods. Proof sample: eq-chaining.ath | |
01/19 | Fundamental proof methods: equality chaining, induction, case analysis, proof by contradiction, abstraction/specialization. Proof samples: induction.ath, cases.ath | |
01/23 | Athena: domains and function symbols, terms, sentences, definitions, assumption bases, datatypes. Proof sample: contradiction.ath | |
01/26 | Athena: polymorphism, meta-identifiers, expressions and deductions. Code samples: fact.ath, lists.ath. | |
01/30 | Proving equalities: numeric equations, equality chaining, terms and sentences as trees, mathematical induction. Proof samples: equalities.ath Proof Assignment 1 Due 02/12 |
10% |
02/02 | Proving equalities: list equations, polymorphic datatypes, ground terms, top-down proof development. Proof samples: list-equalities.ath | |
02/06 | Sentential logic: conjunctions, conditionals, disjunctions, negations, biconditionals. Proof samples: sentential-logic.ath | |
02/09 | Sentential logic: recursive proof methods, proof heuristics. Proof samples: recursive-methods.ath | |
02/13 | First-order logic: universal quantifiers, existential quantifiers, proof heuristics. Proof samples: first-order-logic.ath, neither.ath | |
02/16 | Implication chaining: implication chains, sentences as justifiers. Proof samples: implication-chaining.ath | |
02/20 | No lecture | |
02/23 | Implication chaining: chain-last, chain-first, equivalence chains, chain nesting | |
02/27 | Exam 1 | 20% |
03/02 | No lecture | |
03/06 | Exam1 Review. A correctness proof for a toy compiler. Proof: toy-compiler.ath | |
03/09 | Introduction to Software Verification Part II -- Proofs about Fundamental Data Types and Algorithms. Athena modules for theory development. Proof samples: modules.ath | |
03/20 | Natural number orderings: transitive, irreflexive, and asymmetric properties; trichotomy properties; less-equal properties; ordering and arithmetic. Proof samples: nat-ordering.ath | |
03/23 | Natural number substraction. Ordered lists. Binary search trees. Proof Assignment 2 Due 04/02. Proof samples: nat-subtraction.ath, ordered-lists.ath, binary-search-trees.ath |
10% |
03/27 | Fundamental discrete structures: ordered pairs, options, sets, relations. Proof samples: sets-relations-functions.ath | |
03/30 | Fundamental discrete structures: maps operations and theorems. Proof samples: maps.ath | |
04/03 | Fundamental discrete structures: default maps. | |
04/06 | Binary search: algorithm definition, correctness properties, correctness of an optimized algorithm. Proof samples: binary-search.ath | |
04/10 | A correctness proof for a toy compiler: error handling. Proof: toy-compiler-error-handling.ath | |
04/13 | Fast exponentiation: algorithm definition, strong induction, properties of half, odd/even, power, fast-power, tail recursion, from strong to ordinary induction. Proof samples: fast-power.ath | |
04/17 | Exam 2 | 20% |
04/20 | Introduction to Software Verification Part III -- Research Topics. Selected Paper Critiques and Presentations by Students -- Papers Selections Due 03/06 | 10% |
04/24 | ||
04/27 | Final Project/Paper Presentations-- Proposals Due 03/30 | 30% |
05/01 | No lecture | |
Class Participation Extra Credit | 10% |
Please contact the instructor if there is any question about academic
(dis)honesty.