Formal methods teaching : third International Workshop and Tutorial, FMTea 2019, held as part of the third World Congress on Formal Methods, FM 2019, Porto, Portugal, October 7, 2019, Proceedings / Brijesh Dongol, Luigia Petre, Graeme Smith (eds.)

Includes bibliographical references and author index.

Online resource; title from PDF title page (SpringerLink, viewed September 27, 2019).

Intro; Preface; Organization; Invited/Tutorial Lectures; Is Formal Methods Really Essential?; pseuCo.com; Efficient Online Homologation to Prepare Students for Formal Methods Courses; Contents; Tutorial Lectures; Logic, Algebra, and Geometry at the Foundation of Computer Science; 1 Introduction; 2 Algebra and Logic; 2.1 Boolean Algebra; 2.2 Deductive Logic; 2.3 Spatio-Temporal Logic; 3 Sequential Composition; 3.1 Hoare Triples; 3.2 Verification Rules for Sequential Composition; 3.3 Milner Transition; 4 Concurrent Composition; 4.1 Interchange; 4.2 Basic Principle of Concurrent Programming

4.3 Unifying Theories of Concurrency5 Related Work; 6 Conclusion; References; Teaching Program Verification; Teaching Deductive Verification Through Frama-C and SPARK for Non Computer Scientists; 1 Introduction; 2 Why Is It Difficult to Teach Formal Methods at ISAE-SUPAERO?; 2.1 The ISAE-SUPAERO Engineering Program; 2.2 The Challenges; 2.3 Why Teaching Formal Methods at ISAE-SUPAERO?; 3 Introducing Formal Methods in 17 h; 3.1 Deductive Verification with Frama-C and SPARK; 3.2 A Top-Down Approach with Frama-C; 3.3 A Bottom-Up Approach with SPARK; 3.4 Comparison of Both Approaches

4 The SPARK by Example Experiment: Learning from Examples4.1 What Is SPARK by Example?; 4.2 A Corpus of Proved Algorithms; 4.3 Lessons Learnt; 5 Conclusion; References; Using Krakatoa for Teaching Formal Verification of Java Programs; 1 Introduction; 2 Context of Our Experience; 3 Study of Different Alternatives; 4 Some Examples of Formal Verification with Krakatoa; 4.1 Lectures in the Computer Classroom; 4.2 Exercises in the Computer Classroom; 4.3 The Exam; 5 Results of the Experience; 6 Conclusions and Further Work; References

Teaching Deductive Verification in Why3 to Undergraduate Students1 Introduction; 2 Background on Why3; 3 Learning to Write Precise Specifications; 3.1 Testing of Specifications; 3.2 Testing Larger Specifications; 3.3 Loop Invariants; 4 Towards More Complex Specifications; 4.1 Type Invariants; 4.2 Ghost Code; 5 Proving Recursive Programs; 6 Conclusion; References; Teaching Program Development; Teaching Formal Methods to Future Engineers; 1 Introduction; 2 ENSIIE; 3 Software Engineering and Security Track; 4 Formal Methods for Reliable Systems (MFDLS)

5 Mechanized Formal Proof and Semantics (PROG1)6 Static Analysis and Deductive Verification (PROG2); 7 Conclusion; References; The Computational Relevance of Formal Logic Through Formal Proofs; 1 Introduction; 2 Logical Deduction Frameworks; 3 Logical Deduction versus Proof Commands; 4 Inductive Proofs Versus Recursive Algorithms; 5 Related Work and Conclusions; References; Teaching Formal Methods: From Software in the Small to Software in the Large; 1 Introduction; 2 Content of the Subject; 2.1 Model Checking/SPIN; 2.2 Alloy; 2.3 UML/OCL; 3 Methodology; 3.1 Model Checking; 3.2 Alloy; 3.3 OCL

This book constitutes the refereed proceedings of the Third International Workshop and Tutorial, FMTea 2019, Held as Part of the Third World Congress on Formal Methods, FM 2019, Porto, Portugal, October 2019. The 14 full papers presented together with 3 abstract papers were carefully reviewed and selected from 22 submissions. The papers are organized in topical sections named: Tutorial lectures; Teaching Program Verification; Teaching Program Development; and Effective Teaching Techniques. -- Provided by publisher.