I am currently an Associate Professor (Docent) in the Formal Methods division at the Departement of Computer Science and Engineering at Chalmers University in Gothenburg, Sweden. I am also the Director of the Chalmers MSc programme in Algorithms, Languages and Logic.

In the past, I've been a postdoc at the University of Verona in Italy. I did my PhD in the Mathematical Reasoning Group at the University of Edinburgh.

When I'm not doing science, I'll probably be riding my bike. I compete on the road for Giro Cycle Club. In 2018, I won a silver medal at the Swedish Championships in the time trial team competion. I sometimes write about our team's races here (in Swedish)

## Research Projects

**Learning and Exploration in Automated Theorem
Proving** (June 2015 - )

I was recently awarded a project grant for young researchers by
Vetenskapsrådet (the Swedish Research Council). The project will investigate how techniques
from machine learning can be used to gather useful information from
previous proofs when adressing new, similar problems.

**Automated Reasoning About Recursive Programs**
(Oct 2011 - June 2015)

This project was funded by a VINNMER Marie Curie Fellowship. It aimed at developing automated reasoning tools for
proving properties about recursive programs. Such properties needs
to be proved by induction, which in turn often requires discovery of
auxillary lemmas. We used theory exploration techniques
for this purpose, thus enhancing the power of an automated inductive
prover by automatically creating a richer background theory.
We implemented these ideas in the HipSpec system, which
is an automated inductive prover for Haskell.

**Reasoning for Program Analysis** (Oct 2009 -
Sept 2011)

I was a postdoc researcher at the University of Verona working with Maria Paola Bonacina. We developed a technique for computing interpolants from proofs in the superposition calculus and for DPLL(Gamma + T), which combines a first order superpositon prover with a SMT-sovler.

**Automated
Discovery of Inductive Lemmas** (Sept 2005 - June 2009)

For my PhD, I developed new
techniques for improving automation of inductive proofs in the IsaPlanner system. I
have implemented proof-critics that use information from failed proof
attempts to suggest patches, such as introducing a case-split or
finding missing lemmas. I have also implemented a system, called
IsaCoSy, for synthesising theorems about recursive datatypes
and functions. It can help form a useful background theory, reducing
the need to search for missing lemmas during later proofs.

**Best-First Rippling** (2004-2005)

I implemented a best-first version of the rippling heuristic in IsaPlanner for my final year undergraduate project.

## Teaching

**Ethics
and Philosophy of Computing** (Spring 2015)

I lead a PhD-level seminar course about ethics and IT that
started in April 2015.

**
Testing, Debugging and Verification** (2012-2014)

I was until recently teaching an undergraduate course introducing students to
concepts in both testing and debugging, as well as formal
specification and program verification techniques.

## Publications

**Into the Infinite - Theory Exploration for Coinduction.**
Solrun Halla Einarsdottir, Moa Johansson and Johannes Aman Pohjala.
Conference on Artificial Intelligence and Symbolic Computation (AISC), 2018 (to appear)

**QuickSpec: a lightweight theory exploration tool for programmers (system demonstration)**
Maximilian Algehed, Koen Claessen, Moa Johansson, Nicholas Smallbone
ACM SIGPLAN Notices 52 (10), p. 38-39, 2017.

**Automated Theory Exploration for Interactive Theorem Proving.**
Moa Johansson.
Conference on Interactive Theorem Proving (ITP), p. 1-11, 2017.

**Quick Specifications for the Busy Programmer.** Nicholas Smallbone, Moa
Johansson, Koen Claesson and Maximilian Algehed. Journal of Functional Programming, 2017.
Pre-print: [pdf]

**Proving Type Class Laws for Haskell.** Andreas Arvidsson, Moa
Johansson and Robin Touche. Post-proceedings of the Symposium for Trends in
Functional Programming 2016. [pdf]

**Conditional Lemma Discovery and Recursion Induction in Hipster.**
Irene Lobo Valbuena and Moa Johansson.
Proceedings of the International Workshop on Automated Verification of
Critical Systems (AVoCS). Electronic Communications of the EASST,
volume 72, 2015.
[pdf]

**TIP: Tons of Inductive Problems.**
Moa Johansson, Dan Rosén, Nicholas
Smallbone and Koen Claessen.
Proceedings of the Conference on Intelligent Computer Mathematics
(CICM) 2015. LNAI 9150, p. 333-337, 2015. [pdf].

**The Theory Behind TheoryMine.** Alan Bundy, Flaminia Cavallo,
Lucas Dixon, Moa Johansson and Roy McCasland. IEEE Intelligent
Systems, 30(4), p. 64-69, 2015.
[pre-print pdf].

**Interpolation Systems for Ground Proofs in Automated Deduction: A Survey.** Maria Paola
Bonacina and Moa Johansson. Journal of Automated Reasoning 54(4), p. 353-390,
Springer, 2015. [pdf]

**On Interpolation in Automated Theorem Proving.** Maria Paola
Bonacina and Moa Johansson. Journal of
Automated Reasoning 54(1), p. 69-97, Springer, 2015. [pdf]

**Hipster: Integrating Theory Exploration in a Proof Assistant.**
Moa Johansson, Dan Rosén, Nicholas
Smallbone and Koen Claessen.
Proceedings of the Conference on Intelligent Computer Mathematics
(CICM) 2014. LNCS 8543, p. 108-122. Springer. *Best paper award*. [pdf]

**Proof Pattern Recognition and Lemma Discovery in ACL2.** Jonathan
Heras, Ekaterina Komendantskaya, Moa Johansson and Ewen
Maclean. Proceedings of the International Conference on Logic for
Programming, Artificial Intelligence and Reasoning (LPAR) 2013. LNCS
8312, p. 389-406. Springer. [pdf]

**Automating Inductive Proofs using Theory Exploration.** Koen
Claessen, Moa Johansson, Dan Rosén and Nicholas
Smallbone. Proceedings of the Conference on Automated Deduction (CADE)
2013. LNCS 7898, p. 392-406. Springer.
[pdf].

**On Interpolation in Decision Procedures.** Maria Paola Bonacina
and Moa Johansson. Proceedings of TABLEUX, 2011. LNAI 6793,
p. 1-6. Springer [pdf]

**Towards Interpolation in an SMT-solver with Integrated Superposition.** Maria Paola Bonacina
and Moa Johansson. SMT Workshop, 2011, Snowbird Utah. [pdf]

**Conjecture Synthesis for Inductive Theories. ** Moa Johansson, Lucas Dixon and Alan Bundy. Journal of Automated Reasoning 47(3) p. 251-289, 2011.
[pdf].

**Dynamic Rippling, Middle-Out Reasoning and Lemma Discovery.** Moa
Johansson, Lucas Dixon and Alan Bundy. Verification, Induction,
Termination Analysis - Festschrift for Christoph Walther on the Occasion of His 60th Birthday, 2010. LNCS 6463, p. 102-116. Springer [pdf]

**Case-Analysis for Rippling and Inductive Proof. ** Moa Johansson, Lucas Dixon and Alan Bundy. Proceedings of the Interactive Theorem Proving Conference (ITP), 2010. LNCS 6172, p. 291-306. Springer [pdf]

**Best-First Rippling.** Moa Johansson, Alan Bundy and Lucas Dixon. Reasoning Action and Interaction in AI Theories and Systems - Essays Dedicated to Luigia Carlucci Aiello, p. 83-100, Springer Verlag, 2006.
Also presented at the STRATEGIES workshop at FLoC 2006 in Seattle. [pdf]

### Selected Workshops, Technical Reports and Draft Papers

**Learning and Exploration in Automated Theorem Proving.** Moa
Johansson. 6th International Workshop on Aritifical Intelligence for
Formal Methods (AI4FM), Edinburgh, UK. 2015. [pdf, 3 pages]

**Theory Exploration for Interactive Theorem Proving.** Moa
Johansson. 4th International Workshop on Aritifical Intelligence for
Formal Methods (AI4FM), at ITP Rennes, France. 2013. [pdf, 3 pages]

**HipSpec: Automating Inductive Proofs of Program Properties.**
Koen Claessen, Moa Johansson, Dan Rosén and Nicholas
Smallbone. Workshop on Automated Theory Exploration (ATX), at IJCAR Manchester,
UK, 2012.
[pdf]

**A Calculus for Conjecture Synthesis.** Moa Johansson, Lucas Dixon
and Alan Bundy. Workshop on Automated
Mathematical Theory Exploration (AUTOMATHEO), 2010.
[pdf].

**IsaCoSy: Synthesis of Inductive Theorems.** Moa Johansson, Lucas
Dixon and Alan Bundy. 1st International Workshop on Automated
Mathematical Theory Exploration (AUTOMATHEO), Hagenberg, Austria, 2009. [pdf, 4 pages]

**Proof Critics in IsaPlanner**. Moa Johansson. Isabelle Workshop 2007, Bremen, Germany. [pdf, pages 56 - 59]

**IsaPlanner 2: A Proof Planner in Isabelle.** Lucas Dixon and Moa
Johansson. School of Informatics Technical Report 1302, University of
Edinburgh, 2007 [pdf, 5 pages]

### PhD Thesis

**Automated Discovery of Inductive Lemmas.** Moa Johansson. School of Informatics, University of Edinburgh, 2009 [pdf]