Skip to content

Course Materials for Graduate Class on Algorithmic Software Verification

Notifications You must be signed in to change notification settings

UCSD-PL/algorithmic-software-verification

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

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

Project Presentations

May 30

  • Vazou & Vekris : Abduction
  • Zohour & Mouradian & Ellis : Terminator/Eurosys

June 4

  • Ptival & Seidel : AGDA
  • Tatlock & Bakst : Separation Logic + Bedrock

June 6

  • Leung & Jang : Containers
  • Wood & Bounov : Concurrency/Separation Logic

Jun 11 (Final SLOT) or May 28

  1. Chugh : DJS + J-Star

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

  1. Type Systems [2]

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

  3. Refinement Types [2]

    • Refinement Type Checking
    • Subtyping + Implication + VCGEN
  4. Abstract Refinement Types

HW 2

Algorithmic Verification

  1. Horn Clauses (HMC) & Abstract Interpretation

  2. AI: Theory

    • Intervals/Octagons/Polyhedra
  3. Predicate Abstraction (Liquid Types)

    • Interpolation ?

HW 3

Reasoning About the Heap

  1. Separation Logic

  2. Heap + Higher Order [HTT/Triple]

Reasoning About Untyped Languages

  1. Nested Refinement Types

  2. 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:

  • 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

About

Course Materials for Graduate Class on Algorithmic Software Verification

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published