A picture of me

Hello! That’s (a younger version of) me over there to the right. ☛

I am a researcher at the functional programming division of the Computer Science and Engineering department at Chalmers University of Technology. My research often focuses on exploiting property-based testing (for example discovering, proving, and explaining properties); I also have a side-line in automated reasoning.

Finding me etc.

Publications

  • Conjectures, Tests and Proofs: An overview of theory exploration, with Moa Johansson. Accepted for VPT 2021. [pdf].

  • Twee: An Equational Theorem Prover (System Description). Accepted for CADE 2021. [pdf].

  • Template-based Theory Exploration: Discovering Properties of Functional Programs by Testing with Sólrún Halla Einarsdóttir, Moa Johansson. IFL 2020. [pdf].

  • Enhancing Temporal Logic Falsification with Specification Transformation and Valued Booleans with Johan Eddeland, Koen Claessen, Zahra Ramezani, Sajed Miremadi, Knut Åkesson. IEEE TCAD. [arxiv].

  • Testing Safety PLCs using QuickCheck with David Thönnessen, Martian Fabian, Koen Claessen, Stefan Kowalewski. IEEE CASE 2019. [pdf].

  • Safety at Speed: in-place array algorithms from pure functional programs by safely reusing storage with Markus Aronsson, Koen Claessen, Mary Sheeran. FHPNC 2019. [pdf].

  • Evaluating Two Semantics for Falsification using an Autonomous Driving Example with Zahra Ramezani, Martin Fabian, Knut Åkesson. INDIN 2019. [pdf].

  • Inferring morphological rules from small examples using 0/1 linear programming with Ann Lillieström, Koen Claessen. NoDaLiDa 2019. [pdf].

  • Understanding formal specifications through good examples with Alex Gerdes, John Hughes, Stefan Hanenberg, Sebastian Ivarsson, Meng Wang. Erlang Workshop 2018. [pdf].

  • Efficient encodings of first-order Horn formulas in equational logic with Koen Claessen. IJCAR 2018. [pdf].

  • Using valued Booleans to find simpler counterexamples in random testing of cyber-physical systems with Koen Claessen, Johan Eddeland, Zahra Ramezani and Knut Åkesson. Workshop on Discrete Event Systems. [pdf].

  • Quick specifications for the busy programmer with Moa Johansson, Koen Claessen and Maximilian Algehed. Journal of functional programming. [pdf | jfp | website].

  • Encoding monomorphic and polymorphic types, with Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu. Logical Methods in Computer Science. [pdf | lmcs].

  • 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 PhD 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 PhD 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 PhD 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 PhD thesis.
    Note: In the published version of the paper, Lemma 3 is false. The proof of Theorem 1 is incorrect, although the theorem itself is true. For a corrected version, see my PhD thesis.

  • QuickSpec: guessing formal specifications using testing, with Koen Claessen, John Hughes. Tests and Proofs 2010.
    [pdf | acm | website]. Extended version in my PhD 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 PhD thesis.

Some software

Miscellaneous