Magnus Madsen

I am an assistant professor at the Department of Computer Science at Aarhus University. I was previously assistant professor at Aalborg University. Before that, I was a postdoctoral researcher at the University of Waterloo in the Programming Languages Group under the supervision of Ondřej Lhoták. I received my PhD from Aarhus University for the thesis Static Analysis of Dynamic Languages. My thesis adviser was Anders Møller.

My full curriculum vitae (typically outdated). My Google Scholar. My DBLP. My GitHub.

My email is magnusm followed by an at sign followed by cs.au.dk

My primary research interests are in programming language design, compilers, and program analysis.

PC Member: PLDI '21, SCAM '20, SSEPLC '20, ICOOOLPS '20, MPLR '19, ECOOP '18.

External Reviewer: TOPLAS '19, CSUR '19, OOPSLA '15, TFP '13

Peer-Reviewed Publications

  • Fixpoints for the Masses: Programming with First-Class Datalog Constraints (OOPSLA '20)

    Magnus Madsen, Ondřej Lhoták

    Datalog is a declarative logic programming language that has been used in a variety of applications, including big-data analytics, language processing, networking and distributed systems, and program analysis.

    In this paper, we propose fjrst-class Datalog constraints as a mechanism to construct, compose, and solve Datalog programs at run time. The benefits are twofold: We gain the full power of a functional programming language to operate on Datalog constraints-as-values, while simultaneously we can use Datalog where it really shines: to declaratively express and solve fixpoint problems.

    We present an extension of the lambda calculus with first-class Datalog constraints, including its semantics and a type system with row polymorphism based on Hindley-Milner. We prove soundness of the type system and implement it as an extension of the Flix programming language.

    Paper
  • Polymorphic Types and Effects with Boolean Unification (OOPSLA '20)

    Magnus Madsen, Jaco van de Pol

    We present a simple, practical, and expressive type and effect system based on Boolean constraints. The effect system extends the Hindley-Milner type system, supports parametric polymorphism, and preserves principal types modulo Boolean equivalence. We show how to support type inference by extending Algorithm W with Boolean unification based on the successive variable elimination algorithm.

    We implement the type and effect system in the Flix programming language. We perform an in-depth evaluation on the impact of Boolean unification on type inference time and end-to-end compilation time. While the computational complexity of Boolean unification is NP-hard, the experimental results demonstrate that it works well in practice. We find that the impact on type inference time is on average a 1.4x slowdown and the overall impact on end-to-end compilation time is a 1.1x slowdown.

    Paper
  • Fuzzing Channel-Based Concurrency Runtimes using Types and Effects (OOPSLA '20)

    Quentin Stievenart, Magnus Madsen

    Modern programming languages support concurrent programming based on channels and processes. Channels enable synchronous and asynchronous message-passing between independent light-weight processes making it easy to express common concurrency patterns.

    The implementation of channels and processes in compilers and language runtimes is a difficult task that relies heavily on traditional and error-prone low-level concurrency primitives, raising concerns about correctness and reliability.

    In this paper, we present an automatic program generation technique to test such programming language implementations. We define a type and effect system for programs that communicate over channels and where every execution is guaranteed to eventually terminate. We can generate and run such programs, and if a program fails to terminate, we have found a bug in the programming language implementation.

    We implement such an automatic program generator and apply it to Go, Kotlin, Crystal, and Flix. We find two new bugs in Flix, and reproduce two bugs; one in Crystal and one in Kotlin

    Paper
  • A Semantics for the Essence of React (ECOOP '20)

    Magnus Madsen, Ondřej Lhoták, Frank Tip

    Traditionally, web applications have been written as HTML pages with embedded JavaScript code that implements dynamic and interactive features by manipulating the Document Object Model (DOM) through a low-level browser API. However, this unprincipled approach leads to code that is brittle, difficult to understand, non-modular, and does not facilitate incremental update of user-interfaces in response to state changes.

    React is a popular framework for constructing web applications that aims to overcome these problems. React applications are written in a declarative and object-oriented style, and consist of components that are organized in a tree structure. Each component has a set of properties representing input parameters, a state consisting of values that may vary over time, and a render method that declaratively specifies the subcomponents of the component. React’s concept of reconciliation determines the impact of state changes and updates the user-interface incrementally by selective mounting and unmounting of subcomponents. At designated points, the React framework invokes lifecycle hooks that enable programmers to perform actions outside the framework such as acquiring and releasing resources needed by a component.

    These mechanisms exhibit considerable complexity, but, to our knowledge, no formal specification of React’s semantics exists. This paper presents a small-step operational semantics that captures the essence of React, as a first step towards a long-term goal of developing automatic tools for program understanding, automatic testing, and bug finding for React web applications. To demonstrate that key operations such as mounting, unmounting, and reconciliation terminate, we define the notion of a well-behaved component and prove that well-behavedness is preserved by these operations.

    Paper
  • Finding Broken Promises in Asynchronous JavaScript Programs (OOPSLA '18)

    Saba Alimadadi, Di Zhong, Magnus Madsen, Frank Tip

    Recently, promises were added to ECMAScript 6, the JavaScript standard, in order to provide better support for the asynchrony that arises in user interfaces, network communication, and non-blocking I/O. Using promises, programmers can avoid common pitfalls of event-driven programming such as event races and the deeply nested counterintuitive control flow referred to as callback hell. Unfortunately, promises have complex semantics and the intricate controls and data-flow present in promise-based code hinders program comprehension and can easily lead to bugs. The promise graph was proposed as a graphical aid for understanding and debugging promise-based code. However, it did not cover all promise-related features in ECMAScript 6, and did not present or evaluate any technique for constructing the promise graphs.

    In this paper,we extend the notion of promise graphs to include all promise-related features in ECMAScript6, including default reactions, exceptions, and the synchronization operations race and all. Furthermore, we report on the construction and evaluation of PromiseKeeper, which performs a dynamic analysis to create promise graphs and infer common promise anti-patterns. We evaluate PromiseKeeper by applying it to 12 open source promise-based Node.js applications. Our results suggest that the promise graphs constructed by PromiseKeeper can provide developers with valuable information about occurrences of common anti-patterns in their promise-based code, and that promise graphs can be constructed with acceptable run-time overhead.

    Paper
  • Implicit Parameters for Logic Programming (PPDP '18)

    Magnus Madsen, Ondřej Lhoták

    Implicit parameters allow programmers to omit certain arguments from function calls and have them automatically inferred by the compiler based on their types. At every call site, the compiler determines the values of the implicit parameters based on their declared types and the bindings currently in implicit scope. The programmer controls this mechanism in two ways: by adding bindings to the implicit scope, or by explicitly providing the implicit parameters for the function call

    Implicit parameters are known from functional and object- oriented languages such as Haskell and Scala. In recent years, more languages have added support for implicit parameters, including Agda, Coq, and Idris. Implicit parameters have played an impressive role as the foundation for a broad range of language features such as type classes, capability and effect systems, software transactional memory, macros, and more.

    In this paper, we propose a design of implicit parameters for typed Horn clause based logic programming languages, such as Datalog and Prolog. We illustrate the usefulness of implicit parameters and show how they support logic programming in the large. We explore some of the differences that arise between implicit parameters in functional languages and in logic languages.

    Paper BibTex
  • Safe and Sound Program Analysis with Flix (ISSTA '18)

    Magnus Madsen, Ondřej Lhoták

    Program development tools such as bug finders, build automation tools, compilers, debuggers, integrated development environments, and refactoring tools increasingly rely on static analysis techniques to reason about program behavior. Implementing such static analysis tools is a complex and difficult task with concerns about safety and soundness. Safety guarantees that the fixed point computation – inherent in most static analyses – converges and ultimately terminates with a deterministic result. Soundness guarantees that the computed result over-approximates the concrete behavior of the program under analysis. But how do we know if we can trust the result of the static analysis itself? Who will guard the guards?

    In this paper, we propose the use of automatic program verification techniques based on symbolic execution and SMT solvers to verify the correctness of the abstract domains used in static analysis tools. We implement a verification toolchain for Flix, a functional and logic programming language tailored for the implementation of static analyses. We apply this toolchain to several abstract domains. The experimental results show that we are able to prove 99.5% and 96.3% of the required safety and soundness properties, respectively.

    Paper BibTex
  • Tail Call Elimination and Data Representation for Functional Languages on the Java Virtual Machine (CC '18)

    Magnus Madsen, Ramin Zarifi, Ondřej Lhoták

    The Java Virtual Machine (JVM) offers an attractive runtime environment for programming language implementors. The JVM has a simple bytecode format, excellent performance, multiple state-of-the art garbage collectors, robust backwards compatibility, and it runs on almost all platforms. Further, the Java ecosystem grants access to a plethora of libraries and tooling, including debuggers and profilers.

    Yet, the JVM was originally designed for Java, and its representation of code and data may cause difficulties for other languages. In this paper, we discuss how to efficiently implement functional languages on the JVM. We focus on two overall challenges: (a) how to efficiently represent algebraic data types in the presence of tags and tuples, option types, newtypes, and parametric polymorphism, and (b) how to support full tail call elimination on the JVM.

    We present two technical contributions: A fused representation of tags and tuples and a full tail call elimination strategy that is thread-safe. We implement these techniques in the Flix language and evaluate their performance.

    Paper BibTex
  • A Model for Reasoning About JavaScript Promises (OOPSLA '17)

    Magnus Madsen, Ondřej Lhoták, Frank Tip

    In JavaScript programs, asynchrony arises in situations such as web-based user-interfaces, communicating with servers through HTTP requests, and non-blocking I/O. Event-based programming is the most popular approach for managing asynchrony, but suffers from problems such as lost events and event races, and results in code that is hard to understand and debug. Recently, ECMAScript 6 has added support for promises, an alternative mechanism for managing asynchrony that enables programmers to chain asynchronous computations while supporting proper error handling. However, promises are complex and error-prone in their own right, so programmers would benefit from techniques that can reason about the correctness of promise-based code.

    Since the ECMAScript 6 specification is informal and intended for implementers of JavaScript engines, it does not provide a suitable basis for formal reasoning. This paper presents lambda_p, a core calculus that captures the essence of ECMAScript 6 promises. Based on lambda_p, we introduce the promise graph, a program representation that can assist programmers with debugging of promise-based code. We then report on a case study in which we investigate how the promise graph can be helpful for debugging errors related to promises in code fragments posted to the StackOverflow website.

    Paper BibTex
  • From Datalog to Flix: A Declarative Language for Fixed Points on Lattices (PLDI '16)

    Magnus Madsen, Ming-Ho Yee, Ondřej Lhoták

    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 asa 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-naive 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.

    Paper BibTex Website
  • Feedback-Directed Instrumentation for Deployed JavaScript Applications (ICSE '16)

    Magnus Madsen, Frank Tip, Esben Andreasen, Koushik Sen, Anders Møller

    Many bugs in JavaScript applications manifest themselves as objects that have incorrect property values when a failure occurs. For this type of error, stack traces and log files are often insufficient for diagnosing problems. In such cases, it is helpful for developers to know the control flow path from the creation of an object to a crashing statement. Such crash paths are useful for understanding where the object originated and whether any properties of the object were corrupted since its creation.

    We present a feedback-directed instrumentation technique for computing crash paths that allows the instrumentation overhead to be distributed over a crowd of users and to reduce it for users who do not encounter the crash. We implemented our technique in a tool, Crowdie, and evaluated it on 10 real-world issues for which error messages and stack traces are insufficient to isolate the problem. Our results show that feedback-directed instrumentation requires 5% to 25% of the program to be instrumented, that the same crash must be observed 3 to 10 times to discover the crash path, and that feedback-directed instrumentation typically slows down execution by a factor 2x–9x compared to 8x–90x for an approach where applications are fully instrumented.

    Paper BibTex
  • Static Analysis of Event-Driven Node.js JavaScript Applications (OOPSLA '15)

    Magnus Madsen, Frank Tip, Ondřej Lhoták

    Many JavaScript programs are written in an event-driven style. In particular, in server-side Node.js applications, operations involving sockets, streams, and files are typically performed in an asynchronous manner, where the execution of listeners is triggered by events. Several types of programming errors are specific to such event-based programs (e.g., unhandled events, and listeners that are registered too late). We present the event-based call graph, a program representation that can be used to detect bugs related to event handling. We have designed and implemented three analyses for constructing event-based call graphs. Our results show that these analyses are capable of detecting problems reported on StackOverflow. Moreover, we show that the number of false positives reported by the analysis on a suite of small Node.js applications is manageable.

    Paper BibTex
  • Sparse Dataflow Analysis with Pointers and Reachability (SAS '14)

    Magnus Madsen, Anders Møller

    Many static analyzers exploit sparseness techniques to reduce the amount of information being propagated and stored during analysis. Although several variations are described in the literature, no existing technique is suitable for analyzing JavaScript code. In this paper, we point out the need for a sparse analysis framework that supports pointers and reachability. We present such a framework, which uses static single assignment form for heap addresses and computes def-use information on-the-fly. We also show that essential information about dominating definitions can be maintained efficiently using quadtrees. The framework is presented as a systematic modification of a traditional dataflow analysis algorithm.

    Our experimental results demonstrate the effectiveness of the technique for a suite of JavaScript programs. By also comparing the performance with an idealized staged approach that computes pointer information with a pre-analysis, we show that the cost of computing def-use information on-the-fly is remarkably small.

    Paper BibTex
  • String Analysis for Dynamic Field Access (CC '14)

    Magnus Madsen, Esben Andreasen

    In JavaScript, and scripting languages in general, dynamic field access is a commonly used feature. Unfortunately, current static analysis tools either completely ignore dynamic field access or use overly conservative approximations that lead to poor precision and scalability. We present new string domains to reason about dynamic field access in a static analysis tool. A key feature of the domains is that the equal, concatenate and join operations take O(1) time.

    Experimental evaluation on four common JavaScript libraries, including jQuery and Prototype, shows that traditional string domains are insufficient. For instance, the commonly used constant string domain can only ensure that at most 21% dynamic field accesses are without false positives. In contrast, our string domain H ensures no false positives for up to 90% of all dynamic field accesses.

    We demonstrate that a dataflow analysis equipped with the H domain gains significant precision resulting in an analysis speedup of more than 1.5x for 7 out of 10 benchmark programs.

    Paper BibTex
  • Practical Static Analysis of JavaScript Applications in the Presence of Frameworks and Libraries (FSE/ESEC '13)

    Magnus Madsen, Benjamin Livshits, Michael Fanning

    JavaScript is a language that is widely-used for both web- based and standalone applications such as those in the Windows 8 operating system. Analysis of JavaScript has long been known to be challenging due to the language’s dynamic nature. On top of that, most JavaScript applications rely on large and complex libraries and frameworks, often written in a combination of JavaScript and native code such as C and C++. Stubs have been commonly employed as a partial specification mechanism to address the library problem; alas, they are tedious and error-prone.

    However, the manner in which library code is used within applications often sheds light on what library APIs return or pass into callbacks declared within the application. In this paper, we propose a technique which combines pointer analysis with a novel use analysis to handle many challenges posed by large JavaScript libraries. Our techniques have been implemented and empirically validated on a set of 25 Windows 8 JavaScript applications, averaging 1,587 lines of code, together with about 30,000 lines of library code, demonstrating a combination of scalability and precision

    Paper BibTex
  • Modeling the HTML DOM and Browser API in Static Analysis of JavaScript Web Applications (FSE/ESEC '11)

    Simon Holm Jensen, Magnus Madsen, Anders Møller

    Developers of JavaScript web applications have little tool support for catching errors early in development. In comparison, an abundance of tools exist for statically typed languages, including sophisticated integrated development environments and specialized static analyses. Transferring such technologies to the domain of JavaScript web applications is challenging. In this paper, we discuss the challenges, which include the dynamic aspects of JavaScript and the complex interactions between JavaScript, HTML, and the browser. From this, we present the first static analysis that is capable of reasoning about the flow of control and data in modern JavaScript applications that interact with the HTML DOM and browser API.

    One application of such a static analysis is to detect type- related and dataflow-related programming errors. We report on experiments with a range of modern web applications, including Chrome Experiments and IE Test Drive applications, to measure the precision and performance of the technique. The experiments indicate that the analysis is able to show absence of errors related to missing object properties and to identify dead and unreachable code. By measuring the precision of the types inferred for object properties, the analysis is precise enough to show that most expressions have unique types. By also producing precise call graphs, the analysis additionally shows that most invocations in the programs are monomorphic. We furthermore study the usefulness of the analysis to detect spelling errors in the code. Despite the encouraging results, not all problems are solved and some of the experiments indicate a potential for improvement, which allows us to identify central remaining challenges and outline directions for future work.

    Paper BibTex

Workshop and Other Publications

  • Programming a Dataflow Analysis in Flix (TAPAS '16)

    Magnus Madsen, Ming-Ho Yee, Ondřej Lhoták

    Flix is a logic and functional language designed for the implementation of static analysis tools. Flix is inspired by Datalog and extends it with user-defined lattices as well as monotone filter and transfer functions. In recent work, Flix has been used to express several analyses, including the Strong Update analysis, and the IFDS and IDE algorithms

    Paper BibTex