I am an assistant professor at the Department of Computer Science in the Database, Programming, and Web Technologies group at Aalborg University. I was previously 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 email is my first name at cs.aau.dk.
Flix is a statically typed functional- and logic programming language inspired by Scala, OCaml, F#, Haskell, and Datalog. The syntax of Flix resembles Scala and Datalog. The type system supports local type inference and is based on Hindley-Milner. Flix runs on the Java Virtual Machine and compiles directly to JVM bytecode.
Flix supports hybrid functional and logic programming featuring a built-in fixed point engine based on semi-naive evaluation. The functional and logic languages can be used independently, if so desired. For example, a Flix program can be purely functional, or Flix can be used as a standalone Datalog engine.
Papers related to this line of research include:
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
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
Magnus Madsen, Ondřej Lhoták, Frank Tip
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
Magnus Madsen, Frank Tip, Esben Andreasen, Koushik Sen, Anders Møller
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
Magnus Madsen, Frank Tip, Ondřej Lhoták
Magnus Madsen, Anders Møller
Magnus Madsen, Esben Andreasen
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
Magnus Madsen, Benjamin Livshits, Michael Fanning
Simon Holm Jensen, Magnus Madsen, Anders Møller
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
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 algorithmsPaper BibTex