[Hol-info] FME Teaching Tutorial on 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
Dear all, We continue our Formal Methods Teaching tutorials series with a lecture on Friday, May 24! Prof Prof Tiziana Margaria, University of Limerick, Ireland will reflect on her experiences in teaching Formal Methods in two countries: Germany and Ireland. Tiziana is a computer scientist and software engineer whose research topics include formal methods and model-driven engineering. She has worked in Italy, Germany, Sweden, and Ireland, and currently is the Chair of Software Systems in the University of Limerick's Department of Computer Science and Information Systems. She has a broad experience in the use of formal methods for high assurance systems, in particular concerning functional verification, reliability, and compliance of complex heterogeneous systems, with applications to embedded systems, healthcare, and smart advanced manufacturing. A few pointers from Tiziana's numerous roles are that she is the Past President of FMICS (the ERCIM Working Group on Formal Methods for Industrial Critical Systems); the managing editor of STTT, the Springer Journal on Software Tools for Technology Transfer; and a co-founder of the TACAS and ISoLA series of conferences. In her career spanning several decades of teaching and research in several European contexts, here are a couple of milestones: - a survey on her group's experience: https://link.springer.com/referenceworkentry/10.1007/978-3-030-10576-1_208 - teaching Formal Methods in Germany: https://ceur-ws.org/Vol-1385/paper4.pdf - a book on teaching Foundations of process modelling to non-CS students in Germany: https://link.springer.com/book/10.1007/978-3-662-45006-2 - using models as a high level tool for computational thinking: https://ieeexplore.ieee.org/abstract/document/8377800 https://ieeexplore.ieee.org/abstract/document/7273708 - modelling for teenagers: https://ieeexplore.ieee.org/abstract/document/5090525 https://ieeexplore.ieee.org/abstract/document/7552218 More information about our lecturer can be found here: https://www.ul.ie/hri/person/hri-member/prof-tiziana-margaria. The zoom link for Prof. Margaria’s lecture is https://aboakademi.zoom.us/j/64254430116. The event will last about an hour. Warmly welcome!! Best wishes, Luigia PS: for more info, here is the tutorial series webpage: https://fme-teaching.github.io/2021/08/24/tutorial-series-of-the-fme-teaching-committee/. __ Luigia Petre, Docent, PhD Faculty of Science and Engineering Åbo Akademi University, Finland www.users.abo.fi/lpetre ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] Call for Tutorial Papers at FM 2024: deadline approaching —> April 19!
For the first time ever, the FM symposium hosts a tutorial papers track: https://www.fm24.polimi.it/?page_id=310. We invite you to submit your tutorial contributions here! Important Dates (Tutorial Papers Only) Tutorial Paper Submission April 19th, 2024 (Fri) 23:59 AoE Preliminary Decision May 24th, 2024 (Fri) 23:59 AoE Revised Version Due June 9th, 2024 (Sun) 23:59 AoE Final Decision June 24th, 2024 (Mon) 23:59 AoE Final Paper Due July 1st, 2024 (Mon) 23:59 AoE Conference September 9th – 13th, 2024 Tutorial papers present ideas with a focus on pedagogy over technical innovation. By being written in a broadly-accessible way, a tutorial will clarify important ideas, bring new researchers into the community, and serve as a bridge to practitioners. A good tutorial paper is not expected to have any technical innovation at all. Instead, we will evaluate it on its pedagogy: Is it crisp and clear? Is it readable? Does it help build good intuitions? Is it comfortable to follow? Will it help useful ideas reach a much broader audience? While tutorials about tools are a canonical fit, tutorials about techniques are also welcome. Prospective authors who want to suggest tutorials of other kinds are welcome to contact the chairs to get guidance. In general, we are very open-minded about what tutorials are about, provided they are about topics of interest to the formal methods community. Tutorial papers can be at most 22 pages in LNCS format. There is no minimum length; the tutorial should be as long as necessary to be effective, but should avoid filler. Tools should include links and descriptions of how to run them. Papers are welcome to include an appendix, which reviewers will read at their discretion. (We understand that detailed screen-shots, tool descriptions, etc., are best relegated to an appendix, and reviewers will make a good-faith effort to examine these.) Authors of a paper need not be the creators of the technical concepts it describes. The paper must provide clear references to the original technical content. The presentation must be novel relative to the published literature. Accepted papers will be published in the conference proceedings. Authors of accepted papers will be given a presentation slot in the tutorials period preceding the main conference. The tutorial paper submission should specify the desired length of the presentation, which can be a half or full day. They will also be invited (but are not required) to give a five-minute presentation during the main conference, to give their tutorial wider notice. Authors of tutorials are strongly encouraged to submit at least preliminary versions of runnable/machine-readable artifacts to accompany their papers, where appropriate. Authors of preliminarily accepted tutorials are strongly encouraged to submit an artifact for evaluation by the FM 2024 Artifact Evaluation Committee after the preliminary notification for their tutorial. Authors can also request a tutorial presentation slot without an accompanying paper by submitting a short tutorial proposal instead. Priority will be given, however, to tutorials accompanied by full tutorial papers. Submissions Submit your papers at https://easychair.org/conferences/?conf=fm24 <https://easychair.org/conferences/?conf=fm24> Tutorial Track Committee Member(s) Affiliation Role Luigia Petre<https://luigia-petre.github.io/luigiapetre/> Åbo Akademi University, Finland PC Co-Chair Shriram Krishnamurthi<https://cs.brown.edu/~sk/> Brown University, USA PC Co-Chair Anindya Banerjee<https://software.imdea.org/people/anindya.banerjee/> IMDEA Software Institute, Spain PC Member Brijesh Dongol<https://brijeshdongol.github.io/> University of Surrey, UK PC Member Daniel Jackson<https://people.csail.mit.edu/dnj/> MIT, USA PC Member David Thrane Christiansen<https://davidchristiansen.dk/index.html> Lean FRO, LLC PC Member Jan Friso Groote<https://www.tue.nl/en/research/researchers/jan-friso-groote> Eindhoven University of Technology, Netherlands PC Member Jannis Limperg<https://limperg.de/> University of Munich (LMU), Germany PC Member Jeroen Keiren<https://www.jeroenkeiren.nl/> Eindhoven University of Technology, Netherlands PC Member Marcello Bonsangue<https://www.universiteitleiden.nl/en/staffmembers/marcello-bonsangue#tab-1> Leiden University, Netherlands PC Member Markus Alexander Kuppe<https://www.linkedin.com/in/markus-kuppe-643559180/> Microsoft Research, USA PC Member Maurice ter Beek<https://www.isti.cnr.it/it/chi-siamo/people-detail/361/Maurice_Henri_ter_Beek> CNR-ISTI, Pisa, Italy PC Member Nikolaj Bjorner<https://www.microsoft.com/en-us/research/people/nbjorner/> Microsoft Research, USA PC Member Rosemary Monahan<https://www.maynoothuniversity.ie/faculty-science-engineering/our-people/
[Hol-info] FME Teaching Tutorial on March 28, 2024, 3 pm CET: Prof Wolfram Kahl, McMaster University, Canada: Teaching with CalcCheck
Dear all, We continue our Formal Methods Teaching tutorials series with a lecture on Thursday (!!), March 28! Prof Wolfram Kahl, McMaster University, Canada will lecture on his experiences in teaching with a tool called CalcCheck: a proof checker for teaching calculational Logics and Discrete Mathematics. CalcCheck offers an automated hands-on approach to learning math that traditional teaching methods lack. It supports the development of critical thinking and problem-solving skills, by encouraging students to actively explore and experiment. 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. Prof. Kahl is the developer and maintainer of CalcCheck. More information about our lecturer can be found here: https://www.cas.mcmaster.ca/~kahl/. The zoom link for Prof. Kahl’s lecture is https://aboakademi.zoom.us/j/64254430116. The event will last about an hour. Warmly welcome!! Best wishes, Luigia PS: for more info, here is the tutorial series webpage: https://fme-teaching.github.io/2021/08/24/tutorial-series-of-the-fme-teaching-committee/. __ Luigia Petre, Docent, PhD Faculty of Science and Engineering Åbo Akademi University, Finland www.users.abo.fi/lpetre ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] FME Teaching Tutorial on March 1, 2024, 10am (!) CET: Prof Carroll Morgan, University of New South Wales, Australia: Teaching formal methods informally: a report from the front line
Dear all, We continue our Formal Methods Teaching tutorials series with a lecture on Friday, March 1, 2024 at 10 am CET. Please note the unusual time, due to our speaker's location (Sydney, Australia). Prof Carroll Morgan, University of New South Wales (UNSW), Australia will lecture on his experiences in teaching Formal Methods to Computer Science students, without focusing on the theoretical, formal aspects of the topic. The roots of this talk can be found in Prof Morgan’s invited lecture at the FM19 symposium in Porto - check that lecture’s abstract here: https://www.easychair.org/smart-program/FMTea19/2019-10-07.html. He argued there for incorporating Formal Methods thinking into the very programming courses we teach and simply rename the whole approach as Programming. The lecture was truly inspirational and Carroll continued teaching in this way at UNSW. However, a not-so-small problem occurred since 2019: his class became mandatory and so the attendance increased about 7 times. In the tutorial talk on March 1, Prof Morgan will discuss how he handles this new challenge. More information about our lecturer can be found here: https://www.unsw.edu.au/staff/carroll-morgan. The zoom link for Carroll’s lecture is https://aboakademi.zoom.us/j/64254430116. The event will last about an hour. Warmly welcome!! Best wishes, Luigia PS: for more info, here is the tutorial series webpage: https://fme-teaching.github.io/2021/08/24/tutorial-series-of-the-fme-teaching-committee/. __ Luigia Petre, Docent, PhD Faculty of Science and Engineering Åbo Akademi University, Finland www.users.abo.fi/lpetre ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] FME Teaching Tutorial on January 26, 2024, 3pm CEST: Prof Alcino Cunha, University of Minho, Portugal: Teaching Alloy with Alloy4Fun
Dear all, The Formal Methods Teaching tutorials series starts in 2024 with a lecture on Friday, January 26! Prof Alcino Cunha, University of Minho, Portugal will lecture on his experiences in teaching Alloy with Alloy4Fun on Friday, January 26, 2024 at 3 pm CEST. Alcino uses Alloy4Fun in teaching since 2019, and was one of the proponents of Alloy6 and Alloy4Fun. Here is a bit of context for Alloy4Fun, from https://haslab.github.io/Alloy4Fun/tutorial.html: "Due to the simplicity and flexibility of the language and intuitive and automatic feedback provided by its analyzer, Alloy is often taught in introductory formal methods courses. However, the classic standalone Alloy Analyzer suffers from some limitations that hinder its usage in the classroom, namely *the lack of a straightforward mechanism to share simple Alloy models, instances and associated themes, a process that becomes cumbersome in large classes where students require feedback or have to submit exercise resolutions for evaluation; and *the absence of some automated assessment functionality or online judge system for students to autonomously solve exercises and receive automatic feedback regarding the correctness of their resolutions. The Alloy4Fun platform was developed precisely to address these issues. Alloy4Fun allows users to edit and execute Alloy 6 models online, providing a minimalistic customizable instance visualizer. Both models and instances can be easily shared through permalinks. Moreover, the platform provides support for simple specification challenges in the form of duels where students attempt to discover a secret constraint specified by the instructors. When solving these challenges, students are supported by a hint system to nudge them in the right direction when stuck. Alloy4Fun collects anonymized information about the student submissions and interactions, so that instructors can measure the progress of the students on the shared challenges and identify potential learning bottlenecks." More information about our lecturer can be found here: https://alcinocunha.github.io/. The zoom link for Alcino's lecture is https://aboakademi.zoom.us/j/64254430116. The event will last about an hour. Warmly welcome!! Best wishes, Luigia PS: for more info, here is the tutorial series webpage: https://fme-teaching.github.io/2021/08/24/tutorial-series-of-the-fme-teaching-committee/. __ Luigia Petre, Docent, PhD Faculty of Science and Engineering Åbo Akademi University, Finland www.users.abo.fi/lpetre ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] FM Teaching Tutorial on June 16, 3 pm CEST: Prof. Laura Kovács, Vienna University of Technology, Austria: Teaching Formal Reasoning at TU Wien
Dear all, The Formal Methods Teaching tutorials series continues with a lecture on Friday, June 16! Prof Laura Kovács, Vienna University of Technology, Austria will lecture on her experiences in teaching formal methods on Friday, June 16, 2023 at 3 pm CEST. Laura's teaching career spreads on more than 15 years, with more than a decade at TU Wien. Some of her courses have 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: https://link.springer.com/chapter/10.1007/978-3-030-81097-9_15. Laura's lecture on June 16 is entitled "Teaching Formal Reasoning at TU Wien". More information about our lecturer can be found here: http://lkovacs.com<http://lkovacs.com/>. The zoom link for Laura' lecture is https://aboakademi.zoom.us/j/64254430116. The event will last about an hour. Warmly welcome!! Best wishes, Luigia PS: for more info, here is the tutorial series webpage: https://fme-teaching.github.io/2021/08/24/tutorial-series-of-the-fme-teaching-committee/. __ Luigia Petre, Docent, PhD Faculty of Science and Engineering Åbo Akademi University, Finland www.users.abo.fi/lpetre ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] FM Teaching Tutorial on April 28, 3 pm CEST: Assoc Prof Stefan Hallerstede (Aarhus University, Denmark): A guide to Not teaching Formal Methods
Dear all, The Formal Methods Teaching tutorials series continues with a lecture on Friday, April 28! Assoc Prof Stefan Hallerstede (Aarhus University, Denmark) will lecture on how NOT to teach Formal Methods on Friday, April 28, 2023 at 3 pm CEST. His talk is 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: https://doi.org/10.1007/978-3-030-57663-9_12. Stefan's lecture on Friday is entitled "A guide to Not teaching Formal Methods". More information about our lecturer can be found here: https://pure.au.dk/portal/en/persons/stefan-hallerstede%2865c96a3f-b4af-473c-a0d8-7909b2f2903c%29.html. The zoom link for Stefan' lecture is https://aboakademi.zoom.us/j/64254430116. The event will last about an hour. Warmly welcome!! Best wishes, Luigia PS: the tutorial series webpage is below; we have speakers planned until June! https://fme-teaching.github.io/2021/08/24/tutorial-series-of-the-fme-teaching-committee/. __ Luigia Petre, Docent, PhD Faculty of Science and Engineering Åbo Akademi University, Finland www.users.abo.fi/lpetre ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] FM Teaching Tutorial on March 31, 3 pm CEST --> Prof Emil Sekerinski (McMaster University, Canada): Teaching Concurrent Programming
Dear all, The Formal Methods Teaching tutorials series resumes in 2023 with a lecture on Friday, March 31! Prof. Emil Sekerinski (McMaster University, Canada) will lecture on Teaching Concurrent Programming on Friday, March 31, 2023 at 3 pm CEST. An abstract for his talk comes 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. More information about our lecturer can be found here: http://www.cas.mcmaster.ca/~emil/. The zoom link for Emil' lecture is https://aboakademi.zoom.us/j/64254430116. The event will last about an hour. Warmly welcome!! Best wishes, Luigia PS: the tutorial series webpage is below; we have speakers planned until June! https://fme-teaching.github.io/2021/08/24/tutorial-series-of-the-fme-teaching-committee/. __ Luigia Petre, Docent, PhD Faculty of Science and Engineering Åbo Akademi University, Finland www.users.abo.fi/lpetre ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] FMTea Tutorial on Teaching TLA+ in Industry: Principal Research Engineer Markus Kuppe, RiSE group at Microsoft Research, US, on Friday, December 9, 2022 at 3 pm CET
Dear all, The Formal Methods Teaching tutorials series wraps up 2022 with a lecture on Friday, December 9, 2022! Principal Research Engineer Markus Kuppe (RiSE group at Microsoft Research, US) will lecture on Friday, December 9, 2022 at 3 pm CET on his experiences on teaching TLA+ in industry. His talk is entitled entitled "Stories from the trenches: Teaching the TLA+ specification language in Industry". More information about our lecturer can be found here: https://www.linkedin.com/in/markus-kuppe-643559180/. The zoom link for Markus' lecture is https://aboakademi.zoom.us/j/64254430116. The event will last about an hour. Warmly welcome!! Best wishes, Luigia PS: the tutorial series webpage is below; we continue in January 2023! https://fme-teaching.github.io/2021/08/24/tutorial-series-of-the-fme-teaching-committee/. __ Luigia Petre, Docent, PhD Faculty of Science and Engineering Åbo Akademi University, Finland www.users.abo.fi/lpetre ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] Formal Methods Teaching Tutorial on Frama-C: Dr Allan Blanchard on Friday, October 28, at 3pm CET
Dear all, The Formal Methods Teaching tutorials series continues on the last Friday of October with a lecture on Frama-C! Dr Allan Blanchard (CEA-LIST, France) will lecture on Friday October 28, 2022, at 3 pm CEST with a talk entitled "Formal methods for beginners and for C programs - Using Frama-C and its WP plug-in for teaching". More information about our lecturer can be found here: https://allan-blanchard.fr<https://allan-blanchard.fr/>. The zoom link for Allan's lecture is https://aboakademi.zoom.us/j/64254430116. The event will last about an hour. Warmly welcome!! Best wishes, Luigia PS: the tutorial series webpage is here: https://fme-teaching.github.io/2021/08/24/tutorial-series-of-the-fme-teaching-committee/. __ Luigia Petre, Docent, PhD Faculty of Science and Engineering Åbo Akademi University, Finland www.users.abo.fi/lpetre ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] FME Teaching Tutorials series continues on August 26, at 3 pm CEST: Dr. Robert Lewis (Brown University, US) on "Teaching the theory and practice of proof assistants with Lean"
Dear all, On the last Friday of the summer, we have the opportunity of a theorem prover lecture from an Ivy League colleague! Dr. Robert Lewis (Brown University, US) will lecture on Friday August 26, 2022, at 3 pm CEST on the Lean theorem prover. His talk is entitled "Teaching the theory and practice of proof assistants with Lean". Rob will complete the series of 3 lectures on teaching formal methods at Brown; if interested in the previous two lectures, please check our website (link below in the PS). The zoom link for Rob's lecture is https://aboakademi.zoom.us/j/64254430116. The event will last about an hour. Warmly welcome!! Best wishes, Luigia PS: the tutorial series webpage is up to date with the list of 2021 and 2022 speakers (and links to (almost all of) the recordings of their talks): https://fme-teaching.github.io/2021/08/24/tutorial-series-of-the-fme-teaching-committee/. __ Luigia Petre, Docent, PhD Faculty of Science and Engineering Åbo Akademi University, Finland www.users.abo.fi/lpetre ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] New lecture in FME Teaching Tutorials series on July 29, at 3 pm CEST: Prof. Erika Abraham (RWTH Aachen University, Germany) on "Automatic exercise generation for satisfiability checking"
Dear all, I hope that, even though the summer holidays are upon us, you'll find the time to join us at the upcoming FME Teaching Tutorial, on the last Friday of July! We now have the pleasure of listening to Prof. Erika Abraham's (RWTH Aachen University, Germany) lecture on Friday July 29, 2022, at 3 pm CEST. Her talk is entitled "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. The zoom link is https://aboakademi.zoom.us/j/64254430116. The event will last about an hour. Warmly welcome!! Best wishes, Luigia PS1: the tutorial series webpage is updated with the list of speakers who confirmed their lectures in 2022 here: https://fme-teaching.github.io/2021/08/24/tutorial-series-of-the-fme-teaching-committee/. Please note that we have a speaker scheduled every month until October!! __ Luigia Petre, Docent, PhD Faculty of Science and Engineering Åbo Akademi University, Finland www.users.abo.fi/lpetre ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] FME Tutorial series lecture this week, June 17, at 3 pm CET: Dr Tim Nelson (Brown University, US) on "Building Formal Methods Classes for Everybody"
Dear all, The FME Tutorial series continues! This week we have the pleasure of listening to Dr Tim Nelson's (Brown University, US) lecture on Friday June 17, 2022, at 3 pm CET. His talk is entitled "Building Formal Methods Classes for Everybody". 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. The zoom link is https://aboakademi.zoom.us/j/64254430116. The event will last about an hour. Warmly welcome!! Best wishes, Luigia PS1: the tutorial series webpage is updated with the list of speakers who confirmed their lectures in 2022 here: https://fme-teaching.github.io/2021/08/24/tutorial-series-of-the-fme-teaching-committee/. Please note that we have a speaker every month from now on until October!! PS2: the June 2022 lecture is scheduled exceptionally on the 17th of the month, instead of the usual last Friday of the month, due to the summer holidays of some of the involved academics. __ Luigia Petre, Docent, PhD Faculty of Science and Engineering Åbo Akademi University, Finland www.users.abo.fi/lpetre ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] FM Tutorial Lecture on THURSDAY, April 28, at 3 pm CET: Prof. Jeremy Gibbons on How to Design Co-Programs
Dear all, The FM Tutorial series continues with Prof. Jeremy Gibbons's lecture on THURSDAY April 28, 2022, at 3 pm CET: His talk is entitled "How to Design Co −Programs". The abstract of Prof. Gibbons's 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. The zoom link is https://aboakademi.zoom.us/j/64254430116. The event will last about an hour. Warmly welcome!! Best wishes, Luigia PS1: the tutorial series webpage is updated with the list of speakers who confirmed their lectures in 2022 here: https://fme-teaching.github.io/2021/08/24/tutorial-series-of-the-fme-teaching-committee/. Please note that we have a speaker every month from now on until August, and then also October is booked. PS2: the April 2022 lecture is scheduled exceptionally on the last _Thursday_ of the month, instead of the usual Friday. __ Luigia Petre, Docent, PhD Faculty of Science and Engineering Åbo Akademi University, Finland www.users.abo.fi/lpetre<http://www.users.abo.fi/lpetre> ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] FME Teaching tutorial on Friday, February 25, at 3 pm CET --> Prof Shriram Krishnamurthi, Brown University, US
Dear all, We restart the FME Teaching Committee's series of tutorials in 2022 with Prof. Shriram Krishnamurthi's lecture on Friday, February 25, at 3 pm CET. His talk in entitled "From Tests to Properties: Property-Based Testing Using Relational Problems". The zoom link is https://aboakademi.zoom.us/j/64254430116. The event will last about an hour. Warmly welcome!! Kind regards, Luigia Petre (on behalf of the FME Teaching Committee) PS1: the tutorial series webpage is updated with the list of speakers who confirmed their lectures in 2022 here: https://fme-teaching.github.io/2021/08/24/tutorial-series-of-the-fme-teaching-committee/. PS2: the tutorial series aims to increase the awareness and sharing of tools and techniques used for teaching formal methods __ Luigia Petre, Docent, PhD Faculty of Science and Engineering Åbo Akademi University, Finland www.users.abo.fi/lpetre ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] Teaching tutorial this Friday Dec 10, at 9 am CET: Software Verification with Whiley, David Pearce
Dear all, In the FME Teaching Committee series of tutorials, we continue on Friday, December 3rd, with Assoc. Prof. David Pearce, who will present his experiences of teaching software verification with Whiley. Please note the special time (9am CET) - David lives in New Zealand and is 12h ahead of CET, so for him the talk is at 9 pm. Here is the info in our webpages: https://fme-teaching.github.io/2021/08/24/tutorial-series-of-the-fme-teaching-committee/ And here is the zoom link: https://aboakademi.zoom.us/j/64254430116 Everyone welcome! Kind regards, Luigia Petre (on behalf of the FME Teaching Committee) ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] Ran Ettinger's tutorial on using Dafny to teach: FME Teaching Committee's Tutorial Series, October edition
Dear all, We are now at the second tutorial in the Tutorial Series of the FME Teaching Committee. The idea is to increase the awareness and sharing of tools and techniques used for teaching formal methods. The tutorials are held online via zoom. We record (whenever the speaker agrees) these presentations and collect them on the FME Teaching Committee website: https://fme-teaching.github.io/2021/08/24/tutorial-series-of-the-fme-teaching-committee/. [https://fme-teaching.github.io/2021/08/24/tutorial-series-of-the-fme-teaching-committee/featured.png]<https://fme-teaching.github.io/2021/08/24/tutorial-series-of-the-fme-teaching-committee/> Tutorial Series of the FME Teaching Committee | Formal Methods Teaching Committee<https://fme-teaching.github.io/2021/08/24/tutorial-series-of-the-fme-teaching-committee/> fme-teaching.github.io Schedule for FMTea tutorials In the FME Teaching Committee, we are launching a new tutorial series, planned to be held monthly. We aimto increase the awareness and sharing of tools and techniques used for teaching formal methods. The tutorial will be held online via zoom. We will record (whenever the speaker agrees) these presentations and collect them on the FME Teaching Committee website. Below you’ll find the list of speakers who agreed to share their FM teaching insight. We are very happy to announce our second speaker in the series: Dr Ran Ettinger (Ben-Gurion University, Israel, https://www.cs.bgu.ac.il/~ranger/). Ran's lecture is entitled Teaching Cantor’s theorem, a pumping lemma, and the derivation of a heapsort algorithm using Dafny This tutorial will take place this week on Friday (October 29), at 3pm CET. The zoom coordinates are below. The online event is planned to take about one hour, give or take. Everyone welcome!! With best regards, Luigia Petre on behalf of the FME Teaching Committee PS: The recording of Sandrine's lecture last month is already in the webpage https://fme-teaching.github.io/2021/08/24/tutorial-series-of-the-fme-teaching-committee/, where Ran's will also appear soon. Luigia Petre is inviting you to a scheduled Zoom meeting. Topic: FMTea Tutorial Series Time: This is a recurring meeting Meet anytime Join Zoom Meeting https://aboakademi.zoom.us/j/64254430116 Meeting ID: 642 5443 0116 Join by SIP 64254430116@109.105.112.236 64254430116@109.105.112.235 Join by H.323 109.105.112.236 109.105.112.235 Meeting ID: 642 5443 0116 __ Luigia Petre, Docent, PhD Faculty of Science and Engineering Åbo Akademi University, Finland www.users.abo.fi/lpetre ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] FMTea (Formal Methods Teaching) Tutorial series starting soon!
Dear all, In the FME Teaching Committee we are launching a new tutorial series, planned to be held monthly. The idea is to increase the awareness and sharing of tools and techniques used for teaching formal methods. The tutorial will be held online via zoom. We will record (whenever the speaker agrees) these presentations and collect them on the FME Teaching Committee website: https://fme-teaching.github.io. [https://fme-teaching.github.io/media/logo_hub96a365879c5829aace43d4a4da98a91_104111_300x300_fit_lanczos_2.png]<https://fme-teaching.github.io/> Formal Methods Teaching Committee<https://fme-teaching.github.io/> fme-teaching.github.io 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. We are very happy to announce the first speaker in the series: Prof Sandrine Blazy, University of Rennes 1, France, https://people.irisa.fr/Sandrine.Blazy/, who will talk about using the Why3 tool for deductive program verification. This tutorial will take place on September 24, at 3pm CET. The zoom coordinates are below. The online event is planned to take about one hour, give or take. Everyone welcome!! With best regards, Luigia Petre on behalf of the FME Teaching Committee Luigia Petre is inviting you to a scheduled Zoom meeting. Topic: FMTea Tutorial Series Time: This is a recurring meeting Meet anytime Join Zoom Meeting https://aboakademi.zoom.us/j/64254430116 Meeting ID: 642 5443 0116 Join by SIP 64254430116@109.105.112.236 64254430116@109.105.112.235 Join by H.323 109.105.112.236 109.105.112.235 Meeting ID: 642 5443 0116 __ Luigia Petre, Docent, PhD Faculty of Science and Engineering Åbo Akademi University, Finland www.users.abo.fi/lpetre ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] CfP: FMTea21 --> Formal Methods Teaching Workshop and Tutorial, Nov 21, 2021, ONLINE
ices, US - José N. Oliveira, University of Minho, Portugal - Luigia Petre, Åbo Akademi University, Finland - Leila Ribeiro, Federal University of Rio Grande do Sul, Brazil - Kristin Rozier, Iowa State University, US - Pierluigi San Pietro, Politecnico di Milano, Italy - Emil Sekerinski, McMaster University, Canada - Graeme Smith, The University of Queensland, Australia - Kenji Taguchi, CAV, Japan Contact All questions about submissions should be emailed to the chairs. __ Luigia Petre, Docent, PhD Faculty of Science and Engineering Åbo Akademi University, Finland www.users.abo.fi/lpetre ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] FMTea19 CALL for PARTICIPATION: Formal Methods Teaching, on October 7, 2019, in Porto, Portugal
cience series, volume 11758. Please do not hesitate to contact us for any question that may pop up. We are very happy about the FMTea19 program and look forward to meet you all on October 7 in Porto! Kind regards, Luigia Petre, Brijesh Dongol, Graeme Smith (the PC co-chairs) *** Welcome to FMTea19 *** *** Welcome to PORTO *** *** Welcome to Portugal *** __ __ Luigia Petre, Docent, PhD Faculty of Science and Engineering Åbo Akademi University, Finland www.users.abo.fi/lpetre<http://www.users.abo.fi/lpetre> ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] FMTea19, deadline extension: Formal Methods Teaching Workshop and Tutorial
Dear colleagues, Please consider submitting a paper on your experiences with formal methods teaching to our FMTea19 workshop affiliated with the FM conference in Porto in October. We are encouraging a wide spectrum discussion on how we should teach formal methods in the 21st century, so your contribution will be much appreciated. Also note our excellent invited and tutorial speakers: Carroll Morgan, Tony Hoare, and Bas Luttik! Deadline extended to June 15, paper length 15 pages, publication in Springer LNCS. Looking forward to meeting you in Porto for a cup of FMTea, Luigia, Graeme, Brijesh FMTea19 Formal Methods Teaching Workshop and Tutorial, Event affiliated with FM2019, 3rd World Congress on Formal Methods 7 October 2019, Porto, Portugal Deadline extended to June 15, 2019 OBJECTIVES AND SCOPE Formal Methods provide software engineering with tools and techniques for rigorously reasoning about the correctness of systems. While in recent years formal methods are increasingly being used in industry, university curricula are not adapting at the same pace. Some existing formal methods classes interest and challenge students, whereas others fail to ignite student motivation. We need to find ways to teach formal methods to the next generation, and doing so will require us to adapt our teaching to the 21st century students. FMTea19 is a combined workshop and tutorial at the 3rd World Congress on Formal Methods, FM2019. Its aim is to share experiences of teaching formal methods that have gone well, or that failed in surprising ways, as well as to develop ways to reboot the presence of formal methods in curricula. Tutorial part of FMTea19 We are very pleased to have Carroll Morgan giving an invited talk on his approach to and experiences with teaching formal methods to undergraduate students. Sir Tony Hoare will also join us to give a talk on the foundations of teaching computer science for future formal methods scientists. We will run two more tutorial presentations, held by Holger Hermanns and Bas Luttik, on experiences with concurrency and online teaching. Our goal is to discuss various models of existing FM teaching, together with innovative proposals for remaining relevant as educators of Formal Methods in the 21st century. Workshop Part of FMTea19 In the workshop part of the event, we aim to attract papers detailing authors' experiences with FM Teaching. We would like to get papers discussing successes and failures of various methods, case studies, tools, etc. As self-learning seems to be an important aspect of FM teaching, we appreciate experiences with online teaching, including experiences with teaching formal methods via MOOCs. A non-exhaustive list of topics of interest for the FMTea19 workshop is below: * traditional FM teaching: lectures, exercises, exams * online FM teaching/learning: experiences/proposals * teaching FM for industry * integrating/embedding FM teaching/thinking within other computer science courses * student projects on FM, including group projects Computer science is transforming into a rigorous engineering discipline. Improved teaching techniques will ensure that FM is at the heart of this transformation process. ORGANIZATION FMTea19 is organized by FME's Teaching Committee. Our broad aim is to support a worldwide improvement in learning Formal Methods, mainly by teaching but also via self-learning. To that end, we have already gathered a list of FM courses taught worldwide, that can be seen, for the time being, here: https://github.com/luigiapetre/Formal-Methods-Courses/issues (we are in the process of migrating the courses to a webpage, so they will not live much longer as issues) and plan to collect other resources as well, such as FM case studies, FM inspirational papers, etc. PROGRAM COMMITTEE * Luigia Petre, Åbo Akademi University, Finland (co-chair) * Brijesh Dongol, University of Surrey, UK (co-chair) * Graeme Smith, University of Queensland, Australia (co-chair) * Catherine Dubois, ENSIIE, France * Joao F. Ferreira, University of Lisbon, Portugal * K. Rustan M. Leino, Amazon Web Services, US * Alexandra Mendes, University of Beira Interior, Portugal * Leila Ribeiro, Federal University of Rio Grande do Sul, Brazil * Pierluigi San Pietro, Politecnico di Milano, Italy * Kenji Taguchi, CAV, Japan PREVIOUS EDITIONS Several events focused on teaching aspects for Formal Methods were held in the beginning of the 2000s: two BCS-FACS TFM workshops (Oxford in 2003 and London in 2006), the TFM 2004 conference in Ghent (with proceedings published as Springer LNCS Volume 3294), the FM-Ed 2006 workshop (Hamilton, co-located with FM'06), FORMED (Budapest, at ETAPS 2008), and FMET 2008 (Kitakyushu 2008, co-located with ICFEM). The latest event was TFM2009, the 2nd International FME Conference on Teaching Formal Methods, in November 2009 in Eindhoven, the Netherlands. SUBMISSION DETAILS FMTea19 invites high quality papers
