A picture of me

Hello! That’s me over there to the right. ☛

Finding me etc.


  • Quick specifications for the busy programmer with Moa Johansson, Koen Claessen and Maximilian Algehed, submitted to JFP. [draft pdf | website].

  • Find more bugs with QuickCheck! with John Hughes, Ulf Norell, Thomas Arts. Automation of Software Test 2016. [pdf | acm].

  • TIP: tools for inductive provers with Dan Rosén. LPAR 2015. [pdf | springer | website].

  • Linking Unit Tests and Properties with Alex Gerdes, John Hughes, Thomas Arts. Erlang workshop 2015. [paper | acm].

  • TIP: tons of inductive problems with Koen Claessen, Moa Johansson, Dan Rosén. CICM 2015. [pdf | springer | website].

  • Hipster: integrating theory exploration in a proof assistant, with Moa Johansson, Dan Rosén, Koen Claessen. CICM 2014 (awarded best paper, Calculemus track). [pdf | springer | arxiv | website].

  • An expressive semantics of mocking, with Josef Svenningsson, Hans Svensson, Thomas Arts, Ulf Norell, John Hughes. FASE 2014. [pdf | tech report | Agda source code | springer].

  • Encoding monomorphic and polymorphic types, with Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu. TACAS 2013.
    [pdf | draft report | springer]. Extended version in my thesis.

  • Automating inductive proofs using theory exploration (a.k.a. HipSpec), with Koen Claessen, Moa Johansson, Dan Rosén. CADE 2013.
    [pdf | springer]. Also in my thesis.

  • Accelerating race condition detection through procrastination, with Thomas Arts, John Hughes, Ulf Norell, Hans Svensson. Erlang Workshop 2011.
    [pdf | acm]. Extended version in my thesis.

  • Sort it out with monotonicity: translating between many-sorted and unsorted first-order logic (a.k.a. monkeys and bananas), with Koen Claessen, Ann Lillieström. CADE 2011.
    [pdf | springer | website]. Also in my thesis.

  • QuickSpec: guessing formal specifications using testing, with Koen Claessen, John Hughes. Tests and Proofs 2010.
    [pdf | acm | website]. Extended version in my thesis.

  • Ranking programs using black box testing, with Koen Claessen, John Hughes, Michał Pałka, Hans Svensson. Automation of Software Test 2010.
    [pdf | acm]. Extended version in my lic.

  • Finding race conditions in Erlang with QuickCheck and PULSE, with Thomas Arts, Koen Claessen, John Hughes, Michał Pałka, Hans Svensson, Ulf Wiger. ICFP 2009.
    [pdf | acm]. Extended version in my thesis.



I defended my thesis, "Lightweight verification of functional programs" [pdf], in May 2013. You can find extended versions of many of my publications in it.

Summary: there’s no point proving a program correct without testing it first, because a) the program will have bugs and b) the specification will have bugs. Let’s bring proof and testing closer together! If we write testable specifications, we can move smoothly between the two.


I teach the Data Structures course for GU students in period 4.