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 |
|---|---|---|
| 08/28 | Course overview. Introduction to Software Verification Part I -- Fundamental Proof Methods. Proof sample: eq-chaining.ath | |
| 09/04 | Fundamental proof methods: equality chaining, induction, case analysis, proof by contradiction, abstraction/specialization. Proof samples: induction.ath, cases.ath, contradiction.ath. | |
| 09/05 | Athena: domains and function symbols, terms, sentences, definitions, assumption bases, datatypes. | |
| 09/08 | Athena: polymorphism, meta-identifiers, expressions and deductions. Code samples: fact.ath, lists.ath. | |
| 09/11 | Proving equalities: numeric equations, equality chaining, terms and sentences as trees, mathematical induction. Proof samples: equalities.ath Proof Assignment 1 Due 09/24 |
10% |
| 09/15 | Proving equalities: list equations, polymorphic datatypes, ground terms, top-down proof development. Proof samples: list-equalities.ath | |
| 09/18 | Sentential logic: conjunctions, conditionals, disjunctions, negations, biconditionals. Proof samples: sentential-logic.ath | |
| 09/22 | Sentential logic: recursive proof methods, proof heuristics. Proof samples: recursive-methods.ath | |
| 09/25 | First-order logic: universal quantifiers, existential quantifiers, proof heuristics. Proof samples: first-order-logic.ath, neither.ath | |
| 09/29 | Implication chaining: implication chains, sentences as justifiers. Proof samples: implication-chaining.ath | |
| 10/02 | Implication chaining: chain-last, chain-first, equivalence chains, chain nesting. | |
| 10/06 | Part I Review | |
| 10/09 | Exam 1 | 20% |
| 10/16 | Exam 1 Review. A correctness proof for a toy compiler. Proof: toy-compiler.ath | |
| 10/20 | Introduction to Software Verification Part II -- Proofs about Fundamental Data Types and Algorithms. Athena modules for theory development. Proof samples: modules.ath | |
| 10/23 | Natural number orderings: transitive, irreflexive, and asymmetric properties; trichotomy properties; less-equal properties; ordering and arithmetic. Natural number substraction. Proof samples: nat-ordering.ath, nat-subtraction.ath | |
| 10/27 | Ordered lists. Binary search trees. Proof Assignment 2 Due 11/07. Proof samples: ordered-lists.ath, binary-search-trees.ath |
10% |
| 10/30 | Fundamental discrete structures: ordered pairs, options, sets. Proof samples: sets.ath | |
| 11/03 | Fundamental discrete structures: relations, functions. Proof samples: relations-functions.ath | |
| 11/06 | Fundamental discrete structures: maps operations and theorems, default maps. Proof samples: maps.ath | |
| 11/10 | Binary search: algorithm definition, correctness properties, correctness of an optimized algorithm. Proof samples: binary-search.ath | |
| 11/13 | Fast exponentiation: algorithm definition, strong induction, properties of half, odd/even, power, fast-power, from strong to ordinary induction. Proof samples: fast-power.ath | |
| 11/17 | A correctness proof for a toy compiler: error handling. Proof: toy-compiler-error-handling.ath | |
| 11/20 | Part II Review | |
| 12/01 | Exam 2 | 20% |
| 12/04 | Introduction to Software Verification Part III -- Research Topics. Selected Paper Critiques and Presentations by Students -- Papers Selections Due 10/20 | 10% |
| 12/08 | ||
| 12/11 | Final Project/Paper Presentations-- Proposals Due 11/11 | 30% |
| Class Participation Extra Credit | 5% |
The Rensselaer Handbook of Student Rights and Responsibilities defines several types of academic dishonesty, all of which are applicable to this class. Students found in violation of academic integrity policies will receive a failing grade for this course. Please contact me if there is any question about academic integrity.
At RPI, we care about you, and we are committed to your well-being,
both as a student and as an individual. College is a time of growth,
and it's natural to face challenges along the way. Stress,
relationship issues, low motivation, or mental health concerns can all
affect your experience.
If you're struggling, please know that asking for help is a smart and
courageous step. It's a skill that will serve you well far beyond your
time here. Rensselaer's Health and Counseling Services offers free,
confidential support. Visit http://studenthealth.rpi.edu
or call 518-276-8888 anytime. In an emergency, call 988 or Public
Safety at 518-276-6611.
If you're facing challenges this semester, I hope you'll feel
comfortable reaching out. I care about your success, and I want to
work with you to find the support and flexibility you may need.