DANSAS 2016, Odense, August 19
|09:00 - 09:30||Coffee and breakfast rolls|
|09:30 - 09:40||Welcome|
|09:40 - 10:25||SMT Techniques and Solvers in Automated Termination Analysis (invited talk)|
|10:30 - 11:00||Fruit Break|
|11:00 - 11:25||From Datalog to Flix: A Declarative Language for Fixed Points on Lattices|
|11:35 - 12:00||Static Analysis for Security, Privacy and Mechanism Design|
|12:05 - 13:35||Lunch|
|13:35 - 14:00||Type Unsoundness in Practice: An Empirical Study of Dart|
|14:10 - 14:35||Trace Typing: An Approach for Evaluating Retrofitted Type Systems|
|14:45 - 15:10||Analyzing Test Completeness for Dynamic Languages|
|15:15 - 15:45||Coffee Break|
|15:45 - 16:10||Symbolic Execution of High-Level Transformations|
Ahmad Salim Al-Sibahi
|16:20 - 16:45||Proving Equivalence of Imperative Programs via Constrained Rewriting Induction|
|16:50 - 17:00||Wrap-up and evaluation|
SMT Techniques and Solvers in Automated Termination Analysis
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.
From Datalog to Flix: A Declarative Language for Fixed Points on Lattices
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.
Static analysis for security, privacy and mechanism design
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.
Type Unsoundness in Practice: An Empirical Study of Dart
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
Trace Typing: An Approach for Evaluating Retrofitted Type Systems
Joint work with Colin S. Gordon, Satish Chandra, Manu Sridharan, Frank Tip and Koushik Sen
Analyzing Test Completeness for Dynamic Languages
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
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
Proving Equivalence of Imperative Programs via Constrained Rewriting Induction
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.