Ensuring that our programs behave correctly and reliably is a fundamental challenge facing computing today. Recent years have seen an explosion of a diverse set of new techniques for ensuring program correctness ranging from verification and synthesis approaches to runtime systems to quantitative reasoning. The aim of the workshop is to provide insight into the latest research advances in the area. In a period of two days, the workshop will host a number of invited speakers who will present research talks related to software reliability and correctness.


Organizers: Peter Müller (ETH Zürich) , Martin Vechev (ETH Zürich)

This is the third time the workshop is being held. Materials from the 2014 and 2013 workshops are also available.

Schedule

October 2 (Friday)

TimeSpeakerInstitutionTalk Title & AbstractSlidesVideo
9:00 - 9:15OrganizersETH Zürich
Opening Remarks
9:15 - 10:00 Patrick CousotNYU/ENS
Abstract Induction
PDF
10:00 - 10:45 Thomas GrossETH Zürich
Walls, Gates, and Guards
PDF
10:45 - 11:15Coffee Break  
11:15 - 12:00 Roberto GiacobazziUniversity of Verona (Italy)
and IMDEA Software Institute (Spain)
Analysing Completeness in Program Analysis
PDF
12:00 - 13:30Lunch
13:30 - 14:15 Cristiano CalcagnoFacebook/Imperial College
Infer: deploying static analysis at Facebook
PDF
14:15 - 15:00 Marco PistoiaIBM T.J. Watson Research Center
Combining Static Analysis and Machine Learning for Industrial-quality Information-flow-security Enforcement
PDF
15:00 - 15:30Coffee Break   
15:30 - 16:15 Natasha SharyginaUniversity of Lugano
PeRIPLO: A Framework for Producing Effective Interpolants in SAT-Based Software Verification
PDF
16:15 - 16:45 Martin Vechev
ETH Zürich
Commutativity Race Detection: Concepts, Algorithms and Open Problems
PDF
16:45 - 17:15 Peter Müller ETH Zürich
Viper - A Verification Infrastructure for Permission-based Reasoning
PDF

October 3 (Saturday)

TimeSpeakerInstitutionTalk Title & AbstractSlidesVideo
9:00 - 9:15OrganizersETH Zürich
Opening Remarks
9:15 - 10:00 Vivek SarkarRice University
Avoidance, Detection, and Repair of Bugs in Structured Parallel Programs
PDF
10:00 - 10:45 Ken McMillanMicrosoft Research
Human-machine interaction in invariance proofs
PDF
10:45 - 11:15Coffee Break  
11:15 - 12:00 Andreas PodelskiFreiburg
Proof Spaces
PDF
12:00 - 13:30Lunch
13:30 - 14:15 Akash LalMicrosoft Research
DAG Inlining: A Decision Procedure for Reachability-Modulo-Theories in Hierarchical Programs
PDF
14:15 - 15:00 Umut AcarCarnegie Melon University
Challenges of Parallelism in Research and Teaching
PDF
15:00 - 15:45 Patrick LamUniversity of Waterloo
Static and Dynamic Analysis of Test Suites
PDF
15:45 - 15:50 OrganizersETH ZürichClosing Remarks

Registration

Early Bird: by Sept 1st 2015Regular fee: after Sept 1st, 2015 (latest day: Sept 22, 2015)
Workshop Fee (Students) 70 CHF90 CHF
Workshop Fee (Regular) 110 CHF130 CHF
The registration fees include:

To register, please follow this link: Workshop Registration

For information and questions, please contact Mrs. Marlies Weissert: marlies.weissert@inf.ethz.ch

Travel


ETH Zürich is located in the heart of the city and easy to reach.

From Zürich HB (main station): If you arrive by train to Zürich HB, take either:

From Zürich airport: You can either take the tram to ETH or a train to the city center (Zürich HB):

Accomodation

You can check the availability and prices and make reservations for hotels at Zürich Tourism

The following is a list of hotels in walking distance from the workshop venue:

Some hotels further away: