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.

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.

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.

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.

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 selective, sparse effect annotations may still help to prevent many programming errors. This paper described the design and implementation of a system that statically checks effects in otherwise dynamically-typed JavaScript programs.

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.

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. Demo The demo was originally presented at the Future Programming workshop 2014 [1]. It is publicly available at the following URL: http://vimeo.com/97714727 References [1] Jonathan Edwards, Richard P. Gabriel, and Alex Payne. Fpw’14: Future programming workshop. In Proceedings of the Companion Publication of the 2014 ACM SIGPLAN Conference on Systems, Programming, and Applications: Software for Humanity, SPLASH ’14, pages 77–77, New York, NY, USA, 2014. ACM. ISBN 978-1-4503-3208-8. doi: 10.1145/2660252.2663601. URL http://doi.acm.org/10.1145/2660252.2663601.

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.