Tutorial Series of the FME Teaching Committee

Schedule

Schedule for FMTea tutorials

In the FME Teaching Committee, we coordinate a (new) 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 on the FME Teaching Committee website.

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

Below we list the speakers who (will) share their teaching experiences in formal methods in 2022:

  • 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. 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
  • (Thursday!!) 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. 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.

  • 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. In this talk, Dr. Nelson describes his course, Logic for Systems, which is the first course in Formal Methods at Brown. Although not mandatory, the course has roughly a hundred participants every year. Tim argues that it may be the only formal-methods course that many of them take, and so it is important to have an impact on all students. For instance, all students should be able to express formal properties about systems, even if they don’t know how to prove those properties hold. For their 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 group theory, which shows that students understand that formal methods are universal: they are a tool we use for modeling and reasoning about 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.

  • July 29, 2022: Prof Erika Abraham (RWTH Aachen University, Germany): Automatic exercise generation for satisfiability checking. 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.

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

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

  • October 28, 2022, 3 pm CET: Dr Allan Blanchard (CEA-LIST, France)

Below you’ll find the list of speakers who shared their formal methods teaching insight in 2021:

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

Zoom coordinates

Luigia Petre is inviting you to a scheduled Zoom meeting.

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.