COMP 607: Seminar on Computer-Aided Verification

Compiled by Moshe Y. Vardi

Safety-critical computers increasingly affect nearly every aspect of our lives. Computers control the planes we fly on, monitor our health in hospitals and do our work in hazardous environments. Computers with software deficiencies have resulted in catastrophic failures. The goal of formal verification is to to improve the safety and reliability of such hardware and software.

Computer-aided verification is the study of algorithms and structures applicable to the verification of hardware and software designs. It draws upon ideas and results from logic, graph theory, and automata theory, and combines theoretical and experimental aspects. In the last few years, this area has seen a dramatic expansion of activities. Today, companies such as AT&T, Lucent, Intel, SGI, DEC, Motorola, and SUN, which as recently as 5-6 years ago would have nothing to do with formal verification, cannot wait to get the most advanced tools available, and many of them have formed R&D groups to develop verification software tools and apply them to their own designs. In addition, several commercial tools have been announced over the last couple of years. As tool creation is driven directly from the theory, this creates an unusual opportunity to see theory put directly to practice, a stimulating and attractive reward.

The seminar will serve as a participatory introduction to this dynamic research area. We will meet weekly and read together a doctoral dissertation covering the theoretical and practical aspects of computer-aided verification.

Course Material:

  • Verification at IBM
  • Verification at Intel
  • Proceedings of FMCAD'2013
  • Presentations at FMCAD'2013
  • Dror Fried: Syntax Guided Synthesis, Feb. 3, 2014
  • Giuseppe Perelli: Distributed Synthesis for LTL Fragments, Feb. 14, 2014
  • Morteza Lahijanian: Counter-Strategy Guided Refinement of GR(1) Temporal Logic Specifications, Feb. 21, 2014
  • Srinivas Nedunuri: Exploring Interpolants, Feb. 24, 2014
  • Kuldeep S. Meel: An SMT Method for Optimizing Arithmetic Computations, March 14, 2014
  • Yue Wang: Efficient MUS Extraction with Resolution, March 21, 2014
  • Lucas Martinelli Tabajara: Synthesizing Multiple Boolean Functions using Interpolation on a Single Proof, March 28, 2014
  • Chao Xu: Formal Co-Validation of Low-Level Hardware/Software Interfaces, March 31, 2014
  • Sonali Dutta: Efficient Handling of Obligation Constraints in Synthesis from Omega-Regular Specifications, April 11, 2014.
  • Ye Fang: On the Feasibility of Automation for Bandwidth Allocation Problems in Data Centers, April 14, 2014.
  • Keliang He: Trimming while Checking Clausal Proofs, April 21, 2014.
  • Anitha Golamudi: Proving Termination of Imperative Programs Using Max-SMT, April 28, 2014.