CIS 905 Home Page

Foundations of Abstract Interpretation with Applications to Finite-state Verification

Spring 2001

Overview:

This course is offered to graduate students working on the Bandera project.  The purpose of the course is two-fold:

• Learn the basic definitions of abstract interpretation, how it is used to construct models, and the foundations of the abstraction facilities currently implemented in Bandera.  These concepts should include basic technical definitions that every Ph.D. student working on the project should know.

• Implement at least one new form of abstraction support in Bandera.

We want this course to be a "deliverables" oriented course.  That means that, in contrast to other "reading" courses, we want to make sure that we complete the course with a set of concrete artifacts that testify to specific progress made and concepts learned.

Each student will be expected to

• present around two lectures during the course

• carry out a specific set of duties related to prototype implementation

• collaborate on the construction of technical summaries containing basic abstract interpretation definitions and assessment of methods

Course objectives:

• Bandera Background
  • Construct a white paper describing the foundations and current implementation of the abstraction facilities of Bandera.
• Predicate Abstraction
  • Study recent papers on predicate abstraction
  • Build a prototype predicate abstraction system for Bandera (focusing on instance predicate abstraction).
• Three-value logic analysis (heap abstractions)
  • Study recent papers on three value logic
  • Play around with the publicly available tool
  • Write a short (< 10 pages) summary of how these techniques might be incorporated into Bandera
• Abstraction Refinement
  • Study recent papers on using counterexamples to refine abstractions (focusing on predicate abstraction)
  • Write a short (< 10 pages) summary of how these techniques might be incorporated into Bandera
• Foundational Definitions
  • Making a collection of the basic definitions of abstract interpretation as applied for model-checking that every incoming Ph.D. student working on the Bandera project should know.
• Modal Transition Systems
  • Read recent papers on modal transition systems
  • Write a short summary of how these techniques might be incorporated into Bandera.

Instructors:

• Matt Dwyer
• John Hatcliff
• Michael Huth

Resources:

• Foundational definitions
  • Abstract Interpretation: a Semantics-based Tool for Program Analysis (Sections 1,2) -- Neil D Jones and Flemming Nielson
  • Schmidt, D.A. Binary relations for abstraction and refinement (17 November). Technical Report 2000-3. Corrected version of the paper in Proc. Workshop on Refinement and Abstraction, Amagasaaki, Japan, Nov. 1999, Electronic Notes in Computer Science.
  • Abstract Interpretation and Partition Refinement for Model-checking -- Dennis Dams Ph.D. thesis
• Bandera abstraction documents
  • Staging Static Analyses Using Abstraction-based Program Specialization -- John Hatcliff, Matt Dwyer, Shawn Laubach
• Predicate abstraction
  • Boolean and Cartesian Abstractions for Model-checking C Programs -- Thomas Ball, Andreas Podelski, Sriram Rajamani (to appear at TACAS 2001)
  • Boolean Programs: A Model and Process for Software Analysis, Thomas Ball, Sriram K. Rajamani, MSR Technical Report 2000-14
• Three-valued logic
  • 2 popl papers
• Modal transition systems
  • Modal transition systems: a foundation for three-valued program analysis.  Michael Huth, Radha Jagadeesan, and David Schmidt.  Proceedings of ESOP 2001, LNCS 2028, April, 2001.
  • Abstraction-based model-checking using modal transition systems.  Patrice Godefroid, Michael Huth, and Radha Jagadeesan, March 2001,  (submitted for publication).

Homework and Projects:

• Project I: Abstract Interpreter (tar'ed gzip'ed directory)

Schedule:

• Week 1: Jan 7-13
• Week 2: Jan 14-20
• Week 3: Jan 21-27
  • Tuesday, Jan 23: Course Overview
  • Thursday, Jan 25: Basic definitions
    • Read Sections 1,2 of the Jones/Nielson paper listed above
• Week 4: Jan 28-Feb 3
  • Tuesday: Jones/Nielson paper
  • Thursday: Jones/Nielson paper
• Week 5: Feb 4-10
  • Tuesday: Schmidt paper & Hatcliff/Dwyer/Laubach paper (Sections 1,2)
  • Thursday: (continue above + SML implementation)
• Week 6: Feb 11-17
• Week 7: Feb 18-24
• Week 8: Feb 25-March 3
• Slides for Michael's talk on Modal Transition Systems