465 papers · page 1 of 24
Modern software systems are increasingly concurrent, adaptive, and generative, yet our formal methods still focus primarily on describing what systems do rather than why particular behaviours arise. In this talk, I will present ongoing work on a causal calculus for concurrent sys…
The variability of product lines can exceed purely Boolean configuration spaces. Cardinality-based Feature Models (CFMs) are employed to model multi-instantiation of features along with individually configurable subtrees. Due to the added complexity, the analysis of CFMs cannot b…
Substructural type systems provide static guarantees about resource usage in programs. In most practical systems, however, the available usage constraints and their composition are predetermined by the language design, with only limited support for application programmers to cust…
In programmatic CAD (PCAD), 3D shapes are generally modelled either by position-based composition of simpler shapes, or by direct generation via path-based techniques (e.g., extrusions, sweeps, revolves). While state-of-the-art PCAD tools effectively support position-based modell…
In Haskell, accessing an object's fields requires deconstructing it. Thankfully, it is possible to name the fields of a data type using the record syntax, allowing programmers to access objects' fields using their name. This can help improve the readability of Haskell code. Howev…
We present Metis, a domain-specific language embedded in Haskell for two-player board games on rectangular boards that exploits their shared structure (setup, rules, win condition) through three composable mini-DSLs. Atomic operations for placing, moving, and capturing pieces com…
Rust has emerged as a popular systems language with growing interest in metaprogramming, yet it lacks staging support—developers must write unsafe, untyped macros instead. We present Stageleft, a library that brings type-safe staged programming to standard Rust without compiler m…
Synthesizing recursive functional programs over algebraic data types from input-output examples remains challenging, largely due to the explosion of structurally distinct candidates during search. We present a synthesis approach for structurally recursive list/tree transformation…
Large language models are increasingly used to make static analysis tools accessible through natural language, yet existing systems differ in how much they delegate to the LLM without treating the degree of delegation as an independent variable. We compare three architectures alo…
Access control is a classical way to express which users are allowed to do which actions on which objects. Many formalisms study how to model access control policies. However, fewer works target formal verification of an actual implementation with respect to a given policy. This …
Over the last three decades, multi-stage programming has been used to write high-level, type-safe, optimising code generators for a wide variety of domains, from database queries and stream processing to geometry, parsing, and differentiable programming.
This paper introduces a novel technique for synthesizing imperative programs that meet behavioral specifications given in the form of assumptions and assertions (logic formulas). In particular, we combine basic statement-directed enumerative search, static analysis via abstract i…
Since its introduction at GPCE2020, the eFLINT norm specification language has been used in academic and industrial applications to specify and automate compliance for various norms, such as privacy regulations and data processing agreements. The eFLINT interpreter has been used …
Automated Program Repair (APR) has advanced significantly with the emergence of pre-trained Code Language Models (CLMs), enabling the generation of high-quality patches. However, selecting the most suitable CLM for APR remains challenging due to a range of factors, including accu…
In software development, the efficiency and accuracy of code completion systems are crucial for productivity and codebase discovery. From simple spell checkers to advanced AI-powered tools, there are more ways to complete your code than ever. This results in an explosion in the n…
In software-defined networking, the domain-specific language P4 allows developers to program the behavior of networking devices at a comparatively high level of abstraction. A P4 program defines a state machine to parse incoming packets. The parsers are flexible and efficient but…
The class definitions and class field declarations in the ECMAScript standard suggest that the JavaScript engines could be optimized like class-based static languages. This paper focuses on two well-known optimizations. One is method specialization, using fixed offsets to access …
KSP is an imperative DSL in music production that enables realistic modelling of musical instruments in real-time using Kontakt as a runtime environment. Once a niche topic for hobbyists, the field has since professionalized, with Kontakt becoming an industry standard. Its script…
Staging dynamically typed programming languages safely is a challenge, as the programming-language support for staged computation typically relies on static type systems. To solve this problem, we propose a staged gradual type system that seamlessly integrates static and dynamic …
Design by Contract represents an established, lightweight paradigm for engineering reliable and robust software systems by specifying verifiable expectations and obligations between software components. Due to its laborious nature, developers hardly adopt Design by Contract in pr…