I am 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 username on this machine at uwaterloo dot ca.
My primary research interests are in program analysis, both static and dynamic analysis, functional programming, and compiler implementation. Recently, I have also been working with logic programming and type systems. In static analysis, I have worked on points-to analysis, sparse dataflow analysis, string analysis, and various kinds of program artifact construction, including call graph, event-based graph, and promise graph construction. In dynamic analysis, I have worked on feedback-directed instrumentation where a program is incrementally instrumented over multiple runs to discover a so-called crash path leading from the creation of an object of interest to a crashing statement. For compiler implementation, I have worked on the design and implementation of the Flix language, discussed further below.
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, 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