I am currently an Associate Professor (Docent) at the Departement of Computer Science and Engineering at Chalmers University in Gothenburg, Sweden. My research interests include an diverse mix of applications of AI: from maths and automated reasoning to sports science and natural language processing for political science.

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 (2009-2011). I did my PhD in the Mathematical Reasoning Group at the University of Edinburgh (graduated 2009).

## Research Projects

**Bias and methods of AI technology studying political behavior** (2020 - 2024)

Together with Annika Freden (KAU). This project is funded by WASP-HS and will
investigate how political scientist can use state-of-the-art AI technology
as a tool in their research. A project description can be found on the
WASP-HS site.
PhD student Denitsa Saynova is funded by this project.

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

Project grant for young researchers by
Vetenskapsrådet (the Swedish Research Council). This project
investigates how techniques we automatically can discover conjectures
about programs or mathematical structures using a technique called theory exploration.

**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

**TRACKS project course: Digitalisation in Sports** (Autumn 2020-)

I teach and supervise student projects primarily related to machine learning on sports data.

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

I lead a PhD-level seminar course about ethics and IT that
started in April 2015. Due to lack of funding, this course is not currently running.

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

This is an undergraduate course introducing students to
concepts in both testing and debugging, as well as formal
specification and program verification techniques.

## Publications

**Conjectures, Tests and Proofs: An Overview of Theory Exploration
**
Moa Johansson and Nicholas Smallbone.
Proceedings of 9th Workshop on Verification and Program Transformation, 2021.
[pdf]

**Template-based Theory Exploration: Discovering Properties of Functional Programs by Testing**
Solrun Halla Einarsdottir, Nicholas Smallbone and Moa Johansson.
Proceedings of IFL'20, 2021.
[pdf]

**Identifying cross country skiing techniques using power meters in ski poles.**
Moa Johansson, Marie Korneliusson and Nickey Lizbat Lawrence.
Proceedings of the Norwegian AI Society Symposium, 2019.
[pdf].

A longer version is also available at ArXiv.

**Lemma Discovery for Induction - A Survey**
Moa Johansson.
Proceedings of the Conference on Intelligent Computer Mathematics
(CICM). LNAI 11617, Springer, 2019.
[pdf]

**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.
[pdf]

**Towards Machine Learning on Data from Professional Cyclists.**
Agrin Hilmkil, Oscar Ivarsson, Moa Johansson, Dan Kuylenstierna, Teun van Erp.
World Congress on Performance Analysis in Sports, 2018.
[pdf]

**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. (Invited Talk)
[pdf]

**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

**Automated Conjecturing in QuickSpec.** Moa
Johansson and Nicholas Smallbone. 1st Mathematical Reasoning in
General Artificial Intelligence Workshop, ICLR 2021.
[pdf]

**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]