Tutorial Series of the FME Teaching Committee

Aug 24, 2021 Tutorials

In the FME Teaching Committee, we coordinate a tutorial series, planned to be held monthly. We aim to increase the awareness and sharing of tools and techniques used for teaching formal methods. The series is held online via zoom. We record (whenever the speaker agrees) these presentations and collect them below.

If you wish to receive announcements on these lectures, please subscribe to our mailing list fmtea@fmeurope.org by sending an email to sympa@lists.uu.se with the subject line
SUBSCRIBE IT-FMEUROPE-FMTEA firstname lastname

Zoom coordinates

Here are the details of the scheduled Zoom meeting:

Table of Contents

2025

  • February 28, 2025: Prof Marielle Stoellinga, University of Twente, The Netherlands: Life long learning — experience with educational programs for professionals

2024

  • September 27, 2024, 3 pm CET: Prof Rosemary Monahan, Maynooth University, Ireland, on Teaching Dafny at undergraduate and MSc level on Irish and Erasmus+ European Degree programmes.

    • The recording of Prof. Monahan’s lecture can be seen here and a few snapshots from the lecture here.

    • Read more

      During the tutorial, Rosemary outlined her experiences in teaching Dafny first in a 3rd year course that this year has 185 students, then at the MSc level where there are 50 students, and then at the international Erasmus MSc level. In all these courses, practically the teaching takes place one day per week, where 3 hours of lectures are followed by 3 hours of lab work in applying the concepts learnt. What impresses visibly from this tutorial is not only the amount of students, but also Rosemary’s involvement, dedication and perseverance, coding herself in front of and together with the students and receiving them after class in her office to untangle their proofs. While in the BSc course, she co-lectured with Dr Hao Wu, and has the help of 12 PhD/4th year BSc students in the labs, in the MSc course she is alone handling the labs. Besides, there is a continuous assessment component as well as a written exam. The MSc continuous assessment is often inspired by software verification competitions such as VerifyThis, SVComp, and Toolympics. The teaching material includes Dafny, based on the recent Program Proofs book authored by Rustan Leino; but it also presents related concepts such as Hoare logic, theorem proving in Coq, temporal logic, model checking, SAT/SMT solvers, Event-B and Mu-FRET, the latter being a framework recently developed by Rosemary and colleagues for formalising requirements. Students are excited about the code generation aspects of Dafny and positive feedback has been given in the form of “Model checking popped up in my interview, I am so happy you taught us that!”.

  • May 24, 2024, 3 pm CEST: Prof Tiziana Margaria, University of Limerick, Ireland: Teaching Formal Methods in Germany vs. Ireland: experience from two very different systems.

    • The recording of Prof Margaria’s lecture is here. A few screenshots from the lecture can be seen here.

    • Read more

      Prof Margaria has significant experience in teaching Formal Methods to software engineering students as well as to people with no software development experience. Her courses always revolve around case studies stemming from research, often in cooperation with industry, thus offering strong motivation to those studying. In a recently started project involving both academia and industry, they are going to develop so-called Formal Methods micromodules for the partners in industry, so that they come up to speed with the needed formalisms and tools. In fact, she argues for how to break the vicious circle of industry missing Formal Methods specialists educated by academia, while universities usually do not teach Formal Methods because the common knowledge is that industry manages without it: Tiziana suggests that we can start with teaching Formal Methods modules to industry, starting with FM-infused Model Driven Development as a flavour of the trendy Low-code/No-code movement. In this way, industrialists can experience some Formal Methods strength and ask for more.

      In the tutorial, Prof Margaria describes teaching Formal Methods in two countries: Germany and Ireland, pointing out some differences between their systems and students. Below is a list of teaching contributions in these two countries that Tiziana led:

  • March 28, 2024, 3pm CET: Prof Wolfram Kahl, McMaster University, Canada: Teaching with CalcCheck.

    • The recording of Prof Kahl’s lecture is here. A few screenshots from the lecture can be seen here.

    • Read more

      Prof Kahl talked about his experiences in teaching with an impressive tool called CalcCheck: a proof checker for teaching Logics and Discrete Mathematics to second-year computer science students since 2010. CalcCheck is based on “A Logical Approach to Discrete Math”, a classical logic book by Gries and Schneider. CalcCheck is web-based, with an interface similar to that of Jupyter notebooks that students are already used to. Before using CalcCheck, students used to ask “how do we know if our proofs are correct?”. Now they get feedback on their syntax and proofs, side-by-side with their input. CalcCheck is also used in exams and has an auto-grader component that is of big help to the teachers, both in exams and midterms, but also for homework. Since CalcCheck is such a convenient tool both for teachers and students, since 2018 it was used for twice-a-week homework, a component that was a game changer for student understanding and higher grade distribution. CalcCheck is a tool dedicated to teaching, a proof checker rather than a proof assistant, and it implements the so-called “people logic” (of the textbook by Gries and Schneider) rather than mechanised logic, making it much more student-friendly. Prof. Kahl is the developer and maintainer of CalcCheck. Some features of CalcCheck:

      • Proof Checking: The ability to check the logical validity of each step in a mathematical proof.
      • Interactive Exercises: Students can engage with interactive exercises that are designed to reinforce mathematical concepts and proof techniques.
      • Self-Learning: It can be used for self-learners of mathematical logic, discrete mathematics, and other related fields.
      • Customisability: Teachers can create custom exercises and problem sets tailored to their curriculum, making it a versatile tool for a variety of mathematical topics.

  • March 1, 2024, 10 am CET: Prof Carroll Morgan, University of New South Wales, Australia: Teaching formal methods informally: a report from the front line.

    • The recording of Prof. Morgan’s lecture is here. A few screenshots from the lecture can be seen here.

    • Read more

      The lecture was about Carroll’s teaching of a course where informal reasoning about programs is promoted. The roots of this talk can be found in Prof Morgan’s invited lecture at the FMTea'19 symposium in Porto: check that lecture’s abstract here. He argued there for incorporating Formal Methods thinking into the actual programming courses we teach, simply renaming the whole approach “Introductory Programming”. The lecture was truly inspirational and Carroll continued teaching in this way at UNSW.

      However, just after 2019’s lecture his course had to change suddenly to being wholly on-line, and it significantly increased in size. In the current talk, Prof. Morgan discusses how he handled the new challenges that introduced, and what might lie ahead. One interesting aspect of the course now is a single whole-term programming assignment, incrementally developed by students every successive week. That makes the students always feel up-to-date with the course material: a very important aspect for their self-confidence and continuing engagement in the course topics. Each weekly assignment portion comes with an auto-marked quiz: students get the questions on Tuesday, but not the multiple options (needed for automatic grading) for each question’s answer until Friday; and then they have time to reply to the questions until the following Monday. The few days spent just with the questions allow students time to think and formulate possible answers without knowing yet what choices will be available.

      Prof. Morgan also argues that the target “audience” we need to address in the Formal Methods courses is neither the top nor the bottom minorities, who will do what they usually do more or less independently of how we teach them. Instead, we need to focus on the middle majority — because they are the people who will program our phones in 10 years. If we can make an impression on them, with respect to incorporating the ideas of Formal Methods reasoning into their everyday programming tasks, then we have fulfilled our mission.

  • January 26, 2024, 3pm CET: Prof Alcino Cunha, University of Minho (Department of Informatics), Portugal: Teaching Alloy with Alloy4Fun.

    • The recording of Prof. Cunha’s lecture is here. A few screenshots from the lecture can be seen here.

    • Read more

      Alcino was one of the proponents of Alloy6 and Alloy4Fun, has been teaching with Alloy for more than 15 years, and uses Alloy4Fun in teaching since 2019. Some info on Alloy4Fun can be seen here and Alloy4Fun itself can be found here. The main two goals for proposing Alloy4Fun were (i) the need to easily share models in Alloy with students and (ii) the need to get immediate feedback on the just written specifications. Neither of these were possible with the standard tool for modelling with Alloy (Alloy Analyzer). During the tutorial, Alcino gives a demo on how to write and check Alloy specifications in Alloy4Fun and explains how he uses this in the course Formal Methods in Software Engineering - a mandatory MSc course attended every year by more than 200 students.

2023

  • June 16, 2023, 3 pm CEST: Prof Laura Kovács, Vienna University of Technology (TU Wien), Austria: Teaching Formal Reasoning at TU Wien.

    • The recording of Prof. Kovács' lecture can be seen here and screenshots from the lecture can be seen here.

    • Read more

      Laura talked about her experiences on teaching two courses at TU Wien: Formal Methods for Computer Science, a mandatory MSc course and Automated Deduction, an elective MSc course. While the latter course is attended by about 40-50 students, the former course is mandatory for MSc students and is taught twice per year: both times, it is attended by hundreds of students, which is both a wonder as well as a challenge. For instance, in a recent paper, Laura explains how to manage generating exam sheets in this context, with the awesome detail that the generation of these sheets uses Formal Methods! For more details, here is the link to that 2021 paper. Among several interesting aspects related to the teaching materials, students learn how to generate loop-based programs given the invariants of loops, using tools developed in TU Wien, the research results for this topic being published last year.

      Some remarkable effects of Laura’s teaching are the motivation and inspiration many students get, and driven so, they choose to write their MSc theses in Formal Methods, some of them even choosing to remain in academia in Laura’s research group. This is really wonderful and rare: many of us let our research results to influence our teaching, but for teaching to influence research is less heard of. Driven by the success of these graduated courses, from next spring, TU Wien will also provide a Formal Methods course for BSc students, called Logic and Reasoning. The slides of Laura’s presentation are here.

  • May 26, 2023, 3 pm CEST: Research Director Thierry Lecomte, ClearSy, France: Teaching and Training in Formalisation with B.

    • The recording of Dr. Lecomte’s lecture can be seen here and screenshots from the lecture can be seen here.

    • Read more

      Thierry talked about his experiences of almost 30 years spent in the education of engineers (colleagues or customers) and students, together with the parallel design and improvement of supporting modelling tools in B. In a recently published paper, Thierry says: Applying formal methods in software industry is still perceived as a difficult task. To ease the task, providing tools that help during the development cycle is essential, but proper education of computer scientists and software engineers is also an important challenge to take up! Clearsy is an adept of Piaget’s hypothesis that only one third of the population is able to handle abstraction, and so, people are sorted into their most suitable job based on how they perform in their initial training. People that are hired at Clearsy need to have some experience in modelling, independently of the modelling language. A big part of a Clearsy engineer’s job consists in proving interactively various system properties, in average about 16 proofs per day. Training engineers is therefore focusing on all these aspects. The slides of the presentation are here.

  • April 28, 3 pm CEST: Associate Prof Stefan Hallerstede (Aarhus University, Denmark): A guide to Not teaching Formal Methods.

    • The recording of Prof. Hallerstede’s lecture can be seen here. Screenshots from the lecture can be seen here.

    • Read more

      Stefan’s talk was based on his experience in creating a new curriculum for Software Engineering studies at the undergraduate level, where they embedded Formal Methods somewhat inconspicuously in about 9 fundamental courses. A paper describing this process can be checked here. Creating a new BSc curriculum on Software Engineering in 2020 was a remarkable opportunity, given that in Århus University there is also a more theoretical program as well as a more applied program. Currently, the new Software Engineering program has about 50 students enrolled, but it can take up to 60 every year. The main idea of this program is to focus on what it means to be a good engineer in software: understand why a solution works or does not work, know the technologies, understand the importance of teams and communication - thus, not only programming. The focus is on programming methodology and not program constructs, because it is in the programming methodology that formal methods make sense. Three important features that the BSc program emphasises are (serious) thinking about the problem to solve, being rigorous, and understand program development in the sense of refinement. Teaching is dedicated to the students being young people, for instance containing numerous puzzles and challenges. Students and industrial partners already offer good feedback on this new initiative. The slides from the presentation can be seen here.

  • March 31, 3 pm CEST: Associate Prof Emil Sekerinski (McMaster University, Canada): Teaching Concurrent Programming.

    • The recording of Prof. Sekerinski’s lecture can be seen here. A few screenshots from the lecture can be seen here.

    • Read more

      Emil focuses his research on formal methods for more than three decades now and currently uses formal methods to teach concurrency at McMaster University in Canada. This is a mandatory course for students in their 3rd year of BSc studies and has about 150-200 participants every year. The method for teaching concurrency has been introduced earlier, in a paper presented in 2019 at the FMTea workshop. Multiple languages are used to teach students in this course - python, java, C, Go - and some of these (most notably Go) are not familiar to students beforehand. Also, no separate formal methods course precedes this one in the curriculum, although students have already had some logic and discrete math courses. Notably, the course is taught based on Jupyter notebooks, where students can directly compile python code and indirectly (but rather easily) can compile programs written in the other three languages. These notebooks are also available for self-study.

      The abstract of the talk follows below:

      The education in programming has in a certain sense deteriorated since the 80’s and 90’s: programming languages and environments, as common in industry and to which students are exposed in Computer Science, Software Engineering, and related programs, have become complex. Mastering them consumes students to an extent that courses cannot decouple the (timeless) principles of programming from the (short-lived) specifics of the programming environments at hand; the mathematical background on program design is often not taught. This is particularly critical for concurrent programming, which has become increasingly relevant but cannot be mastered without a theoretical background. The author has been developing course material for a required 3rd year Software Engineering course at McMaster University, Concurrent System Design with around 170 students, since 2018 to address that issue by web-based interactive notebooks using Jupyter that combine explanations, the mathematical theory, and execution of programs directly in the notebooks. Correctness reasoning, including non-interference of processes, is explained through hierarchical state diagrams. This talk gives an overview of the course material, which is available as an open educational resource, and reports on the experience.

2022

  • December 9, 2022, 3 pm CET: Principal Research Engineer Markus A. Kuppe, (RiSE group at Microsoft Research, US): Stories from the trenches: Teaching the TLA+ specification language in Industry.

    • The recording of Eng. Kuppe’s lecture can be seen here. A few screenshots from the lecture can be seen here.

    • Read more

      Markus works with Formal Methods at Microsoft for about 8 years, focusing on scaling verification to real-world problems and building tools that embed specification with established software engineering processes. He also teaches occasionally TLA+ to industrialists and in this lecture he described his experiences. Markus started by pinpointing the main features of TLA+, such as the fact that we can write both programs and the properties about the programs in the same language, the TLC model checker (main verification workhorse, enabling the proving of safety, liveness and refinement), PlusCal (the pseudocode avatar of TLA+, somewhat preferred for its non-mathematical syntax, although features such as complex fairness and refinement cannot be captured), Apalache (the new kid on the block in terms of verification, based on Z3), and TLAPS (the proof system which encompasses all the above). Examples in TLA+ can be checked here. He described challenges for engineers, such as the fact the liveness and fairness are not concepts common in programming; he also observed how various characteristics do not pose a challenge to programmers, such as the TLA+ syntax (programmers are “polyglots”) and the “always” and “eventually” operators. The TLA+ teaching materials that Markus uses in his workshops can be seen here.

  • October 28, 2022, 3 pm CEST: Dr Allan Blanchard (CEA-LIST, France): Formal methods for beginners and for C programs - Using Frama-C and its WP plug-in for teaching.

    • The recording of Dr. Blanchard’s lecture can be seen here. A few screenshots from the lecture can be seen here.

    • Read more

      Frama-C is a set of (mostly open-source) tools aimed at analysing C-code. ACSL is the specification language used to express contracts that the C-code should implement or conform to. In his tutorial, Allan described the WP plugin of Frama-C, a static analyser of C-code based on the weakest precondition calculus. He showed how interesting properties can be verified (e.g., the ACSL properties) and how also runtime problems that might occur are flagged by WP. Allan teaches WP to students in two courses and teaches also to industry. Safety-critical sectors (in railway, aviation, nuclear plants, etc) have an easier time accepting and adapting to Frama-C than non-critical sectors, as the former have a culture of using formal methods in some forms for some decades already. CEA-LIST works with the latter as well, introducing the subject stepwise. Certification can also be achieved with Frama-C - this provides motivation to students for investing in this field. Here you can contact the Frama-C community and here you can check up many resources, including publications and manuals on the different resources.

  • September 30, 2022, 3 pm CEST: Prof Michael Leuschel (Heinrich-Heine-University Düsseldorf, Germany): Teaching Formal Methods and Theoretical Computer Science with ProB.

    • The recording of Prof Leuschel’s lecture can be seen here. A few screenshots from the lecture can be seen here.

    • Read more

      Michael is the inventor of ProB and his lecture focused on several areas related to ProB and teaching. First, he discussed ways of using ProB for teaching various computer science courses, from basic ones, such as Logic for Computer Science and Automata Theory to more advanced ones such as Safety-Critical Systems. Together with his research group, Michael developed a jupyter kernel for ProB and uses jupyter notebooks to, e.g., express ProB formulas, executable models for various formalisms (deterministic and non-deterministic finite automata, Turing machines, etc), executable B versions for various algorithms, and visualisations of these. Here and here are some examples. Second, students are given opportunities to get involved in developing code for ProB, for instance to develop various plugins. Michael showed an impressive ProB timeline slide where students contributions are emphasised: they are numerous! Third, we were shown how to combine animation and visualisation in ProB to teach. Some classical Event-B examples were shown (the cars on a bridge problem from the Event-B book of Abrial) as well as a Sudoku visualisation made by a young student. VizB - ProB’s visualisation feature was demonstrated with these examples.

  • August 26, 2022, 3 pm CEST: Dr Robert Lewis (Brown University, US): Teaching the theory and practice of proof assistants with Lean.

    • The recording of Dr. Lewis' lecture can be seen here. A few screenshots from the lecture can be seen here.

    • Read more

      In the lecture, Dr Lewis explains how he teaches his course, called “Formal Proof and Verification”. This is an elective course on learning to prove properties with the Lean theorem prover. The course is inspired by a similar course held by Jasmin Blanchette at VU Amsterdam, based on the “Hitchhiker’s Guide to Logical Verification”, that Jasmin Blanchette co-authored. In the course, the students learn to use logic as a precise specification language and learn the theory and practice of Interactive Theorem Provers. Rob encourages them to prove, even if the proofs are not completed. Also, part of the students contribute to writing code for the Lean theorem prover. It is this combination of academic software development and precise modeling that makes the students more prepared to continue doing research in the Formal Methods area.

  • July 29, 2022: Prof Erika Abraham (RWTH Aachen University, Germany): Automatic exercise generation for satisfiability checking.

    • The recording of Prof. Abraham’s lecture can be seen here. A few screenshots from the lecture can be seen here.

    • Read more

      In the lecture, Erika presents her course on satisfiability checking, that includes both SAT and SMT. This is an elective course. In 2008, when she started teaching the course, there were 3 students participating. Last year, during pandemic conditions, more than 500 students registered to the course in hybrid mode: around 70 were in the lecture hall, while the rest attended online. Most of the students did finish the course, 380 and 250 respectively registering for the two possible exam dates. Erika discusses what probably contributes to the success of the course, as well as the practical problems that occur and the approach to solve them. Among these, the automated generation of comparable SMT-solving exercises is one of the main issues.

      The abstract of Prof. Abraham’s lecture is here:

      We offer a lecture on satisfiability checking, repeated annually each winter term since 2009. The contents cover SAT solving to check the satisfiability of propositional logic formulas as well as SAT-modulo-theories (SMT) solving for checking the satisfiability of logical formulas over different theories (equality logic with uninterpreted functions, bit-vector arithmetic, linear and nonlinear real and integer arithmetic).

      This lecture is challenging to teach, as the underlying math is - at least for the arithmetic theories - quite involved. The manual execution of the algorithms by the students plays a substantial role, thus it is important to offer the students a pool of exercises. Furthermore, with more that 500 registered students in the last winter term under pandemic conditions, we needed a large number of individual but comparable exercises for interactions during the lecture as well as for the online exam.

      However, the automated generation of comparable SMT-solving exercises turned out to be a hard nut. In this talk we discuss the obstacles and propose some solutions.

  • June 17, 2022: Dr Tim Nelson (Brown University, US): Building Formal Methods Classes for Everybody.

    • The recording of Dr Nelson’s lecture can be seen here. A few screenshots from the lecture can be seen here, together with the chat from the talk.

    • Read more

      In this talk, Dr. Nelson describes his course, Logic for Systems, which is the first course in Formal Methods at Brown. He argues that, for some students, it will also be the only formal method course they take and discusses ways to make the course have an impact on all students. For instance, all students should understand the notion of invariant and how to prove it. Although not mandatory, the course has in average 135 participants every year! For the final projects, the students can choose freely what system to model and prove properties about: while there are many software-specific systems they choose, there are also projects about chemistry, baseball and basketball, which really shows that students understand that formal methods are universal: they are a tool we use for modeling and proving whatever system!

      The abstract of Dr Nelson’s lecture is here:

      We think math and logic are beautiful and essential. If you teach a formal methods class, you probably agree. Some of our students, perhaps the most visible to us, also feel that way. But what about the other 90%, the students who aren’t inclined to take our classes or any non-required “theory” class at all? If formal methods really are essential, we owe every student an opportunity to explore them, discover useful ideas, and maybe even fall in love.

      Some people derisively respond to a more inclusive class by assuming it will coddle students. On the contrary, these students have their own strengths and abilities that we can and should design rigorous content around. After all, many of them will build the technologies we all use every day, so deepening their view of formalism satisfies both moral and selfish imperatives. This talk will cover the design space of such a course: pedagogy, tool choice (sometimes building our own!), assignment design, and even TA hiring. I’ll talk about things that have worked well for us, other things that didn’t, and what we learned along the way.

  • April 28, 2022, 3 pm CET: Prof. Jeremy Gibbons (University of Oxford, UK): How to Design Co−Programs.

    • The recording of Prof. Gibbons’s lecture can be seen here. A few screenshots from the lecture can be checked here.

    • Read more

      Prof. Gibbons takes us on a tour of teaching programming to novices and explains that writing a program does not happen by magic. His main thesis is that programs rely heavily on the structure of the input data as well as on that of the output data. This is a refinement to the hypothesis of the classic book, “How to Design Programs” by Felleisen, Findler, Flatt, and Krishnamurthi, which supports the idea the the structure of a program should follow the structure of the program’s input data. The talk is supported by the paper and slides below:

      • How to Design Co−Programs (Jeremy Gibbons). In Journal of Functional Programming. Vol. 31. No. e15. 2021. Link here.
      • Slides here.

      The abstract of Prof. Gibbons' lecture is here:

      The observation that program structure follows data structure is a key lesson in introductory programming: good hints for possible program designs can be found by considering the structure of the data concerned. In particular, this lesson is a core message of the influential textbook “How to Design Programs” by Felleisen, Findler, Flatt, and Krishnamurthi. However, that book discusses using only the structure of input data for guiding program design, typically leading towards structurally recursive programs. We argue that novice programmers should also be taught to consider the structure of output data, leading them also towards structurally corecursive programs.

  • February 25, 2022, 3 pm CET: Prof Shriram Krishnamurthi (Brown University, US): From Tests to Properties: Property-Based Testing Using Relational Problems.

    • The recording of Prof. Krishnamurthi’s lecture can be seen here. Screenshots from the lecture, as well as the chat window can be checked here.

    • Read more

      Shriram is involved in teaching 3 formal methods courses at Brown, with audiences varying between 70 and 200 students. In his talk, he discusses the importance of understanding the properties our programs should conform to, the role of unit testing in coding, as well as how students could gain from focusing on the problem to solve before programming a solution to it. Shriram’s talk is based on two papers: * Using Relational Problems to Teach Property-Based Testing (John Wrenn, Tim Nelson, Shriram Krishnamurthi), link here * Automated, Targeted Testing of Property-Based Testing Predicates (Tim Nelson, Elijah Rivera, Sam Soucie, Thomas Del Vecchio, Jack Wrenn, Shriram Krishnamurthi), link here

2021

  • December 10, 9am CET: Assoc Prof David Pearce (Victoria University of Wellington, New Zealand): Teaching Software Verification with Whiley.

    • The recording of Assoc. Prof. Pearce’s lecture can be seen here. Screenshots from the lecture as well as the chat with questions can be checked from here.

    • Read more

      Whiley is a programming language that can be used for verification and it was initiated by David himself. Here is the Wikipedia page for it and here the github page. David’s talk is divided into two parts - the first one describing and demonstrating Whiley and the second one offering hints on teaching it.

  • November 20-21, 9am-4pm CET: Tutorials@FM21
    • FMTea videos can be seen from here; FMTea is currently the main workshop on teaching formal methods.
    • FMI videos can be seen from here; FMI is a tutorial about formal methods used in connection with the digital twin concept.
    • Event-B IDE videos can be seen from here; Event-B IDE is a tutorial about developing an IDE for the Event-B language.
    • Momba videos can be seen from here; Momba is a tutorial about quantitative modelling with python.

  • October 29, 2021, 3pm CET: Dr Ran Ettinger (Ben-Gurion University, Israel): Teaching Cantor’s theorem, a pumping lemma, and the derivation of a heapsort algorithm using Dafny.

    • The recording of Dr. Ettinger’s lecture can be seen here. A few screenshots from the lecture can be seen here.

    • Read more

      Ran demonstrates in this lecture a hands-on approach on how to prove mathematical theorems with Dafny, a programming language generally used for verifying the correctness of software. This is a refreshing approach that Ran continues to teach even now when he moved to industry (NVidia). Dafny was initiated by Rustan Leino at Microsoft Research and is now (since Rustan moved to Amazon) maintained by Amazon Web Services. Here is Dafny’s github website and here is Dafny’s Wikipedia page.

  • September 24, 2021, 3pm CET: Prof Sandrine Blazy (University of Rennes 1, France): Why3 tool for deductive program verification.

    • The recording of Prof. Blazy’s lecture can be seen here. A few screenshots from the lecture can be seen here.

    • Read more

      Why3 is an intermediate language used for deductive verification: the user writes a specification, a corresponding program, and uses Why3 to prove that the program satisfies the specification. This is achieved in the background by the tool, by generating verification conditions, using the weakest precondition calculus. Why3 interfaces with numerous (currently about 20) automatic and interactive theorem provers and does not require the user to come up with many assertions, except those validating specifications. Here you can check Why3’s website.

The aim of the FME Teaching Committee is to support a worldwide improvement in learning formal methods, mainly by teaching but also via self-learning.