The Seventh Workshop on Tools for Automatic Program Analysis
September 7, 2016
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.
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)
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 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 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.
(Talk titles are linked to PDF abstracts.)
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.
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.
Hakjoo Oh, Kihong Heo, Hongseok Yang and Kwangkeun Yi
Mahmoud Mohsen and Bart Jacobs
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
Raphaël Rieu-Helft and Pascal Cuoq
Gadi Tellez and James Brotherston
Magnus Madsen, Ming-Ho Yee and Ondřej Lhoták
Reuben Rowe and James Brotherston
- 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
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.