This article reports our 7-year activity to introduce the formal method, B-Method to our college. Our activity mainly includes the mandatory short-term experiment for the whole member of the 4th-grade class (the age of 18 or 19), with few prerequisites about the logical mathematics. Under the time constraints - the course of only 140 min. per week, two or three weeks -, our experiment covers all of three fields: formal specification, proof obligation generation and model checking, and also gives the students the opportunities to briefly experience of state explosion problem. The authors set the educational goal for the experiments as giving opportunities to commit a formal method as the software engineer’s fundamental knowledge. The authors also arranged the short-time - at most 3-hour - lectures for people other than the students mentioned above who cannot write a logical predicate at all. The goal of this lecture is to give them the opportunity to find tacit facts with sound reasoning from documents. On a web page ( https://www.asahi-net.or.jp/ ny9t-oons/b-method_english.html ), the authors uploaded details - course materials, contents of models and the results of survey questions -. As far as the data of the survey questions show, it seems that the educational goal for the experiments is achieved, our experiment and lecture seem to be generally accepted, but there are some abilities to improve the methodology within the time constraint of the course.
Formal methods are often perceived by students as abstract and disconnected from real software development, particularly when addressing concurrent systems. This paper reports on an experience of teaching formal methods in a Master-level course through project-based learning, using the Anemone workbench and the Multi-Bach coordination language. Rather than relying on small artificial examples, students apply formal modelling to parts of their own projects involving concurrency and coordination. Animation and trace inspection support the exploration of dynamic behaviours and interleavings, helping students connect formal descriptions to intuitive system behaviour. We describe the course context and representative student projects, and report observations on engagement, recurring modelling difficulties, and learning outcomes. We also discuss limitations of the approach, including tool-learning overhead and scalability concerns. Overall, the experience suggests that tool-supported projects can make formal methods more accessible and meaningful for advanced students while preserving their formal foundations.
Autograding has been widely used in programming courses for decades. It reduces the marking load on teaching staff, providing them with more time to give higher quality feedback. There is relatively little work, however, on autograding in formal methods courses where the emphasis is not on programming, but on writing proofs and specifications. This paper describes a tool which employs the proof capabilities of Dafny to automatically grade students’ weakest precondition proofs and Dafny method specifications. The tool has been designed to (i) be reusable for new versions of assignments, with minimal input from teaching staff, (ii) allow fine-grained marking, in order to give students part marks for partially correct solutions, and (iii) not artificially constrain students’ use of programming techniques where they need to provide code as well as specifications, allowing them to apply best programming practices. The paper evaluates the use of the tool over two assignments of a course with 217 undergraduate and Masters students and highlights lessons learnt.
Developing highly reliable software requires the use of formal verification methods, but integrating them into the education of IT students is difficult due to the gap between theoretical understanding and practical skills. In this paper, we present the design, implementation, and analysis of VeHa-2025, a national verification hackathon aimed at overcoming these challenges through hands-on learning, particularly through competitions focused on specific verification problems. Our event combines tracks in model checking (SPIN, TLA+) and deductive verification (Isabelle/HOL, Coq-Rocq, Why3, C-lightVer). Launched in 2023 as a volunteer initiative by a group of academics, VeHa evolved into an academy-industry partnership by 2025. VeHa-2025 included a structured educational cycle consisting of preparatory workshops, an invited lecture, a three-day competitive problem-solving period, and a post-event verification of solutions. The analysis of metrics, submitted solutions, and participant feedback presented in this article demonstrates the growing effectiveness of our hackathon in developing practical skills, building a community, and equipping participants with competencies in formal methods that are in demand in industry. We argue that such competitive, practice-oriented formats are a valuable pedagogical tool for motivating and training the next generation of software verification engineers.
Alloy is a lightweight formal method that is well suited to teaching logic because it combines expressive logics with automatic analysis and visual feedback. In this paper, we report our experience using specification challenges on the Alloy4Fun platform in our formal methods courses. We briefly describe the types of challenges we have used over the years and discuss how different hints can help students make progress in solving them. Our main conclusion is that specification challenges are highly engaging and useful for students, but they should be balanced with broader modeling and validation activities to support long-term learning outcomes. They are also useful for research, because Alloy4Fun’s data-collection infrastructure enables the release of open datasets that can be mined for insights into Alloy usage and for the evaluation of new tools and techniques.
