TAPAS 2016

The Seventh Workshop on Tools for Automatic Program Analysis

September 7, 2016
Edinburgh, UK

Objective

In the last fifteen years, a wide range of static analysis tools have emerged, some of which are currently in industrial use or are well beyond the advanced prototype level. Many impressive practical results have been obtained, which allow complex properties to be proven or checked in a fully or semi-automatic way, even in the context of complex software developments. In parallel, the techniques to design and implement static analysis tools have improved significantly, and much effort is being put into engineering the tools. This workshop is intended to promote discussions and exchange experience between specialists in all areas of program analysis design and implementation and static analysis tool users.

Previous workshops have been held in Perpignan, France (2010), Venice, Italy (2011), Deauville, France (2012), Seattle, WA, USA (2013), Munich, Germany (2014), and Saint-Malo, France (2015).

TAPAS 2016 will be co-located with SAS 2016, and also PPDP and LOPSTR 2016.

Scope

The technical program of TAPAS 2016 will consist of invited lectures together with presentations based on submitted abstracts.

Submitted presentation abstracts can cover any aspect of program analysis tools including, but not limited to the following:

  • design and implementation of static analysis tools (including practical techniques used for obtaining precision and performance)
  • components of static analysis tools (front-ends, abstract domains, etc.)
  • integration of static analyzers (in proof assistants, test generation tools, IDEs, etc.)
  • reusable software infrastructure (analysis algorithms and frameworks)
  • experience reports on the use of static analyzers (both research prototypes and industrial tools)

Invited Speakers

Jan Midtgaard, Technical University of Denmark
Jan works with static analysis, functional programming, and their intersection at DTU Compute, Technical University of Denmark. Previously he has worked at both INRIA Rennes and Aarhus University, from where he also received his PhD.
Aditya Nori, Microsoft Research Cambridge
Aditya Nori is a member of the Programming Principles and Tools group at Microsoft Research Cambridge. His research interests are: the design and analysis of reliable intelligent systems with current focus on precise and robust medical image analysis for cancer treatment. Over the past few years, he has worked on exploring various synergies between programming languages and machine learning – these include the use of machine learning techniques for proving programs correct, specification inference via Bayesian analysis, probabilistic programming via program analysis, and productivity tools for machine learning tasks. He is a co-winner of the ACM SIGSOFT Distinguished Paper award at FSE 2006 and FSE 2015. He received his PhD in computer science from the Indian Institute of Science, Bangalore.
Peter O'Hearn, University College London / Facebook
Peter O’Hearn works as an Engineering Manager at Facebook with the Static Analysis Tools team, and as a Professor of Computer Science at University College London. His research has been in the broad areas of programming languages and logic, ranging from new logics and mathematical models to industrial applications of program proof. With John Reynolds he developed separation logic, a theory which opened up new practical possibilities for program proof. In 2009 he cofounded a software verification startup company, Monoidics Ltd, which was acquired by Facebook in 2013. The Facebook Infer program analyzer, recently open-sourced, runs on every modification to the code of Facebook’s mobile apps — including the main Facebook apps for Android and iOS, Facebook Messenger and Instagram — in a typical month issuing millions of calls to a custom separation logic theorem prover and resulting in hundreds of bugs being fixed before they reach production. Peter has been the recipient of a number of awards for his work in verification, including the 2016 Godel Prize, the 2016 CAV award, and a 2011 Most Influential POPL paper award.

Program

(Talk titles are linked to PDF abstracts.)

9:00am-9:15am
Intro
9:15am-10am
Peter O'Hearn
Developing and Deploying the Infer Program Analyzer at Facebook

Abstract: Catching bugs early in the development process improves software quality and saves developer time. Static analyzers are magical tools that catch bugs before runtime without requiring any extra effort from developers. At Facebook, we are building Infer, an open-source (fbinfer.com) static analyzer for Android, iOS, and C++ code. In this talk, I will discuss the challenges we have faced in developing static analysis techniques that can cope with Facebook’s scale and velocity, the challenges of different modes of deployment, and some lessons we have learned that might be relevant to static analysis research.

10:00am-10:30am
coffee break
10:30am-11:15am
Jan Midtgaard
QuickChecking Static Analysis Properties

Abstract: A static analysis can check programs for potential errors. A natural question that arises is therefore: who checks the checker? Researchers have given this question varying attention, ranging from basic testing techniques, informal monotonicity arguments, thorough pen-and-paper soundness proofs, to verified fixed point checking. In this talk we demonstrate how quickchecking can be used to test a range of static analysis properties with limited effort. We show how to check a range of algebraic lattice properties, to help ensure that an implementation follows the formal specification of a lattice. Moreover, we offer a number of generic, type-safe combinators to check transfer functions and operators on lattices, to help ensure that these are, e.g., monotone, strict, or invariant. We report on how we have used the approach to quickcheck both a type analysis for the Lua programming language as well as some examples from the literature. Overall we argue that the approach can be useful for finding errors in static analyses, for improving their precision, and for guiding their design.

11:15am-11:40am
Hakjoo Oh, Kihong Heo, Hongseok Yang and Kwangkeun Yi
12:05pm-1:30pm
lunch
1:30pm-2:15pm
Aditya Nori
Probabilistic Programming: Formal Techniques and Applications

Abstract: Probabilistic models, particularly those with causal dependencies, can be succinctly written as probabilistic programs. Recent years have seen a proliferation of languages for writing such probabilistic programs, as well as various tools and techniques for probabilistic programming. In this talk, I will describe three ideas: 1) a provably correct sampler for probabilistic programs, 2) synthesis of probabilistic programs, and 3) an application that employs probabilistic programming for debugging machine learning tasks. All these ideas are inspired by analogous problems in formal methods and software engineering.

2:15pm-2:40pm
Raphaël Rieu-Helft and Pascal Cuoq
2:40pm-3:05pm
Gadi Tellez and James Brotherston
3:05pm-3:30pm
coffee break
3:30pm-3:55pm
Magnus Madsen, Ming-Ho Yee and Ondřej Lhoták
3:55pm-4:20pm
Grigory Fedyukovich
4:45pm-5pm
wrapup

Important Dates

  • Submission deadline: July 11, 9pm PDT (EXTENDED)
  • Notification of acceptance: July 18
  • Early registration deadline: August 15
  • Final version due: September 1
  • Workshop: September 7

Venue and Registration

Please see the main PPDP / LOPSTR / SAS page for details.

Attendees should determine if they need a visa to visit the UK; the visa process can take 6-8 weeks. If you need a visa, please register and send in the information needed to generate a visa support letter, as described on the registration page.

Organizing Committee

Manu Sridharan, Samsung Research America (chair)
Sukyoung Ryu, KAIST
Ilya Sergey, University College London
Harry Xu, University of California, Irvine
Eran Yahav, Technion