Thesis Defense: A Symbolic Approach towards Constraint Based Software Verification

Hello ACM!

It’s that time of the year again: we are all invited to attend the following Master’s thesis defense this Friday. More information below!

I’d like to invite all CS faculty, graduate students, and staff to Shubhra Datta’s Master’s thesis defense, this Friday, September 9, at 9 a.m. in the CS conference Room (CS 221).

An abstract of her thesis is provided below. The complete document can be found at



Verification and validation (V&V) are two components of the software engineering process that are critical to achieve reliability that can account for up to 50% of the cost of software development [20]. Numerous techniques ranging from formal proofs to testing methods exist to verify whether programs conform to their specifications. Recently, constraint programming techniques for V&V have emerged [15,20]: they use the idea of proof by contradiction. They typically aim at proving that the code is inconsistent with the negation of the specification, which means that the software conforms to its specifications. Although the framework seems straightforward, the number of generated constraints can be high and the solving process tedious.

In this work, we propose ideas for improvement based on symbolic manipulation of the constraints to be solved. Our approach differs from the current approach in its way to determine the compliance of the code with respect to its specification. Instead of using numeric solvers, we designed symbolic techniques to check compliance between the code and its specification.

We analyzed how much practical the approach is if the program is correct and if the program is incorrect: can we make the verification process faster by applying our rules? CPBPV: a Constraint-Programming Framework for Bounded Program Verification [21], the work done by H. Collavizza,  M. Rueher, and P. Hentenryck is the inspiration for our work.

We established that our approach is feasible, and our experimental results prove that our proposed method is a promising addition to the existing framework to eliminate some of the basic challenges associated with constraint-based software verification.

Thesis Committee:
Dr. Martine Ceberio (Chair),
Dr. Vladik Kreinovich, and
Dr. Virgilio Gonzalez

Summer Formal 2011: First Summer School on Formal Techniques

Are you a graduate student interested in summer school and formal techniques?

Then this opportunity is for you!

May 23-27, 2011

Menlo College, Atherton, California USA

Formal verification techniques such as model checking, satisfiability,
and static analysis have matured rapidly in recent years.  These
techniques are widely applicable in computing as well as in engineering,
biology, and mathematics.  This school will focus on the principles and
practice of formal verification, with a strong emphasis on the hands-on
use of verification technology.  It primarily targets graduate students
who are interested in using or developing verification technology in
their own research.

We have NSF support for the travel and food/accommodation for students from
US universities, but welcome applications from graduate students at non-US
universities as well.

The lecturers at the school include

* Leonardo de Moura (Microsoft) and Bruno Dutertre (SRI International):
Satisfiability Modulo Theories
* Jason Baumgartner (IBM):
Hardware Verification: Model Checking and Equivalence Checking
* David Monniaux (VERIMAG):
Static Analysis
* Ken McMillan (Microsoft):
Abstraction, Interpolation, and Composition
* Neha Rungta and Peter Mehlitz (NASA Ames):
Software Verification with Java PathFinder
* Natarajan Shankar (SRI):
Interactive Theorem Proving

More information on the school can be found at
Students are invited to apply for admission to the school by visiting this
web site.  We especially welcome applications from women and
under-represented minorities.  Applications must be received by Mar 31, 2011.

Tom Ball, Lenore Zuck, and Natarajan Shankar
Summer Formal Steering Committee

Create a website or blog at

Up ↑