Workshop on Software Verification

A preconference workshop of the 25th FSTTCS
December 14, 2005

Preparatory Tutorial: December 13, 2005

University of Hyderabad,
adjacent to IIIT (International Institute of Information Technology)

Hyderabad, INDIA
Click here for local arrangements

Workshop Organizers
P. Madhusudan (UIUC) and Sriram Rajamani (Microsoft Research)

The engineering of correct software is one of the grand challenges of computer science. Design and verification methodologies to ensure correct software will have a great impact on how programs are built in the industry, and yet we know very little on how to attack this problem. The workshop will focus on verification: techniques and methods that build on theoretically sound foundations to tools that can perform verification of realistic programs. The workshop will be composed of a set of invited talks that span a spectrum of problems and solutions, and will hopefully convey the excitement of this emerging area to an informed but not expert audience. In particular, we will hear talks that cover the following topics: abstraction based model checking, theorem proving, static analysis, analysis of data structures using shapes, and analysis methods for concurrency.

We will also have a preparatory tutorial on the 13th to prime the audience on background material for the workshop on the 14th.

Confirmed invited workshop speakers:
Shaz Qadeer (Microsoft Research, Redmond, USA)
Tom Henzinger (EPFL, Lausanne, Switzerland)
G. Ramalingam (IBM Research)
Stefan Schwoon (Univ of Stuttgart)
Natarajan Shankar (SRI, USA)

Pre-workshop tutorial Programme (13 December 2005, Tuesday)
9:15am Opening Remarks
9:30am - 10:45 am S.P. Suresh, Chennai Math. Inst., Chennai
Dataflow Analysis - Part I
10:45am - 11:00am Break
11:00am - 12:15 pm Supratik Chakraborty, IIT, Bombay
Dataflow analysis - Part II
12:15pm - 1:45pm Lunch
1:45pm - 3:00pm P. Madhusudan, Univ of Illinois at Urbana-Champaign
Predicate abstraction and abstract interpretation
3:00pm - 3:15pm Break
3:15pm - 4:30pm R. Ramanujam, Inst. of Math. Sc., Chennai
Pushdown model-checking

Workshop Programme (14 December 2005, Wednesday)
8:45am Opening Remarks
9:00am - 10:10 am Tom Henzinger, EPFL, Switzerland
The BLAST Model Checker
10:10am - 10:30am Break
10:30am - 11:40 pm G. Ramalingam, IBM Research
Heap Abstractions for Software Verification
11:40pm - 12:50pm Shaz Qadeer, Microsoft Research
Precise data-race detection and efficient model checking using locksets
12:50pm - 2:20pm Lunch
2:20pm - 3:30pm Stefan Schwoon, Univ of Stuttgart
Weighted PDS and their application to program analysis
3:30pm - 3:50pm Break
3:50pm - 5:00pm Natarajan Shankar, SRI
The Challenge of Verified Software