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:
(Talk titles are linked to PDF abstracts.)
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.
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.
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.
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.
Manu Sridharan, Samsung Research America (chair)
Sukyoung Ryu, KAIST
Ilya Sergey, University College London
Harry Xu, University of California, Irvine
Eran Yahav, Technion