CSE 637: Program Semantics and Verification


Instructor: Radu Grosu ( grosu@cs.sunysb.edu),

Class: Tue/Thu  11:20am - 12:40pm, CS 1441

Office hours: Tue/Thu 4-5pm, CS Building room 1425, and by appointment


Reactive software systems are becoming an integral part of nearly every engineered product: they control consumer products, commercial aircraft, nuclear power plants, medical devices, weapon systems, aerospace systems, automobiles, public transportation systems, and so on.  At the same time quality and confidence issues are increasing in importance. Errors may result in loss of life, destruction of property, failure of businesses, and environmental harm.  Today, designers check that a reactive software system works properly by using simulation and testing. However, as reactive systems become more complex and pervasive, these traditional techniques are not sufficient to assure desired reliability. Abstract interpretation, model checking and related computer-aided verification techniques are emerging as practical alternatives. They allow the designer to verify that a software system satisfies its abstract logical specification. This approach has been most effective for control-intensive components, and is rapidly becoming an integral part of the design cycle in many embedded software companies.


The participants will learn how to model a reactive (hardware or software) sytem, express desired properties of the reactive system and check that the system satisfies these properties. They will get familiar with  the algorithmic methods used for this check.


The course requires basic knowledge of algorithms, data structures, automata theory, computational complexity, and propositional logic. Knowledge of operating systems, communication protocols, and hardware is useful. The course requires mathematical maturity, and is appropriate for graduate students who wish to pursue research in formal methods or related areas. If you need more information to decide, contact the instructor.


The course introduces the operational semantics of reactive software systems as a fundamental instrument in developoing tools and techniques  for the automated verification of temporal (logic) properties of software systems.

The emphasis is on the underlying logical and automata-theoretic concepts, the algorithmic solutions, and heuristics to cope with the high computational complexity. Topics include


We will look at various tools including:


The course will use a selection of papers considered to be among the most relevant in this area.


There will be no exams.

There will be periodic homework assignments and a class project. The project can be done in groups of two or three, and will require a presentation in the final week. Projects can be of various forms:

Tentative Schedule








Aug 31

- Computer aided software analysis: Overview, requirements specification, reactive programs, compilation process, program abstraction, data-flow and control-flow graphs, program analysis, and software model checking.




Sep 02-14

- Abstract Interpretation: Syntax and Semantics of programs, static semantics, consistent abstract interpretation, lattice of abstract interpretations, abstract evaluation of programs, Fixpoint approximation methods, widening and narrowing.

  P. Cousot and R. Cousot

ai1, ai2ai3, ai4  


Sep 16

 Rosh Hashanah (no class)




Sep 21-30

- Predicate Abstraction: parallel systems, predicate transformers, abstract semantics of programs, abstract state lattice, abstract transitions, computing abstract successors abstract  state space exploration, complexity, abstract state graph construction, state graph refinement implementation, reachability algorithm, applications

  P. S. Graf and H. Saidi

 pa2, pa3


Oct 3-12

- Abstraction refinement: Overview of the SLAM toolkit, the predicate abstraction tool C2bp, the model checking tool for boolean programs Bebop and the automatic refinement tool Newton.

 T.Ball, S.K. Rajamani



 Oct 14-21

 - Automated predicate abstraction of C Programs: Challenges of predicate abstraction in C, weakest precondition and cubes, pointers and aliasing, predicate abstraction for assignments, gotos and conditionals, and procedure calls, soundness and completeness, the C2bp tool.

 T.Ball, R. Majumdar, T. Millstein, S.K. Rajamani

c2bp1, c2bp2, c2bp3  


Oct 23-30

- Model checking boolean programs: Hierarchic state machines, push-down automata and boolean programs, statements, variables and scope, construction of the control flow graph, trace semantics, reachability via interprocedural dataflow analysis, path edges, summary edges, transfer functions, shortest trajectories, optimizations, the Bebop tool.

 T.Ball, S.K. Rajamani



Nov 04-25

 - Counterexample driven refinement: Explaining infeasible paths, path simulation via strongest postconditions, abstract explanations, basic path simulation, procedures and pointers, implementation in the {\sc Newton} tool, experiments.

 T.Ball, S.K. Rajamani


Nov 27

Thanksgiving (no class)




Dec 02-16

- Transition predicate abstraction: Automata-theoretic verification of concurrent programs, liveness and fair termination, abstract transition programs, transition predicates, automated abstraction, just termination, compassionate termination, lexicographic completeness.

M. VardiA. Podelski, a. Rybalchenko 



Last updated on Dec 16, 2004 by Radu Grosu