SMT Techniques and Solvers in Automated Termination Analysis

Carsten Fuhs

Birkbeck, University of London

Termination is the property of a program that regardless of the input, execution of the program will always come to a halt eventually. Although this property is undecidable, since the early 2000s fully automated techniques and tools for termination analysis have flourished in several communities: term rewriting, imperative programs, functional programs, logic programs, ...

A common theme behind most of these tools is the use of constraint-based techniques to advance the proof of (non-)termination. Recently, in particular SAT and SMT solvers are used as back-ends to automate these techniques. In my talk, I will give an overview of automated termination analysis from an SMT solving perspective.

Slides available as .pdf

From Datalog to Flix: A Declarative Language for Fixed Points on Lattices

Magnus Madsen

University of Waterloo

We present FLIX, a declarative programming language for specifying and solving least fixed point problems, particularly static program analyses. FLIX is inspired by Datalog and extends it with lattices and monotone functions. Using FLIX, implementors of static analyses can express a broader range of analyses than is currently possible in pure Datalog, while retaining its familiar rule-based syntax.

We define a model-theoretic semantics of FLIX as a natural extension of the Datalog semantics. This semantics captures the declarative meaning of FLIX programs without imposing any specific evaluation strategy. An efficient strategy is semi-naïve evaluation which we adapt for FLIX. We have implemented a compiler and runtime for FLIX, and used it to express several well-known static analyses, including the IFDS and IDE algorithms. The declarative nature of FLIX clearly exposes the similarity between these two algorithms.

Slides available as .pdf

Static analysis for security, privacy and mechanism design

Fritz Henglein

DIKU

Dynamic networking, Big Data analytics, artificial intelligence, autonomous devices (cars, robots, Internet of Things), additive manufacturing (3D printing), blockchain (distributed systems with "smart" contracts) are enthusiastically propagated technology trends becoming central to the very fabric of society. At their core is software, which assuredly needs to function properly. Early indications are disconcerting, however: the technologies are typically driven by technology optimists with no or only rudimentary knowledge of static analysis and related assurance techniques. This talk will sketch and illustrate some of the challenges and invite the DANSAS community to contribute to actively shaping policy, design and implementation of cybersecurity, privacy and mechanisms. The concrete background is the formation of a national cybersecurity network across multiple innovation networks and the establishment of the EU Private-Public-Partnership (PPP) in cybersecurity, which will shape the Horizon 2020 work programme 2018-20.

Slides available as .pdf

Type Unsoundness in Practice: An Empirical Study of Dart

Gianluca Mezzetti

Aarhus University

The type system in the Dart programming language is deliberately designed to be unsound: for a number of reasons, it may happen that a program encounters type errors at runtime although the static type checker reports no warnings. According to the language designers, this ensures a pragmatic balance between the ability to catch bugs statically and allowing a flexible programming style without burdening the programmer with a lot of spurious type warnings.

In this work, we attempt to experimentally validate these design choices. Through an empirical evaluation based on open source programs written in Dart totalling 2.4 M LOC, we explore how alternative, more sound choices affect the type warnings being produced. Our results show that some, but not all, sources of unsoundness can be justified. In particular, we find that unsoundness caused by bivariant function subtyping and method overriding does not seem to help programmers. Such information may be useful when designing future versions of the language or entirely new languages.

Joint work with Anders Møller and Fabio Strocco

Slides available as .pdf

Trace Typing: An Approach for Evaluating Retrofitted Type Systems

Esben Andreasen

Aarhus University

Recent years have seen growing interest in the retrofitting of type systems onto dynamically-typed programming languages, in order to improve type safety, programmer productivity, or performance. In such cases, type system developers must strike a delicate balance between disallowing certain coding patterns to keep the type system simple, or including them at the expense of additional complexity and effort. Thus far, the process for designing retrofitted type systems has been largely ad hoc, because evaluating multiple variations of a type system on large bodies of existing code is a significant undertaking. We present trace typing: a framework for automatically and quantitatively evaluating variations of a retrofitted type system on large code bases. The trace typing approach involves gathering traces of program executions, inferring types for instances of variables and expressions occurring in a trace, and merging types according to merge strategies that reflect specific (combinations of) choices in the source-level type system design space. We evaluated trace typing through several experiments. We compared several variations of type systems retrofitted onto JavaScript, measuring the number of program locations with type errors in each case on a suite of over fifty thousand lines of JavaScript code. We also used trace typing to validate and guide the design of a new retrofitted type system that enforces fixed object layout for JavaScript objects. Finally, we leveraged the types computed by trace typing to automatically identify tag tests --- dynamic checks that refine a type --- and examined the variety of tests identified.

Joint work with Colin S. Gordon, Satish Chandra, Manu Sridharan, Frank Tip and Koushik Sen

Slides available as .pdf

Analyzing Test Completeness for Dynamic Languages

Anders Møller

Aarhus University

In dynamically typed programming languages, type errors can occur at runtime. Executing the test suites that often accompany programs may provide some confidence about absence of such errors, but generally without any guarantee. We present a program analysis that can check whether a test suite has sufficient coverage to prove a given type-related property, which is particularly challenging for program code with overloading and value dependent types. The analysis achieves a synergy between scalable static analysis and dynamic analysis that goes beyond what can be accomplished by the static analysis alone. Additionally, the analysis provides a new coverage adequacy metric for the completeness of a test suite regarding a family of type-related properties.

Based on an implementation for Dart, we demonstrate how such a hybrid static/dynamic program analysis can be used for measuring the quality of a test suite with respect to showing absence of type errors and inferring sound call graph information, specifically for program code that is difficult to handle by traditional static analysis techniques.

Joint work with Christoffer Quist Adamsen and Gianluca Mezzetti

Symbolic Execution of High-Level Transformations

Ahmad Salim Al-Sibahi

ITU

Transformations form an important part of developing domain specific languages, where they are used to provide semantics for typing and evaluation. Yet, few solutions exist for verifying transformations written in expressive high-level transformation languages.

We take a step towards that goal, by developing a general symbolic execution technique that handles programs written in these high-level transformation languages. We use logical constraints to describe structured symbolic values, including containment, acyclicity, simple unordered collections (sets) and to handle deep type-based querying of syntax hierarchies.

We evaluate this symbolic execution technique on a collection of refactoring and model transformation programs, showing that the white-box test generation tool based on symbolic execution obtains better code coverage than a black box test generator for such programs in almost all tested cases.

Joint work with Aleksandar S. Dimovski and Andrzej Wasowski

Slides available as .pdf

Proving Equivalence of Imperative Programs via Constrained Rewriting Induction

Cynthia Kop

University of Copenhagen

This talk is about a method to prove correctness of imperative programs by using a translation to term rewriting. We will discuss LCTRSs---term rewriting systems with logical constraints---and show how typical C-functions can be translated into LCTRSs. Then we show how we can use rewriting induction to inductively prove equivalence between two different functions. We can use this to show the correctness of an implementation compared to a specification, to show equivalence between two specifications, and to automatically verify memory safety; all considering realistic functions, involving for instance integers and arrays.

Slides available as .pdf