ABSTRACT. Googling Math is fun. returns close to 300 million hits.

Is that part of "the problem" for maths education? Maybe if one says so emphatically that a topic is fun, it reveals actually that it needs special treatment, that it's optional and that students must be enticed to learn it. Of course being a full-blown mathematician is optional --- but it is self-evident that being able to deploy elementary maths in everyday life is not optional, or at least should not be. Yet many adults cannot do even simple arithmetic.

Perhaps Formal Methods is similar: by insisting that it's essential, we might be losing some of our leverage. Of course not everyone has to be a "neat" (vs. a "scruffy"). But it is still true that an appreciation of algorithmic rigour should be compulsory for beginning programmers, together with some idea of how to achieve it in what has become their everyday life. Yet there are many experienced programmers who have never heard of invariants.

So maybe there's a place for elementary formal methods -- for FM by stealth -- to be learned at the same time as one's first-year introduction to programming: not singled out, not separated (and certainly not labelled "formal" or "elementary", and without any extra prerequisites (like logic) beyond what is required for beginners already. Teach assertions about assignments, conditionals, loops (what they establish) at the same time, at first encounter, just as we teach already their syntax (how to write them) and their operational aspects (what they do). And bring to that as much informal intuition as we can muster: use hand-waving, pictures... and even flowcharts, where it all started.

Formal Methods? Let's not call it that: let's call it Programming.

ABSTRACT. This paper shows by examples how the Theory of Programming can be taught to first-year CS undergraduates. The only prerequisite is their High School acquaintance with algebra, geometry, and propositional calculus. The student’s motive is to learn methods of reducing effort required to complete their practical assignments on time, with high marks, and with great enjoyment.

ABSTRACT. This tutorial presents pseuCo, an academic programming language designed to teach concurrent programming. The language features a heavily simplified Java-like look and feel. It supports shared-memory as well as message-passing concurrent programming primitives. The behaviour of pseuCo programs is described by a formal semantics mapping on value-passing CCS or coloured Petri nets, and is made executable using compilation to Java. PseuCo is not only a language but an interactive experience: pseuCo.com provides access to a web application designed for first hands-on experiences with CCS and with concurrent programming patterns, supported by a rich and growing toolset. It provides an environment for students to experiment with and understand the mechanics of the fundamental building blocks of concurrency theory and concurrent programming based on a complete model of the program behaviour. PseuCo and pseuCo.com constitute the centerpiece of an award-winning lecture series, mandatory for Bachelor students at Saarland Informatics Campus.

ABSTRACT. At Eindhoven University of Technology, the majority of students enrolling in our master programme on Embedded Systems have one or more deficiencies in prerequisite bachelor-level knowledge and skills. In the past, we tried to determine such deficiencies on the basis of application data (e.g., a transcript of their bachelor programme), and students were then required to repair them by including one or two bachelor courses in their study programme. This approach was found to be both unreliable and inefficient. To improve, we developed an online homologation recommendation tool by which students can determine to which extent they satisfy the prerequisites of the programme and fully automatically get a recommendation on how to repair deficiencies. Furthermore, we have developed several online self-study homologation modules.

In my talk, I will discuss my experiences with developing both the homologation recommendation tool and the online homologation module "Logic and Set Theory", which addresses prerequisites for the mandatory formal methods course that is part of the Embedded Systems programme. The homologation module consists of over 50 short videoclips and a week-by-week exercise programme. In our experience, the material successfully and efficiently prepares master-level students for an exam of our bachelor course "Logic and Set Theory".

ABSTRACT. Deductive verification of software is a formal method that is usually taught in Computer Science curriculum. But how can students with no strong background in Computer Science be exposed to such a technique? We present in this paper two experiments made at ISAE-SUPAERO, an engineering program focusing on aerospace industry. The first one is a classic lecture introducing deductive methods through the Frama-C platform or the SPARK programming language. The second one is the production by two undergraduate students of a complete guide on how to prove complex algorithms with SPARK. Both experiments showed that students with no previous knowledge of formal methods nor theoretical Computer Science may learn deductive methods efficiently with bottom-up approaches in which they are quickly confronted to tools and practical sessions.

ABSTRACT. In this work, we present a study of different support tools to teach formal verification of Java programs and show our experience with Krakatoa, an automatic theorem prover based on Hoare logic which allows students to interactively visualize the different steps required to prove the correctness of a program, to think about the used reasoning and to understand the importance of verification of algorithms to improve the reliability of our programs.

ABSTRACT. We present the contents of a new formal methods course taught to undergraduate students in their third year at the University of Rennes 1 in France. This course aims at initiating students to formal methods, using the Why3 platform for deductive verification. It exposes students to several techniques, ranging from testing specifications, designing loop invariants, building adequate data structures and their type invariants, to the use of ghost code. At the end of the course, most of the students were able to prove correct in an automated way non-trivial sorting algorithms, as well as standard recursive algorithms on binary search trees.

ABSTRACT. Formal methods are vast and varied. This paper reports the essentials of what I have observed and learned by teaching the Inductive Method for security protocol analysis for nearly twenty years. My fundamental finding is something I realised after just a couple of years, that my target audience of post-graduate students with generally little appreciation of theory would need something different from digging deep down in the wonders of proof ever since class two. The core finding is a decalogue of steps forming the teaching methodology that I have been developing ever since the fundamental finding became clear. For example, due to the nature of the Inductive Method, an important step is to convey the power and simplicity of mathematical induction, and this does not turn out hard upon the sole basis that students are familiar with the informal analysis of security protocols. But the first and foremost step is to convince the learners that they already somewhat used formal methods, although for other applications, for example in the domains of Physics and Mathematics. The discourse will convey as few technicalities as possible, in an attempt to promote the general message that formal methods are not extraterrestrial even for students who are not theorists. The paper introduces all steps individually and justifies them towards the general success of the teaching experience.

ABSTRACT. We present our approach to comprehensibly complement an undergraduate introduction to software engineering course with formal methods.

We discuss our objectives wrt. formal methods, and outline the formal content of the course and the narratives that we use to reach these objectives.

Evaluation results from four seasons of teaching the course give no indication of over-straining students wrt. level or workload.

ABSTRACT. This paper summarises our experience in teaching Formal Methods to Computer Science and Software Engineers students from various universities around the world, including the University of Madeira in Portugal, the Pontificia Universidad Javeriana and the University of The Andes in Colombia, Carnegie Mellon University (CMU) in the USA, and Innopolis University (INNO) in Russia. We report challenges we have faced during the past 10 to 15 years when teaching formal methods using the Event B formalism, and describe how we have evolved the structure of our courses to respond to those challenges. We strive to help students to build skills on Formal Methods that they can employ later on in their future IT jobs in software Industry. Our goal is to promote the wide use of Formal Methods by software Industry. We consider that this goal cannot be achieved without first universities transferring to Industry students with a strong background in Formal Methods and related formal tools. Formal Methods are key to software development because they are based on Discrete Mathematics which can be used to properly reason about properties that the software one develops should have. We have conducted two surveys among our students, the first one at CMU and the second one at INNO, that we use here to document and justify our decisions in terms of the course structure. The first survey is about the use of Event B as main mathematical formalism, and the second one is about the organisation of teams of students within the classroom to work on software projects that use Event B as main mathematical formalism. Our hope is that our work can be reused by other Faculty to make their own decisions on course structure and content in the teaching of their Formal Methods courses.

ABSTRACT. Formal methods provide systematic and rigorous techniques for software development. We are convinced that they must be taught in Software Engineering curricula. In this paper, we present a set of courses about formal methods included in a Software Engineering & Security track of ENSIIE, Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise, a French engineering school delivering the "Ingénieur de l'ENSIIE" degree (master level). These techniques have been taught over the last fifteen years in our education programs in different formats. They definitevely evolve to a large tool support. One of the difficulty we encounter is that students consider these kinds of techniques difficult and requiring much work and thus are inclined to choose other courses when they can. Furthermore students are strongly focused on the direct applicability of the knowledge they are taught, and they are not all going to pursue a professional career in the development of critical systems. Our experience shows that students can gain confidence in formal methods when they understand that, through a rigorous mathematical approach to system specification, they acquire knowledge, skills and abilities that will be useful in their professional future as Computer Scientists Engineers.

ABSTRACT. The construction of correct software, i.e. a computer program that meets a given specification, is an important goal in Computer Science. Nowadays, not only critical software (the ones used in airplanes, hospitals, banks, etc) are supposed to provide additional guarantees of its correctness. Nevertheless, this is not an easy task because proofs are often long and full of details. In this sense, a strong background in logical deduction is essential to provide Computer Science (CS) professionals the necessary competencies to understand and provide mathematical proofs of the programs. Logic courses for CS tend to follow old precepts without emphasising mastering deduction itself. In our institution, for several years we have followed a more pragmatical approach, in which the foundational aspects of both natural deduction and deduction à la Gentzen are taught and, in parallel, the operational premises of deduction are put into practice in proof assistants. Thus, CS students with a minimum knowledge in programming are challenged on providing correctness certificates for simple algorithms. "Putting their hands in the dough" they acquire a better understanding of the value and importance of deductive technologies in computing. Here we show how this is done relating natural deduction, deduction à la Gentzen and using the proof assistant PVS in the simple context of a library of sorting algorithms.

ABSTRACT. In this paper, we report the experience of the authors teaching formal methods to undergraduates in the fourth year of the Software Engineering degree in the University of Málaga. The subject is divided into three blocks devoted to explaining the application of formal methods at different abstraction levels during the process of developing software. Although we teach the theoretical basis for students to understand the techniques, we mainly focus on the practical application of formal methods. Students are asked to realize in pairs three modelling and specifying projects of medium size (one for each block). The practical work corresponds to the 60% of the student evaluation, the remaining 40% is evaluated with a theory exam. We have been teaching the subject during the last five years with very good results.

ABSTRACT. As formal methods come into broad industrial use for verification of safety-critical hardware, software, and cyber-physical systems, there is an increasing need to teach practical skills in applying formal methods at both the undergraduate and graduate levels. In the Aerospace industry, flight certification requirements like the FAA's DO-178B, DO-178C, DO-333, and DO-254, along with a series of high-profile accidents, have helped turn knowledge of formal methods into a desirable job skill for a wide range of engineering positions. We approach the question of verification from a safety-case perspective: the primary teaching goal is to impart students with the ability to look at a verification question and identify what formal methods are applicable, which tools are available, what the outputs from those tools will say about the system, and what they will not, e.g., what parts of the safety case need to be provided by other means. We overview the lectures, exercises, exams, and student projects in a mixed-level (undergraduate/graduate) Applied Formal Methods course taught in an Aerospace Engineering department. We highlight the approach, tools, and techniques aimed at imparting a good sense of both the state of the art and the state of the practice of formal methods in an effort to effectively prepare students headed for jobs in an increasingly formal world.

ABSTRACT. The Gries-Owicki non-interference condition is fundamental to concurrent programming, but difficult to explain as it relies on proof outlines rather than only pre- and postconditions. This paper reports on teaching a practical course on concurrent programming using hierarchical state diagrams to model concurrent programs and argue for their correctness.

ABSTRACT. Discrete Mathematics is an inevitable part of any undergraduate computer science degree programme. However, computer science students typically find this to be at best a necessary evil with which they struggle to engage. Twenty years ago, we started to address this issue seriously in our university, and we have instituted a number of innovations throughout the years which have had a positive effect on engagement and, thus, attainment. At the turn of the century, a mere 2% of our first-year students attained a 1st-class mark (a mark over 70%) in the discrete mathematics course whilst over half of the class were awarded a failing grade (a mark under 40%). Despite the course syllabus and assessment remaining as difficult as ever (if not more challenging), and despite maintaining the same entrance requirements to the programme whilst more than tripling the class size, for the past two years, two-thirds of the class attained Dis

ABSTRACT. Programmers from the imperative tradition often have little experience of using inductive definitions and inference, and that may explain why executable SOS specifications have not become a standard feature of mainstream language development toolkits. We wish to "de-mystify" SOS for such programmers, allowing precise and principled specifications to be given for even small industrial DSL's. eSOS (elided Structural Operational Semantics) is a compact tool for specifying executable formal semantics. It is designed to be a translation target for enriched SOS specification languages. The simplicity of eSOS and its reference Java implementation allow programmers to follow the details of an execution trace, and to step through rules using a conventional debugging framework, allowing them to understand and use SOS-based specifications to construct usable language interpreters.

ABSTRACT. At Kiel University, a course on theory of computation and a course on logic in computer science form the basis for teaching formal methods. Over the last years, new study programs (computer science education, business information systems, international master's programme) have emerged, calling for changes to these courses. Guided by the experience gathered over time, course syllabus, teaching formats, and examination practices were adapted, resulting in a complex scheme. In this paper, we review this development, with particular focus on managing heterogeneity and bridging the gap between actual and required qualification of enrolling students. Key ingredients of our teaching concept are a spiral approach and frequent testing.

ABSTRACT. Much has been written about the challenges of teaching discrete mathematics and formal methods. In this paper we discuss the experiences of delivering a course that serves as an introduction to both. The one-week intensive course, Software Engineering Mathematics, is delivered as part of the University of Oxford's Software Engineering Programme to groups of professional software and security engineers studying for master's degrees on a part-time basis. We describe how a change in the course's emphasis -- involving a shift towards a focus on modelling-based group exercises -- has given rise to some pleasing results.