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)
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 -
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.
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.
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.
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]
Automated Discovery of Inductive Lemmas. Moa Johansson. School of Informatics, University of Edinburgh, 2009 [pdf]