CSCI.6962/CSCI.4962 Software Verification -- Spring 2020

Instructor:  Carlos Varela
Office:  Lally 308, x6912
Office Hours:  Mondays and Thursdays 1pm-1:50pm; or by appointment
Meeting Place:  LOW 3051
Meeting Hours:  Mondays and Thursdays 2pm-3:50pm
Home pagehttp://www.cs.rpi.edu/academics/courses/spring20/sv/
Submitty Site


Course Description

This course will enable students to understand and apply software verification techniques with a particular emphasis on fundamental proof methods. The course will cover proof methods including implication chaining, applied to equational reasoning, sentential logic, and first-order logic. The course will also cover proofs about fundamental data types and algorithms. The course will use the Athena dual computation/deduction language, and the MIT Press book "Fundamental Proof Methods in Computer Science" by Konstantine Arkoudas and David Musser. Students will also review current research on software verification on topics of their interest, for example: model checking, symbolic testing, temporal logic, modal logics, formal programming language semantics, proof-carrying code, dependent types, and session types. Contingent on time availability, the course will study proofs at an abstract level for reusability and their application to proofs about concurrent actor programs.

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:


Course Contents

  1. Introduction to Proof Methods using Athena
  2. Fundamental Proof Methods
  3. Proofs about Fundamental Data Types
  4. Proofs about Algorithms
  5. Research Topics
  6. Proofs at an Abstract Level
  7. Proofs for Concurrent Programs

Tentative Course Syllabus

Date Topic Grade
01/13 Course overview. Introduction to Software Verification Part I -- Fundamental Proof Methods. Proof sample: eq-chaining.ath
01/16 Fundamental proof methods: equality chaining, induction, case analysis, proof by contradiction, abstraction/specialization. Proof samples: induction.ath, cases.ath, contradiction.ath
01/23 Athena: domains and function symbols, terms, sentences, definitions, assumption bases, datatypes.
01/27 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/03 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/10 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/18 Implication chaining: implication chains, sentences as justifiers. Proof samples: implication-chaining.ath
02/20 Implication chaining: chain-last, chain-first, equivalence chains, chain nesting.
02/24 Part I Review
02/27 Exam 1 20%
03/02 Exam1 Review. A correctness proof for a toy compiler. Proof: toy-compiler.ath
03/05 Introduction to Software Verification Part II -- Proofs about Fundamental Data Types and Algorithms. Athena modules for theory development. Proof samples: modules.ath
03/23 Natural number orderings: transitive, irreflexive, and asymmetric properties; trichotomy properties; less-equal properties; ordering and arithmetic. Proof samples: nat-ordering.ath
03/26 Natural number subtraction. Ordered lists. Binary search trees.
Proof Assignment 2 Due 04/08. Proof samples: nat-subtraction.ath, ordered-lists.ath, binary-search-trees.ath
10%
03/30 Fundamental discrete structures: ordered pairs, options, sets, relations. Proof samples: sets-relations-functions.ath
04/02 Fundamental discrete structures: maps operations and theorems. Proof samples: maps.ath
04/06 Fundamental discrete structures: default maps.
04/09 Binary search: algorithm definition, correctness properties, correctness of an optimized algorithm. Proof samples: binary-search.ath
04/13 Part II Review
04/16 Exam 2 20%
04/20 Introduction to Software Verification Part III -- Research Topics. Selected Paper Critiques and Presentations by Students -- Papers Selections Due 03/05 10%
04/23
04/27 Final Project/Paper Presentations-- Proposals Due 04/03 30%
Class Participation Extra Credit 10%

Reading Material -- Parts I and II


Research Papers -- Part III

Students will critique and present selected papers from recent journal and conference publications, including but not limited to: You may also search papers in Google Scholar, or ACM's Digital Library

Academic Integrity

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 dishonesty policies will receive a failing grade for this course.

Please contact the instructor if there is any question about academic (dis)honesty.


Last modified: Thu Apr 9 12:02:23 EDT 2020