Skip to content

luigiapetre/Formal-Methods-Courses

BranchesTags

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

7 Commits
.github/ISSUE_TEMPLATE
.github/ISSUE_TEMPLATE
 
 
README.md
README.md
 
 
update_readme.sh
update_readme.sh
 
 

Repository files navigation

Formal-Methods-Courses

Here we collect worldwide courses teaching formal methods

Software Analysis

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
  • Webpage: https://github.com/bugcounting/software-analysis/
  • Year/Level: MSc (also available to PhD students)

Theoretical Computer Science II

  • 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

Formal Methods

Applied Formal Methods

  • 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/

Trustworthy programming

Certified Programming

  • 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
  • Webpage: http://www.di.ubi.pt/~desousa/PC/pc.html
  • Year/Level: PhD

Computer Aided Verification

  • 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/

Software Verification

  • 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

Logic and Semantics of Programming Languages

  • 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

Types and Lambda Calculus

Systems Verification

  • 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

Logic and Formal Methods (Logik und formale Methoden)

  • 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

System Validation

Programming Languages

  • 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

Rule Based Design

  • 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

System Validation

  • 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

Software Specification

Process Algebra

  • 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

System Validation

  • 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

Formal Methods for Software Engineering (25 ECTS)

  • 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

Proofs of Programs

  • 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
  • Webpage: http://www.lri.fr/~marche/MPRI-2-36-1/
  • Year/Level: MSc This course is at level MSc, more precisely at second year of Parisian Master in Computer Science

Security Engineering

Formal Methods in Software Engineering

Logic for system analysis

  • Country: Norway

  • Course code, if applicable:

  • University hosting the course: University of Oslo

  • Contact person Peter Ölveczky, peterol

  • Concepts taught:

    • Formal modeling and analysis;
    • Equational logic;
    • Rewriting logic;
    • Distributed systems;
    • Transport protocols;
    • Distributed algorithms (distributed commit, distributed mutual exclusion, distributed leader election);
    • Cryptographic protocols modeling and analysis;
    • Temporal logic and TL model checking;
    • Real-time and probabilistic systems;

  • Tools used: Maude

  • Webpage: https://www.uio.no/studier/emner/matnat/ifi/INF3232/index-eng.html

  • Year/Level: 2,3

Testing, Debugging, and Verification

Software Engineering using Formal Methods

Introduction to C program proof using Frama-C and its WP plugin

Modeling and Programming

  • 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

Certified Software

  • 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

Mechanized Reasoning about Programs

  • 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
  • Webpage: http://frederic.loulergue.eu/teaching/cs451.pdf
  • Year/Level: 4, MSc, PhD

Computação Fiável (Reliable Programming)

Reasoning about Programs

Proofs of Programs

  • 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
  • Webpage: http://www.lri.fr/~marche/MPRI-2-36-1/
  • Year/Level: MSc This course is at level MSc, more precisely at second year of Parisian Master in Computer Science

Reasoning about Programs

Verifying Complex Systems

  • 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

Formal methods for concurrent and real-time systems

  • 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

Vérification déductive de programmes (deductive verification of programs)

  • 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

HECS (High-Confidence Embedded and Cyberphysical Systems)

  • 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

Programming: Correctness by Construction

  • 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

Introduction to Model Driven Development

  • 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:

Engineering Interactive Systems

Logic and Computation

  • 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

Model Checking

Specification Languages and Models

Formal Software Engineering

Safety Critical Systems

Software Correctness

High Integrity Systems Engineering

  • 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

Software Testing and Quality Assurance

  • 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/

Advanced Topics in Theory and Practice of Software

Advanced Algorithms

Foundations of Computing

  • 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

Overview of Logic and Computation

  • 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

System Modelling & Design

  • 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/

Reasoning about Programs

Concurrency: Theory and Practice

About

Here we collect worldwide courses teaching formal methods

Resources

Readme
Activity

Stars

35 stars

Watchers

6 watching

Forks

4 forks
Report repository

Releases

No releases published

Packages

No packages published

Contributors 2

  •  
  •  

Languages