Algorithmic Software Verification

Course Materials for Graduate Class on Algorithmic Software Verification

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
• ADD MORE HERE

List of Papers

• JS* (Swamy et al, PLDI 2013) NOTE: waiting for camera ready to be posted here
• Separation Logic and Abstraction (Parkinson and Bierman, POPL 2005)
• Abduction (Dilligs and Aiken, PLDI 2012)
• Containers (Dilligs and Aiken, POPL 2011)
• RockSalt (Morrisett et al, PLDI 2012)
• BedRock (Chlipala, PLDI 2011)
• HMC (Jhala et al, CAV 2011)
• Dependent Types for ML (Zhu and Jagannathan, VMCAI 2013)
• Dafny (Leino) (more benchmarks)
• Termination (papers from Cook, et al) TODO: choose some from here
• Concurrency via Separation Logic (papers from Parkinson, Birkedal, et al) TODO: choose some from here
• Security (papers of Gordon, Fournet, Bhargavan, et al) TODO: choose some from here
• ADD MORE HERE

Requirements

1. Scribe one lecture maybe

2. Probably 2-3 assignments

   • implement some of the above

3. Present one lecture definitely

   • read 2-3 papers on the list above
   • synthesize
   • present