The workshop will feature invited tutorials to cover a couple of selected topics in the area in depth. The workshop will also feature a set of short invited talks to cover the breadth of the area.

Students are particularly encouraged to attend since they may get an opportunity to find a mentor to work on common problems of interest.

Tutorials

• Systematic Software Testing by Sarfraz Khurshid (University of Texas, Austin)
  Abstract: The most commonly used methodology for validating the quality of software is testing. However, the traditional techniques for testing are ad hoc, ineffective, and expensive. Recent years have seen significant progress in new techniques that check software systematically, handle complex programs, and are automatic. This tutorial first describes the basics of software testing, and then describes two techniques that automate systematic testing: (1) Korat -- a technique that was developed recently for black-box testing; and (2) symbolic execution -- a technique that was developed over three decades ago but is seeing a real resurgence for white-box testing. Case-studies that illustrate the power and effectiveness of the two techniques are also presented.
• Building a specialized static analyzer: the Astrée experience by Antoine Miné (CNRS, France)
  Abstract: Astrée is a sound static analyzer that discovers all the run-time errors in embedded C programs. Astrée is based on a very general and parametric Abstract Interpretation framework, and is tailored for a specific class of applications, avionics control-command software, where it delivers a high precision. It was able to prove automatically the absence of run-time errors in industrial programs of hundreds of thousand lines. In this talk, we will present the design of Astrée. In particular, we will describe and illustrate the semantic and algorithmic decisions we made during its specialization towards high precision and scalability.

Short Talks

• Refinement Types for Secure Implementations by Karthik Bhargavan (MSR Cambridge)
• On the Verification of Concurrent Programs by Ahmed Bouajjani (University of Paris)
• Conflict-Tolerant Features by Deepak D'Souza (IISc, Bangalore)
• Static Computation of Symbolic Complexity Bounds by Sumit Gulwani (MSR Redmond)
• Access Control Interoperability by Rupak Majumdar (UCLA)
• A Type System for Data Flow Integrity by Prasad Naldurg (MSR Bangalore)
• The interleaving-explosion problem in testing concurrent programs by P. Madhusudan (UIUC)
• Cryptography meets Programming Languages: A new class of problems by Ramarathnam Venkatesan (MSR Redmond)

Organizers

• Sumit Gulwani
• Prasad Naldurg
• Madhusudan Parthasarthy

Sponsors

• FSTTCS 2008
• Microsoft Research, India