University of Hyderabad,
adjacent
to IIIT (International Institute of Information
Technology)
Hyderabad, INDIA
Click here for local arrangements
|
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.
|
| Shaz Qadeer | (Microsoft Research, Redmond, USA) |
|---|---|
| Tom Henzinger | (EPFL, Lausanne, Switzerland)
|
| G. Ramalingam | (IBM Research)
|
| Stefan Schwoon | (Univ of Stuttgart)
|
| Natarajan Shankar | (SRI, USA) |
| 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 |
| 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 |