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

Instructor:  Carlos Varela
Office:  Lally 308, x6912
Office Hours:  Tuesdays and Fridays 12pm-12:50pm; or by appointment
Meeting Place:  Ricketts 208
Meeting Hours:  Tuesdays and Fridays 10am-11:50am
Home page:  http://www.cs.rpi.edu/academics/courses/spring18/sv/
RPI LMS Page

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, program analyses, 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
    8.

Tentative Course Syllabus

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%

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 Updated -- April 16th, 2018.