Contact: tapas2015@easychair.org

Objectives

In the last ten 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), and Seattle, WA, USA (2013), and Munich, Germany (2014).

Scope

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

We welcome presentations on all aspects of program analysis tools including, but not limited to the following:

• design and implementation of static analysis tools to check, prove or infer properties (including practical techniques used for obtaining precision and performance);
• components and other reusable infrastructure of static analysis tools (front-ends, abstract domains, solvers, analysis algorithms, frameworks, etc.);
• integration of static analyzers (in proof assistants, test generation tools, IDEs, etc.);
• experience reports on the use of static analyzers (both research prototypes and industrial tools);
• challenges for static analysis tools, such as new properties to address or bottlenecks to overcome;
• usability of static analysis tools (including user interfaces and other tools helping to exploit static analysis results); and
• tool demonstrations, and comparisons, by tool authors or experienced users.

Invited Speakers

Patrick Cousot, New York University

Sound Verification by Abstract Interpretation

Abstract: Automatic program verification tools have to cope with programming language and machine semantics, undecidability, and mathematical induction, and so are all complex and imperfect. The ins and outs of automatic program verification will be discussed in light of the theory and practice of abstract interpretation.

Biography: Patrick Cousot received the Doctor Engineer degree in Computer Science and the Doctor ès Sciences degree in Mathematics from the University Joseph Fourier of Grenoble, France.

Patrick Cousot is Silver Professor of Computer Science at the Courant Institute of Mathematical Sciences, New York University, USA.

Before he was Professor at the the École Normale Supérieure, Paris, France, the École Polytechnique and the University of Metz and a Research Scientist at the French National Center for Scientific Research at the University Joseph Fourier of Grenoble, France.

Patrick Cousot is the inventor, with Radhia Cousot, of Abstract Interpretation.

Patrick Cousot was awarded the Silver Medal of the CNRS (1999), a honorary doctorate from the Fakultät Mathematik und Informatik of the Universität des Saarlandes (2001), the Grand Prix of Computer Science and its Applications of the Fondation Airbus Group attributed by the French Academy of Sciences (2006), a Humboldt Research Award (2008), and, with Radhia Cousot, the ACM-SIPLAN Programming Languages Achievement Award (2013) and the IEEE Harlan D. Mills Joint Award (2014). He is Member of the Academia Europaæ, Informatics section (since 2006).

Pascal Cuoq, TrustInSoft

Verifying the Absence of Undefined Behavior in a Minimal but Realistic Configuration of PolarSSL

Abstract: Software bugs of all nature are unpleasant. Functional bugs require a functional specification before they can be automatically detected, or their absence formally proved. For an under-specified programming language such as C, one implicit expectation is that the program's execution will not run into undefined behavior. This expectation is convenient because it can be formalized with only a few rare points of disagreement with C developers' own view of the C language. At the same time, this implicit expectation is a useful one to verify formally: in the context of C programs taking inputs from an unfriendly outside world, undefined behavior sometimes end up giving the attacker more control over the host computer than the developer intended.

The authors verified the absence of undefined behavior in a minimal but realistic configuration of PolarSSL 1.1.8. Since an SSL/TLS server does not provide Remote Procedure Call-like functionality to outsiders through defined behavior, the only way it can provide this functionality is through undefined behavior. Indeed, as found during the verification, PolarSSL 1.1.7 probably provided remote code execution functionality to outsiders for some compilations and target platforms (CVE-2013-5914).

The authors used analyses available in the Frama-C platform for the verification, with additional proprietary plug-ins for tracking the properties being verified and applying sanity checks to the results. This presentation provides insights into the process and the results of this verification.

Biography: Pascal Cuoq first studied static analysis with Marc Pouzet during his PhD, and became more interested in Abstract Interpretation during his post-doctoral year with Kwangkeun Yi. For ten years he worked in CEA LIST's Software Reliability lab, initially on the software verification tool CAVEAT, and then as one of the initiators of Frama-C. In 2013, together with Benjamin Monate and Fabrice Derepas, Pascal Cuoq founded the company TrustInSoft to transfer Frama-C from the world of safety-critical software, where it has its roots, to the world of software security, where some formal assurances seem much needed.

Don Sannella, Contemplate & University of Edinburgh

ThreadSafe: Static Analysis for Java Concurrency

Abstract: ThreadSafe is a commercial static analysis tool that focuses on detection of Java concurrency defects. By restricting attention to concurrency bugs, ThreadSafe can find bugs that other static analysis tools, both commercial and freely available, miss or are not designed to look for. Its findings are generated from information produced by a class-by-class flow-sensitive, path-sensitive, context-sensitive points-to and lock analysis, with heuristics to tune the analysis to avoid false positives. It has been successfully applied to codebases of more than a million lines.

Biography: Professor in the School of Informatics at Edinburgh University, Don Sannella was educated at Yale, UC Berkeley, and Edinburgh University. He is Editor-in-Chief of the journal Theoretical Computer Science and a Fellow of the Royal Society of Edinburgh. In 2009, after 30 years of academic research on formal specification, verification and refinement, static analysis and security, Don (together with David Aspinall) founded Contemplate, where he is currently CEO, to develop tools for programmers to improve the quality of software products, building on the results of a research project on static analysis for Java. Contemplate's product ThreadSafe is used by companies worldwide to identify and avoid software failures in complex Java applications.

Max Schaefer, Semmle

Analysing Software Engineering Data

Abstract: Semmle offers a static analysis platform centred around two key concepts: database-backed program analysis, and analysis of non-code artifacts. The former means that analyses are implemented as queries written in QL, a high-level, declarative, object-oriented dialect of Datalog, which run on a relational database representing the code base under analysis. The latter means that this database is enriched with all kinds of meta-information associated with the software development process, such as source control information, issue tracking data, or test coverage metrics, which can be analysed in conjunction with the code itself.

We will demonstrate on a few examples how QL empowers static analysis experts and ordinary developers alike to implement both quick syntactic checks and deeper semantic analyses. We will also show how the seamless integration of code and non-code artifacts can be leveraged to improve analysis results, and how it enables us to ask and answer questions that lie outside the realm of classic static analysis.

Biography: Max is a research engineer with Semmle Ltd. in Oxford, where he is in charge of analysis support for JavaScript and contributes to the core analysis platform. Before joining Semmle, he was with IBM Research and NTU Singapore, working on static analysis, testing, and hybrid analysis for dynamic languages. He holds a doctorate from Oxford University.

Accepted Presentations

Wolfgang Ahrendt, Laura Kovacs and Simon Robillard.

Loop Analysis Using Theorem Proving and Symbol Elimination

In 2009, the symbol elimination method for loop invariant generation was introduced. Symbol elimination exploits the power of first-order theorem proving, in particular of the Vampire prover, to generate quantified loop invariants, possibly with quantifier alternations, of program loops over arrays. Symbol elimination is fully automatic, that is it does not require the user to provide additional predicates or templates. Symbol elimination relies on so-called extended expressions, which are symbolic representations of the value of a program variable as a function of the loop iteration counter. First-order formulas with extended expressions form a rich language, with which one can express many interesting loop properties, for example by using some lightweight static analysis over program variables. Once these loop properties with extended expressions are collected, the next step of symbol elimination is to use the saturation engine and consequence elimination capabilities of Vampire. This way, logical consequences of the loop properties with extended expressions are derived; however, these consequences contain no extended expressions and are expressed using the language of program expressions. Therefore, these properties describe loop invariants and can be used in the context of Hoare logic–based verification or other verification systems.
In this paper, we describe a new implementation of symbol elimination and loop analysis in Vampire. We also extend symbol elimination by using the pre- and post-conditions of loops. We use these specifications to get more precise invariants and to select invariants relevant to the correctness proof of the loop. Together with the loop specification, the properties generated by symbol elimination capture the information needed to directly verify the partial correctness of the loop. This way, symbol elimination offers an automatic alternative to, for example, the classic Hoare rule–based verification for loops.
Our implementation of symbol elimination and loop analysis in Vampire is not limited to a specific programming language, but instead takes as input a simple guarded command language. As an example of the usability of our work in the context of a real language with more complex semantics, we interfaced our tool with the KeY verification system. KeY formalizes the correctness of annotated Java programs as dynamic logic formulas, and tries to automatically prove these formulas. In the case of programs containing loops, user-provided invariants are usually required in order to apply the dedicated dynamic logic rule. We exploit symbolic execution, already used by KeY to prove properties of programs, to obtain a semantically correct translation of Java code into the language used by our tool. We then use this translation to either produce invariants to be used in the dynamic logic rule or delegate the proof of correctness of that part of the program to Vampire.
We have successfully evaluated our work on a number of examples coming from KeY, thus providing interesting and realistic case studies of using symbol elimination in the static analysis of loops.

Georges Dupéron and Roland Ducournau.

k-l-CFA: A Practical Implementation

We have implemented k-l-CFA (control-flow analysis) for a real-world object-oriented programming language. We present how we handle some features of the language which interact with the analysis, and compare the precision of the results obtained via different ways of handling them. These features include generic types, delegates (closures encapsulating a method pointer and its receiver object), as well as covariant arrays.
We have compared the results obtained in our analysis with those produced by an independently developed implementation. This mutual black-box comparison enabled identification of other variation points in the CFA algorithm and additionally, assessment of the quality of both implementations.

Colin Runciman and Simon Thompson.

Demur: Checking Functional-program Properties Using Bounded Recursion

The Demur tool translates programs and properties expressed in a large subset of Haskell to decidable models in Z3. These models use a bounded-depth representation of recursive function definitions, where the bound is increased from zero as checking proceeds. An explicit and distinguishable representation of undefined parts of data values enables Demur to maximize property-checking power despite approximation – for example, by using parallel three-valued logical operators. Several case-studies present a mixture of successes and failures in comparison with current widely-used tools for property checking. Possible routes to improved performance are identified. Comparisons are drawn with other Z3-based tools with functional-language translators, such as Leon and Halo.

Boris Yakobowski.

Fast Whole-program Verification Using On-the-fly Summarization

We present an on-the-fly summarization mechanism, employed by the Value Analysis plugin of Frama-C to significantly speed up its analyses. When a function call has been fully analyzed, the analyzer memorizes (1) the variables that were read during the analysis, (2) those that were written, and (3) the values for those input and output variables. This forms a summary of this particular call, which is saved in the hope that it may be reused later. This is the case when another call occurs with unchanged values for the input variables. We implemented our technique within Frama-C/Value. Using an agressive strategy that catches indiscriminately all function calls, we routinely obtain ×15 speedups in analysis time, with reasonable overhead w.r.t. memory consumption.

Important Dates

Submission deadline:	26	June	2015 (anywhere on earth)
Author notification:	17	July	2015
Early registration deadline:	21	July	2015
Workshop:	8	September	2015

Venue, Registration, and Accommodation

Please refer to the SAS 2015 website.

Program

9:00 – 10:00	Pascal Cuoq	Verifying the Absence of Undefined Behavior in a Minimal but Realistic Configuration of PolarSSL
10:00 – 10:30	Boris Yakobowski	Fast Whole-program Verification Using On-the-fly Summarization
coffee break
11:00 – 12:00	Don Sannella	ThreadSafe: Static Analysis for Java Concurrency
12:00 – 12:30	Georges Dupéron and Roland Ducournau	k-l-CFA: A Practical Implementation
lunch break
14:00 – 15:00	Patrick Cousot	Sound Verification by Abstract Interpretation
15:00 – 15:30	Wolfgang Ahrendt, Laura Kovacs and Simon Robillard	Loop Analysis Using Theorem Proving and Symbol Elimination
coffee break
16:00 – 17:00	Max Schaefer	Analysing Software Engineering Data
17:00 – 17:30	Colin Runciman and Simon Thompson	Demur: Checking Functional-program Properties Using Bounded Recursion

Program Committee

Josh Berdine	Microsoft Research (chair)
Arie Gurfinkel	Software Engineering Institute, Carnegie Mellon University
Jan Reineke	Saarland University
Manuel Hermenegildo	T.U. Madrid (UPM) and IMDEA Software Institute
Ralf Huuck	NICTA, University of New South Wales, and Red Lizard Software
Mihaela Sighireanu	LIAFA, University of Paris Diderot, and CNRS
Laura Kovacs	Chalmers University of Technology
Andreas Podelski	University of Freiburg
Mooly Sagiv	Tel-Aviv University