Algorithmic Software Verification

Course Materials for Graduate Class on Algorithmic Software Verification

Requirements

1. Scribe one lecture

2. Program three assignments

   • implement some of the above algorithms
   • use verification tools

3. Present one 40 minute talk

   • read 1-3 papers from the list below
   • prepare slides and get vetted by me
   • synthesize and present

Plan

Deductive Verification

1. Decision Procedures/SMT [2]

   • EUIF

   • DIFF

   • DPLL

   • SMT

   • Proofs?

2. Contd.

3. Floyd-Hoare Logic [2]

   • SP/WP
   • VCGen
   • SSA (Flanagan-Saxe)

4. Contd.

HW 1

5. Type Systems [2]

   • Hindley Milner (?)
   • Local Type Inference/Bidirectional Checking
   • Subtyping

6. Contd.

7. Refinement Types [2]

   • Refinement Type Checking
   • Subtyping + Implication + VCGEN

8. Abstract Refinement Types

HW 2

Algorithmic Verification

9. Horn Clauses (HMC) & Abstract Interpretation

10. AI: Theory

    • Intervals/Octagons/Polyhedra

11. Predicate Abstraction (Liquid Types)

    • Interpolation ?

HW 3

Reasoning About the Heap

12. Separation Logic

13. Heap + Higher Order [HTT/Triple]

Reasoning About Untyped Languages

14. Nested Refinement Types

15. Heap + ... DJS

Project Lectures

List of Topics

• SAT/SMT
• Hoare Logic
• Types, Polymorphism, Subtyping
• Refinement Types
• Abstract Interpretation
• Horn Clauses/Fixpoint
• Liquid Types
• Heap & State
• Separation Logic
• Imperative Refinement Types
• Symbolic Model Checking, BDDs, Craig Interpolants
• ADD MORE HERE

List of Papers

• Separation Logic Peter O'Hearn, CAV 2008

• Termination (papers from Rybalchenko, et al) here

• Fancy First-Order Logics HAVOC STRAND

• JS* (Swamy et al, PLDI 2013)here

• Separation Logic and Objects (Parkinson and Bierman, POPL 2005)

• Abduction (Dilligs and Aiken, PLDI 2012)

• Containers (Dilligs and Aiken, POPL 2011)

• HTT + BedRock (Chlipala, PLDI 2011)

• Concurrency via Separation Logic (papers from Parkinson, Birkedal, et al) here

• Abstracting Abstract Machines: Van Horn & Might

• Quantitative Bounds: COSTA, RAML, SPEED

• Dependently Typed Languages:

  • ATS
  • Agda
  • Idris

• Concurrency [e.g. Mike Emmi's papers] via Sep Logic [e.g. Jagannathan, Parkinson]

• Security [papers of Gordon, Fournet, Bhargavan]

• RockSalt(Morrisett et al, PLDI 2012)

• Dependent Types for ML (Zhu and Jagannathan, VMCAI 2013)

• Dafny (Leino) (more benchmarks)

• Security (papers of Gordon, Fournet, Bhargavan, et al) here

• IC3 [Bradley]

• ADD MORE HERE

Homework Plan

HW 1 1a. VCG 1b. Use ESC/J

HW 2 2a. ConsGen = VCG+K for LoopInv via FIXPOINT 2b. Implement FIXPOINT (over liquid-fixpoint)

HW 3 3a. VCG for Refinement Type Checking 3b. Consgen = VCG+K for Liquid Type Inference via FIXPOINT HW 1:

• EUIF + DIFF
• VCG for TJS
• Use VeriFAST

HW 2:

• BiDir Type Checking for TJS
• Refinement Type VCGen for TJS
• Use LiquidHaskell

HW 3:

• ConsGen for TJS
• PA for Horn Clauses = Liquid Types for TJS

---

HW 1 <----------- HEREHEREHEREHERE

0. Wrap parser

1. Port small tests

   • int-incr
   • if-max
   • if-abs

2. Parse small functions : FilePath -> Com

3. VCGen :: Com -> Pred

4. valid :: Pred -> Bool [liquid-fixpoint wrapper for Pred]

5. Port big tests

   • while-array
   • while-binsearch
   • adpcmini.c

---

Lecture Links

SAT

Lintao Zhang

• SAT 1
• SAT 2