Here we collect worldwide courses teaching formal methods
Course name: Software analysis
Course code, if applicable: INF.M062
University hosting the course: USI (Università della Svizzera italiana), Switzerland
Contact person Carlo A. Furia
Concepts taught: deductive verification, static analysis, type systems, model checking, predicate abstraction, symbolic execution, dynamic analysis
Tools used: Dafny and the Checker Framework (for the course's assignments). The course also includes brief demos of Frama-C, Spin, CPAchecker, and Klee
Year/Level: MSc (also available to PhD students)
Country: Luxembourg
Course code, if applicable:
University hosting the course: University of Luxembourg
Contact person Jun Pang, jun.pang
Concepts taught: transition systems, linear-time properties, omega-regular properties, Buchi automata, LTL, CTL, LTL model checking, CTL model checking
Tools used: Spin
Webpage:
https://wwwen.uni.lu/studies/fstc/bachelor_in_computer_science/programme
Year/level: 2
Country: Luxembourg
Course code, if applicable:
University hosting the course: University of Luxembourg
Contact person Jun Pang, jun.pang
Concepts taught: Alloy, process algebra, mu-calculus, model checking, mcrl2
Tools used: Alloy, mcrl2
Webpage: https://wwwen.uni.lu/studies/fstc/master_in_information_and_computer_sciences/programme
Year/Level: MSc
Country: US
Course code, if applicable: AERE/COMS 407/507
University hosting the course: Iowa State University (Ames, IA, USA)
Contact person Kristin Yvonne Rozier (kyrozier
Concepts taught: Logic Specifications, Temporal Logics (LTL, CTL), Explicit Model Checking, Symbolic Model Checking, Theorem Proving, Survey of state-of-the-art including the capabilities and limitations of applying formal methods for systems analysis, focusing on the aerospace domain
Tools used: Spin, SPOT, nuXmv, PVS
Webpage: http://temporallogic.org/courses/AppliedFormalMethods/
Country: France
Course code, if applicable:
University hosting the course: University of Rennes 1
Contact person Sandrine Blazy, Sandrine.Blazy
Concepts taught: deductive verification, pre and post-conditions, loop invariants, type invariants, ghost code
Tools used: Why3
Webpage:
https://formations.univ-rennes1.fr/formation/programmation-de-confiance?studentstatus=112
(in French)
Year/level: 3
Country: Portugal
Course code, if applicable: 11511
University hosting the course: University of Beira Interior
Contact person Simão Melo de Sousa (desousa
Concepts taught: Type Theory, Proof Assistant, Hoare Logic, deductive verification tools
Tools used: COQ, Why3
Year/Level: PhD
Country: UK
Course code, if applicable: 06-28201
University hosting the course: University of Birmingham
Contact person David Parker
Concepts taught: Modal logic, Temporal logic, Model checking, Real-time and probabilistic model checking
Tools used: Examples: Nu-SMV, SPIN, ProB,FDR, Z3, UPPAAL, PRISM, ProVerif
Webpage: https://www.cs.bham.ac.uk/internal/modules/2018/06-28201/
Country: UK
Course code, if applicable: COS6020-B
University hosting the course: University of Bradford
Contact person ???
Concepts taught: Classical logic, formal specification, model checking, reactive systems, program verification
Tools used:
Webpage: https://www.bradford.ac.uk/repos/modules/2020-21/cos6020-b.php
Country: UK
Course code, if applicable: CM30226
University hosting the course: Bath
Contact person ???
Concepts taught: Category theory, Simply typed lambda calculus, natural deduction, Curry-Howard isomorphism
Tools used:
Webpage: http://www.bath.ac.uk/catalogues/2011-2012/cm/CM30226.htm
Country: UK
Course code, if applicable: COMS30009
University hosting the course: University of Bristol
Contact person Steven Ramsay
Concepts taught: Lambda calculus, Programming Languages, Type systems
Tools used:
Webpage: https://www.bris.ac.uk/unit-programme-catalogue/UnitDetails.jsa?ayrCode=19%2F20&unitCode=COMS30009
Country: UK
Course code, if applicable: COM3028
University hosting the course: University of Surrey
Contact person Brijesh Dongol (b.dongol
Concepts taught: Modal logic, Temporal logic (LTL, CTL), Model checking, Hoare logic
Tools used: NuSMV, Dafny, MCMAS
Webpage: https://catalogue.surrey.ac.uk/2018-9/module/COM3028
Country: Germany Course code: TI5002
University hosting the course: THM Technische Hochschule Mittelhessen
Contact person Burkhardt Renz
Concepts taught: Propositional Logic, SAT-Solving, Predicate Logic, Linear Temporal Logic, Natural Deduction
Tools used: Logic Workbench (https://github.com/esb-lwb/lwb), Alloy, SPIN, Jape
Webpage: https://esb-dev.github.io/lfm.html
Country: UK
Course code, if applicable:
University hosting the course: Canvas MOOC Platform
Contact person Mohammad Reza Mousavi, mm789
Concepts taught: Formal Verification, Model Checking, Process Algebra, Behavioural Equivalences
Tools used: mCRL2 (www.mcrl2.org)
Webpage: https://www.canvas.net/browse/halmstad/courses/system-validation, https://ocw.tudelft.nl/courses/system-validation/
Year/Level: MSc
Country: Portugal
Course code, if applicable:
University hosting the course: Instituto Superior Técnico (University of Lisbon)
Contact person João F. Ferreira, joao
Concepts taught: Denotational Semantics, Operational Semantics, Axiomatic Semantics, Hoare Logic, Separation Logic, Interactive Theorem Proving, Functional Programming
Tools used: Coq, Haskell
Webpage: https://fenix.tecnico.ulisboa.pt/disciplinas/LPro26/2018-2019/2-semestre
Year/Level: MSc
Country: Netherlands
Course code, if applicable:
University hosting the course: Open University of the Netherlands
Contact person Stef Joosten, stef.joosten
Concepts taught: Specify an information system by means of constraints on a data space built up of relations.
Tools used: Ampersand (the tool)
Webpage: https://www.ou.nl/-/IM0403_Rule-Based-Design
Country: Netherlands
Course code, if applicable:
University hosting the course: TU Delft
Contact person Jeroen Keiren, j.j.a.keiren
Concepts taught: Labelled transition systems, process algebra, behavioural equivalences, mu-calculus, model checking, model based testing, ioco
Tools used: mCRL2
Webpage: https://studiegids.tudelft.nl/a101_displayCourse.do?course_id=45569
Year/Level: MSc
Country: Netherlands
Course code, if applicable:
University hosting the course: Eindhoven University of Technology
Contact person Jeroen Keiren, j.j.a.keiren
Concepts taught: UML, Labelled transition systems, LTL, timed automata, model-based testing, ioco
Tools used: starUML, UPPAAL
Country: Netherlands
Course code, if applicable:
University hosting the course: Eindhoven University of Technology
Contact person Bas Luttik, s.p.luttik
Concepts taught: Process calculus, structural operational semantics, various notions of bisimilarity, axiomatisation, soundness and completeness
Tools used: No tools
Webpage: https://canvas.tue.nl/courses/8829
Year/Level: MSc
Country: Netherlands
Course code, if applicable:
University hosting the course: Eindhoven University of Technology
Contact person Jan Friso Groote, J.F.Groote
Concepts taught: Behavioural equivalences, behavioural modelling, reasoning about processes, modal logics (modal mu-calculus), application to an industrial case study.
Tools used: mCRL2 (www.mcrl2.org)
Webpage: https://mitpress.mit.edu/books/modeling-and-analysis-communicating-systems
Year/Level: MSc
Country: Portugal
Course code, if applicable:
University hosting the course: University of Minho
Contact person Jose N. Oliveira, jno
Concepts taught: Formal specification, Modeling, Verification, Calculational design, Software architecture
Tools used: NuSMV, Alloy, mCRL2, Reo, UPPAAL, MiniSat, SMT-LIB, Why3, Coq, Frama-C, Dafny, CBMC, ANTLR, RAPL
Webpage: http://mei.di.uminho.pt/?q=en/mfes-en Year/level: MSc
Country: France
Course code, if applicable:
University hosting the course: Université Paris-Diderot
Contact person Claude Marché (Claude.Marche
Concepts taught: Hoare Logic, Weakest preconditions, handling procedure calls modularly, handling data structures, aliasing issues, separation logic
Tools used: Why3, Frama-C
Year/Level: MSc This course is at level MSc, more precisely at second year of Parisian Master in Computer Science
Country: Germany
Course code, if applicable:
University hosting the course: Bauhaus-Universität Weimar
Contact person Stefan Lucks, Stefan.Lucks
Concepts taught: Ada, tool-based testing, the theory and practice of static verification with SPARK, distributed systems
Tools used: -- gnat -- the SPARK toolset -- gps, emacs' Ada mode, ...
Country: Spain
Course code, if applicable:
University hosting the course: University of Málaga
Contact person María-del-Mar Gallardo, gallardo
Concepts taught: Model checking, alloy, uml/ocl
Tools used: Spin, alloy, use
Year/Level: 4
Country: Norway
Course code, if applicable:
University hosting the course: University of Oslo
Contact person Peter Ölveczky, peterol
Concepts taught:
Tools used: Maude
Webpage: https://www.uio.no/studier/emner/matnat/ifi/INF3232/index-eng.html
Year/Level: 2,3
Country: Sweden
Course code, if applicable: TDA567
University hosting the course: Chalmers University
Contact person Srinivas Pinisetty
Concepts taught: formal specification and verification of code
Tools used: Daphny
Webpage: http://www.cse.chalmers.se/edu/year/2017/course/TDA567/index.html
Country: Sweden
Course code, if applicable: TDA293
University hosting the course: Chalmers University
Contact person Wolfgang Ahrendt
Concepts taught: model checking, deductive verification, JML
Tools used: SPIN, KeY
Webpage: http://www.cse.chalmers.se/edu/year/2016/course/TDA293/index.html
Country: France
Course code, if applicable:
University hosting the course:
Contact person Allan Blanchard (mail
Concepts taught: Frama-C, Deductive proof, Proof of C programs
Tools used: Frama-C
Webpage: https://allan-blanchard.fr/publis/frama-c-wp-tutorial-en.pdf
Country: France
Course code, if applicable:
University hosting the course: University of Toulouse/INPT/ENSEEIHT
Contact person Marc Pantel (Marc.Pantel
Concepts taught: Logic, Induction, Hoare logic, Program proof, Language theory
Tools used: Coq, Why3
Webpage:
Year/Level: 3
Country: France
Course code, if applicable:
University hosting the course: University of Toulouse/INPT/ENSEEIHT
Contact person Marc Pantel (Marc.Pantel
Concepts taught: Software analysis tools (weakest precondition, model checking, abstract interpretation), Logic programming, Constraint Logic Programming, SAT, SMT
Tools used: Students develop small abstract interpreter, gnu prolog, miniSAT, Z3
Webpage:
Year/Level: MSc
Country: US
Course code, if applicable: CS 451/551
University hosting the course: Northern Arizona University
Contact person Frédéric Loulergue (frederic.loulergue
Concepts taught: operational semantics; axiomatic semantics; deductive verification; certified compilation; formalization in Coq; program analysis with Frama-C
Tools used: Coq, Frama-C
Year/Level: 4, MSc, PhD
Country: Portugal
Course code, if applicable:
University hosting the course: University of Beira Interior
Contact person Simao Melo de Sousa (desousa
Concepts taught: Deductive Program Verification, proof assistants, static program analysis
Tools used: COQ, Why3, frama-C
Webpage: http://www.di.ubi.pt/~desousa/CF/comfia.html, http://www.di.ubi.pt/~desousa/SFS/sfs.html
Year/Level: MSc, PhD
Course code, if applicable: 11480
University hosting the course: University of Beira Interior
Contact person Simao Melo de Sousa (desousa
Concepts taught: Deductive Program Verification, proof assistants, static program analysis
Tools used: COQ, Why3, frama-C
Webpage: http://www.di.ubi.pt/~desousa/CF/comfia.html, http://www.di.ubi.pt/~desousa/SFS/sfs.html
Year/Level: MSc
Course code: CSSE3100
Tools: KeY theorem prover
Country: France
Course code, if applicable:
University hosting the course: Université Paris-Diderot
Contact person Claude Marché (Claude.Marche
Concepts taught: Hoare Logic, Weakest preconditions, handling procedure calls modularly, handling data structures, aliasing issues, separation logic
Tools used: Why3, Frama-C
Year/Level: MSc This course is at level MSc, more precisely at second year of Parisian Master in Computer Science
Course code: CSSE3100
Tools: KeY theorem prover
Country: US
Course code, if applicable:
University hosting the course: Carnegie Mellon University
Contact person Bryan Parno (parno
Concepts taught: Software verification, systems, automation
Tools used: Z3, Dafny, Coq
Webpage: http://www.cs.cmu.edu/~15811/
Year/Level: PhD
Country: Italy
Course code, if applicable:
University hosting the course: Politecnico di Milano
Contact person Dino Mandrioli (dino.mandrioli
Concepts taught: Logics for specifying syteme; HOare's method; timed Petri nets, TRIO (a metric temporal logic for real-time systems). Case studies.
Tools used: Zot, a local model checker.
Webpage: http://home.deib.polimi.it/mandriol/Didattica/sitofms.html
Country: France
Course code, if applicable:
University hosting the course: Université Paris-Saclay
Contact person Andrei Paskevich and Julien Signoles (julien.signoles
Concepts taught: Hoare logic, WP calculus, formal specifications, memory models
Tools used: Frama-C (WP plug-in) and Why3
Webpage: https://www.lri.fr/~conchon/parcours_fiil/science_logiciel.html
Country: France
Course code, if applicable:
University hosting the course: Univ. Grenoble Alpes
Contact person Hubert Garavel & Laurence Pierre (hubert.garavel
Concepts taught: Applied formal methods
Tools used: many
Webpage: http://hecs.imag.fr
Year/Level: MSc
Country: UK
Course code, if applicable: COM00012H
University hosting the course: University of York
Contact person Jeremy Jacob, jeremy.jacob
Concepts taught: Model-oriented (Z) & process-oriented (CSP) specification & refinement
Tools used: CZT; FDR4
Webpage: (Behind a firewall) Year/level: 3
Country: Ireland
Course code, if applicable:
University hosting the course: University of Limerick
Contact person Tiziana Margaria, tiziana.margaria
Concepts taught: ormal models, logics and model checking
Tools used:
Webpage:
Country: New Zealand
Course code, if applicable: COMP426
University hosting the course: The University of Waikato
Contact person Judy Bowen, judy.bowen
Concepts taught: Formal specification of interactive systems
Tools used:
Webpage: https://paperoutlines.waikato.ac.nz/outline/COMP426-17B%20(HAM)
Country: New Zealand
Course code, if applicable: COMPX361
University hosting the course: The University of Waikato
Contact person Steve Reeves, stever
Concepts taught: Logic, program verification
Tools used:
Webpage: https:/papers.waikato.ac.nz/subjects/COMPX/COMPX361
Country: New Zealand
Course code, if applicable: COMP452
University hosting the course: The University of Waikato
Contact person Robi Malik, robi.malik
Concepts taught: Model checking
Tools used:
Webpage: https://paperoutlines.waikato.ac.nz/outline/COMP452-18A%20(HAM)
Country: New Zealand
Course code, if applicable: COMP454
University hosting the course: The University of Waikato
Contact person Steve Reeves, stever
Concepts taught: Formal specification using Z
Tools used:
Webpage: https://paperoutlines.waikato.ac.nz/outline/COMP454-17B%20(HAM)
Country: New Zealand
Course code, if applicable: SWEN421
University hosting the course: Victoria University Wellington
Contact person David Pearce, david.pearce
Concepts taught: Hoare Logic, software verification
Tools used:
Webpage: https://www.victoria.ac.nz/courses/swen/421/2018/offering?crn=18661
Country: New Zealand
Course code, if applicable: SWEN326
University hosting the course: Victoria University Wellington
Contact person David Pearce, david.pearce
Concepts taught: Software verification, model checking, static analysis
Tools used:
Webpage: https://www.victoria.ac.nz/courses/swen/326/2018/offering?crn=30042
Country: New Zealand
Course code, if applicable: SWEN324
University hosting the course: Victoria University Wellington
Contact person David Pearce, david.pearce
Concepts taught: Hoare Logic, software verification
Tools used:
Webpage: https://www.victoria.ac.nz/courses/swen/324/2018/offering?crn=30041
Country: Australia
Course code, if applicable: SWEN90010
University hosting the course: The University of Melbourne
Contact person Toby Murray, toby.murray
Concepts taught: Alloy, Hoare Logic, SPARK Ada
Tools used: Alloy
Webpage: https://handbook.unimelb.edu.au/2018/subjects/swen90010/
Year/Level: MSc
Country: Australia
Course code, if applicable: CITS5501
University hosting the course: The University of Western Australia
Contact person Arran Stewart, arran.stewart
Concepts taught: Alloy
Tools used: Alloy
Webpage: http://teaching.csse.uwa.edu.au/units/CITS5501/
Country: Australia
Course code, if applicable: COMP782
University hosting the course: Macquarie University
Contact person Annabelle McIver, annabelle.mciver
Concepts taught: Hoare Logic, verification
Tools used:
Webpage: http://handbook.mq.edu.au/2018/Units/ResearchUnit/COMP782
Country: Australia
Course code, if applicable: COMP781
University hosting the course: Macquarie University
Contact person Annabelle McIver, annabelle.mciver
Concepts taught: Hoare Logic, model checking
Tools used:
Webpage: http://handbook.mq.edu.au/2017/Units/ResearchUnit/COMP781
Country: Australia
Course code, if applicable: COMP1600
University hosting the course: Australian National University
Contact person Rajeev Gore, Rajeev.Gore
Concepts taught: formal specification, Hoare Logic
Tools used:
Webpage: https://programsandcourses.anu.edu.au/course/COMP1600
Country: Australia
Course code, if applicable: COMP4630
University hosting the course: Australian National University
Contact person Rajeev Gore, Rajeev.Gore
Concepts taught: logics, automated reasoning
Tools used:
Webpage: https://programsandcourses.anu.edu.au/course/comp4630
Country: Australia
Course code, if applicable: COMP2111
University hosting the course: University of New South Wales
Contact person Kai Engelhardt, kaie
Concepts taught: Hoare Logic, data refinement
Tools used:
Webpage: http://www.cse.unsw.edu.au/~cs2111/
Country: Australia
Course code, if applicable: CSSE3100
University hosting the course: The University of Queensland
Contact person Graeme Smith, smith
Concepts taught: Hoare Logic, theorem proving, refinement calculus
Tools used: KeY
Webpage: https://my.uq.edu.au/programs-courses/course.html?course_code=csse3100
Year/Level: 3
Country: Australia
Course code, if applicable: CSSE7610
University hosting the course: The University of Queensland
Contact person Graeme Smith, smith
Concepts taught: Model Checking
Tools used: SPIN
Webpage: https://my.uq.edu.au/programs-courses/course.html?course_code=csse7610
Year/Level: MSc