Research

While prior work on coalition theories focuses either solely on office or on policy motivations of parties, more elaborate theories combine both types of motivation. Said combination makes them much more appropriate for explaining coalition formation but also more complex. One possibility to make these models broadly applicable are coalition tools. Since existing tools do not incorporate advances from such theories, we present a new coalition tool called Coalizer which takes both office and policy motivations into account and reflects the state of coalition theory. Among others, Coalizer includes features like the computation of policy utility values basing on party positions (supporting different estimation modes), the combination of office and policy utility values, and the indication of utility maximizing strategies for parties. In this paper, we present our coalition tool and illustrate its functionality with the example of the German federal elections in 2017. Coalizer is available online at www.mytuc.org/mcbz.

Program verifiers statically check programs based on source code annotations such as invariants, pre- and postconditions. These annotations can be more precise than simple types. For example, a sorting routine might be annotated with a postcondition stating that its result is sorted.

However, the verification process for these annotations can become complex. Therefore, simple error messages may not be sufficient to help the programmer resolve verification issues. In order to improve the programming experience for verified programming, this paper presents IDVE, an integrated development and verification environment that lets users interactively inspect and debug verification issues. The goal of IDVE is to provide a development tool that assists users with program verification analogous to how interactive step-by-step debugging avoids manual 'printf debugging'. IDVE enables programmers to interactively manipulate assumptions and assertions of verification conditions with a novel verification inspector, and IDVE automatically generates tests that serve as executable and debuggable counterexamples.

In addition to presenting the approach and implementation of the integrated development and verification environment, we also conducted a user study with 18 participants to evaluate how the proposed features of the environment are perceived. Participants with and without prior experience with program verifiers had to solve a series of simple programming and verification tasks and answer an online survey. Features of IDVE were generally seen as helpful or potentially helpful but user interface design is an essential factor for their utility.

This dissertation includes contributions to both live programming and program verification and explores how programming environments can be designed to leverage benefits of both concepts in an integrated way.

Programming environments assist users in both writing program code and understanding program behavior. A fast feedback loop can significantly improve this process. In particular, live programming provides continuous feedback for live code updates of running programs. This idea can also be applied to program verification. In general, verifiers statically check programs based on source code annotations such as invariants, pre- and postconditions. However, verification errors are often hard to understand, so programming environment integration is crucial for supporting the development process.

The research for this dissertation involved the implementation of esverify, a program verifier for JavaScript, as well as prototype implementations of multiple programming environments. These implementations demonstrate potential benefits and limitations of proposed solutions and enable empirical evaluation with case and user studies. Additionally, the proposed designs were formally defined in order to explain the core idea in a concise way and to prove properties independent of concrete specifics of existing systems and programming languages.

The resulting systems represent possible solutions in a vast design space with various contributions. The research on live programming showed that a programming model that separates event handling from output rendering enables not only live code updates but also runtime version control and programming-by-example. For program verification, esverify represents a novel approach for static verification of both higher-order functional programs and dynamically-typed programming idioms. esverify can verify nontrivial algorithms such as MergeSort and a formal proof in the Lean theorem prover shows that its verification rules are sound. Finally, a programming environment based on esverify supports inspection and live edits of verification conditions including step-by-step debugging of automatically generated tests that serve as executable counterexamples. As part of a user study, participants used these features effectively to solve programming tasks and generally found them to be helpful or potentially helpful.

Program verifiers statically check correctness properties of programs with annotations such as assertions and pre- and postconditions. Recent advances in SMT solving make it applicable to a wide range of domains, including program verification. In this paper, we describe esverify, a program verifier for JavaScript based on SMT solving, supporting functional correctness properties comparable to languages with refinement and dependent function types. esverify supports both higher-order functions and dynamically-typed idioms, enabling verification of programs that static type systems usually do not support. To verify these programs, we represent functions as universal quantifiers in the SMT logic and function calls as instantiations of these quantifiers. To ensure that the verification process is decidable and predictable, we describe a bounded quantifier instantiation algorithm that prevents matching loops and avoids ad-hoc instantiation heuristics. We also present a formalism and soundness proof of this verification system in the Lean theorem prover and a prototype implementation.

While prior work on coalition theories focuses either solely on office or on policy motivations of parties, more recent theories combine both types of motivation. They are therefore much more appropriate for explaining coalition formation but, at the same time, they are also more complicated. One possibility to make these models broadly applicable are coalition tools. However, existing tools do not incorporate advances from more recent theories and are, for example, confined to the identification of minimal winning coalitions. In this paper, we present a new coalition tool called Coalizer which takes both office and policy motivations into account and reflects the state of coalition theory. As data input, Coalizer needs the seat distribution in a parliament as well as information on party positions. While the latter can come from various sources, Coalizer is explicitly targeted at multi-issue data as it is provided by voting advice applications for many elections. Coalizer is, to the best of our knowledge, the most comprehensive coalition tool and includes, among others, the following features: identification of (minimal) winning coalitions, computation of office utility values basing on seat distributions, computation of policy utility values basing on party positions, visualization of party distances, a weighted combination of office and policy utility values, and showing utility maximizing strategies for parties and equilibria based on the combined utility values. In our paper, we i) sketch the recent coalition theories on which Coalizer is based, ii) describe the functionality of our coalition tool, and iii) evaluate Coalizer at the example of the German federal elections in 2017.

To provide a better programming experience, live programming environments allow changes to the code of running programs. These changes are usually made by editing the source code. In this paper, we introduce live programming by example which enables updates to the code by direct manipulation of the program’s user interface. Besides a formal definition of live programming by example, we also present a concrete prototype implementation for JavaScript that enables the programmer to change string literals in the source code by direct manipulation of the HTML output based on a dynamic string origin analysis. While this prototype only supports light-weight synthesis, future live program synthesis algorithms could support a wider range of program edits.

Refactoring is a code transformation performed at development time that improves the quality of code while preserving its observable behavior. Macro expansion is also a code transformation, but performed at compile time, that replaces instances of macro invocation patterns with the corresponding macro body or template. The key insight of this paper is that for each pattern-template macro, we can automatically generate a corresponding refactoring tool that finds complex code fragments matching the macro template and replaces them with the equivalent but simpler macro invocation pattern; we call this novel refactoring process "macrofication". Conceptually, macrofication involves running macro expansion in reverse; however, it does require a more sophisticated pattern matching algorithm and additional checks to ensure that the refactoring always preserves program behavior. We have implemented a macrofication tool for a hygienic macro system in JavaScript, integrated it into a development environment and evaluated it by refactoring a popular open source JavaScript library. Results indicate that it is sufficiently flexible for complex refactoring and thereby enhances the development workflow while scaling well even for larger code bases.

Reactive Programming enables declarative definitions of time-varying values (signals) and their dependencies in a way that changes are automatically propagated. In order to use reactive programming in an imperative object-oriented language, signals are usually modelled as objects. However, computations on primitive values then have to lifted to signals which usually involves a verbose notation. Moreover, it is important to avoid cycles in the dependency graph and glitches, both of which can result from changes to mutable global state during change propagation. This paper introduces reactive variables as extension to imperative languages. Changes to reactive variables are automatically propagated to other reactive variables but, in contrast to signals, reactive variables cannot be reified and used as values. Instead, references to reactive variables always denote their latest values. This enables computation without explicit lifting and limits the dependents of a reactive variable to the lexical scope of its declaration. The dependency graph is therefore topologically ordered and acyclic. Additionally, reactive updates are prevented from mutating global state to ensure consistency. We present a working prototype implementation in JavaScript based on the sweet.js macro system and a formalism for integration with general imperative languages.

Live programming environments assist programmers by allowing code edits to running programs, providing continuous feedback and potentially even traveling back in time to past execution states. Event-based languages like JavaScript facilitate these features, but the entanglement of code, state and output still hinders live programming. This paper shows how hot swapping, time travel and continuous feedback can be achieved by restricting standard JavaScript programs to have a single, pure rendering function and no function values in the global state. Furthermore, we describe this design for general event-based languages and how these properties can be enforced statically or dynamically.

While types describe what values an expression computes, the effects of an expression describe how it is computed, e.g. whether its evaluation manipulates global state, accesses the file system or may throw certain exceptions. Having to specify types and effects throughout the program might not be feasible in a scripting language but simple effect contracts may still help to prevent many programming errors. This paper described the design and implementation of a system that statically checks effect contracts in JavaScript programs.

Traditional debugging visualizes the execution state at a certain point in time. With omniscient debugging, it is possible to navigate and inspect the execution at different points in time. This demo present a prototype of a live coding environment that makes it easy to navigate the execution and extends omniscient debugging with an additional dimension in order to navigate to different versions of the code. While the implementation is still at an early state, the basic idea is promising for future research in debugging and programming.

Currently, Reflectance Transformation Imaging (RTI) technology is restricted to desktop and high performance computing devices. In recent years, mobile devices and tablets have become ubiquitous due to their increased performance. However, the size of RTI files (≈100 MB) limits the range of portable devices capable of displaying RTI files. In this paper, we explore different compression techniques, and develop an RTI viewer prototype for both Android and iOS devices. Experiments with JPEG, JPEG2000, lossless compression show the resulting error for compression ratios of 30:1 is comparable to the error of traditional two-dimensional images. For higher compression rates, we present a novel αβ-JPEG algorithm which compresses color and reflectance information individually.

As web pages evolve to complex software applications, the web authoring tools must evolve as well. The Lively system integrates development and deployment of applications into a collaborative, self-sustaining environment on the web. However, the JavaScript debugging tools in Lively are still incomplete due to the lack of a cross-browser debugging API that allows access to the runtime execution state without relying on plugins.

We achieved execution state reification by interpreting JavaScript on top of the underlying JavaScript VM. This does not affect the runtime performance of Lively because the interpreter is only used for code that explicitly requires access to the execution state. Seamless transitions between natively executed and interpreted code enable on-demand debugging with breakpoints and stepping.

The implementation of this approach showed that closures and other JavaScript features like dynamic evaluation cause problems when both modes of execution work together. These problems were solved for Lively by restricting these language features but a general purpose cross-browser debugger is topic of future work.

The behavior of mobile applications is particularly affected by their execution context, such as location and state a the mobile device. Among other approaches, context-oriented programming can help to achieve context-dependent behavior without sacrificing modularity or adhering to a certain framework or library by enabling fine-grained adaptation of default behavior per control-flow.

However, context information relevant for mobile applications is mostly defined by external events and sensor data rather than by code and control flow. To accommodate this, the JCop language provides a more declarative approach by pointcut-like adaptation rules.

In this paper, we explain how we applied JCop to the development of Android applications for which we extended the language semantics for static contexts and modified the compiler. Additionally, we outline the successful implementation of a simple, proof-of-concept mobile application using our approach and report on promising early evaluation results.