Tutorial
9:00 - 11:00 am Systematic Software Testing by Sarfraz Khurshid

Coffee Break
11:00 - 11:30 am

Invited Short Talks
11:30 - 11:45 am On the Verification of Concurrent Programs by Ahmed Bouajjani
11:45 - 12:00 pm The interleaving-explosion problem in testing concurrent programs by P. Madhusudan
12:00 - 12:15 pm Access Control Interoperability by Rupak Majumdar
12:15 - 12:30 pm Conflict-Tolerant Features by Deepak D'Souza

Lunch (12:30 pm - 2:00 pm)

Afternoon Session (2:00 pm - 6:30 pm)

Tutorial
2:00 - 4:00 pm Building a specialized static analyzer: the Astrée by Antoine Miné

Coffee Break
4:00 - 4:30 pm

Invited Short Talks
4:30 - 4:45 pm Static Computation of Symbolic Complexity Bounds by Sumit Gulwani
4:45 - 5:00 pm Refinement Types for Secure Implementations by Karthik Bhargavan
5:00 - 5:15 pm A Type System for Data Flow Integrity by Prasad Naldurg
5:15 - 5:30 pm Cryptography meets Programming Languages: A new class of problems by Ramarathnam Venkatesan

Discussion Session
5:30 - 6:30 pm

Dinner (at MSRI from 7:00 pm)

Tutorial Descriptions

• 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.
  Speaker: Sarfraz Khurshid is an Assistant Professor in the Electrical and Computer Engineering department at the University of Texas at Austin, where he leads the Software Verification and Testing Group. He obtained his PhD in Computer Science from MIT in 2004. He received a BSc in Mathematics and Computer Science from Imperial College London, and read Part III of the Mathematical Tripos at Trinity College Cambridge. His current research focuses on software testing, specification languages, code conformance, model checking, data structure repair, and applications of heuristics in program analysis.


• 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.
  Speaker:Antoine Miné is a junior research scientist at the French CNRS (National Center for Scientific Research). He received his PhD in computer science in 2004 from the Ecole Normale Superieure (Paris, France) for his dissertation on "Weakly Numerical Abstract Domains". His main research interets are: program semantics, Abstract Interpretation theory, static program analysis, and their application to improve the reliability of software. He has participated in the design of the Astrée static analyzer that proved the absence of run-time errors on safety-critical industrial avionic software.