Formal Methods Teaching: 4th International Workshop and Tutorial, FMTea 2021, Virtual Event, November 21, 2021, Proceedings

Description

This book constitutes the refereed proceedings of the 4th International Workshop and Tutorial, FMTea 2021, Held as Part of the 4th World Congress on Formal Methods, FM 2021, as a virtual event in November 2021. The 8 full papers presented together with 2 short papers were carefully reviewed and selected from 12 submissions. The papers are organized in topical sections named: experiences and proposals related with online FM learning and teaching, integrating/embedding FM teaching/thinking within other computer science courses, teaching FM for industry, and innovative learning and teaching methods for FM. Preface Organization Invited Talks Teaching Logic and Mechanized Reasoning with Lean 4 Automating Teaching Efforts for Deductive Verification Teaching Data Structures and Algorithms with a Proof Assistant Contents Introducing Formal Methods to First-Year Students in Three Intensive Weeks 1 Introduction 2 Context for the Course 3 Goals and Overall Philosophy of the Course 4 Structure of the Course 4.1 Week One: Warming up 4.2 Week Two: First Project 4.3 Week Three: Second Project and Final Exam 5 The Two Pandemic Editions 6 Evaluation and Conclusions References Online Teaching of Verification of C Programs in Applied Computer Science 1 Introduction 2 Background 2.1 University of Applied Sciences 2.2 C Program Verification 3 Verification Approaches and Tools 3.1 Deductive Verification 3.2 Abstract Interpretation 3.3 Software Bounded Model-Checking 4 Online Teaching 5 Exercise Selection 5.1 Exercise 1—Informal Specification 5.2 Exercise 2—First Order Logic 5.3 Exercise 3—Hoare Logic 5.4 Exercise 4—Deductive Verification Using Frama-C 5.5 Exercise 5—Arrays 5.6 Exercise 6—Runtime Errors 5.7 Exercise 7—Abstract Interpretation 5.8 Exercise 8—Bounded Model Checking 6 Evaluation 6.1 Challenges for Students 6.2 Results 6.3 Student Evaluation of the Course 7 Conclusion and Outlook References A Proposal for a Framework to Accompany Formal Methods Learning Tools 1 Learning Tools in Theoretical Computer Science 2 The Proposed Didactic Framework 3 Two Exemplary Instances of the Proposed Framework 4 Conclusion References Increasing Engagement with Interactive Visualization: Formal Methods as Serious Games 1 Introduction 2 Background and Related Work 3 Proof Calculi as Serious Games 3.1 Formal Methods Are Serious Games 3.2 Teaching Methods 3.3 KalkulierbaR 4 Discussion 5 Conclusion References Increasing Student Self-Reliance and Engagement in Model-Checking Courses 1 Introduction 2 Context 3 Course Evolution 3.1 The Origins: a Classical Lecture-Based Course 3.2 First Iteration: Introducing Research- and Inquiry-Based Learning 3.3 Second Iteration: Lessons Learned: Mixing Lecture and Practical Exercises 3.4 Third Iteration: Improved Teaching Methods and Online Teaching 4 Comparison of Grades 5 Conclusions References Teaching Formal Methods to Software Engineers through Collaborative Learning (Short Paper) 1 Introduction 2 Course Context and Structure 3 Introducing Collaborative Learning 4 Group Assignment: Goals and Structure 4.1 Educational Goals 4.2 Project Content: Model-Checking for Warehouse Robotics 5 Evaluation Survey Results 6 Conclusion References Lessons of Formal Program Design in Dafny 1 Introduction: About the Course 2 Lessons 10–12: Insertion Sort 2.1 Specification for a Sorting Algorithm 2.2 Refinement Steps 1–5: The Outer Loop 2.3 Refinement Steps 6–10: The Inner Loop 2.4 A Final Step of Refinement: Swapping Adjacent Array Elements 3 Assessment References Teaching Correctness-by-Construction and Post-hoc Verification – The Online Experience 1 Introduction 2 Related Work 3 Teaching Formal Methods – Software Quality 2 4 Verification Techniques and Tool Support 4.1 Post-hoc Verification 4.2 Correctness-by-Construction 5 User Study Design 5.1 General User Study Design 5.2 Differences in the First and Second User Study 6 Results and Discussion 6.1 Defects in Implementation and Specification 6.2 User Experience 6.3 Discussion of the Research Questions 6.4 Threats to Validity 7 Lessons Learned for Online Teaching References Using Isabelle in Two Courses on Logic and Automated Reasoning 1 Introduction 2 Related Work 3 Curricular Overview 4 BSc Course: Logical Systems and Logic Programming 5 MSc Course: Automated Reasoning 6 Discussion and Future Work 7 Conclusion References Introducing Formal Methods to Students Who Hate Maths and Struggle with Programming 1 Introduction 2 Introducing Formal Methods into a Concurrency Course 3 Assessments - Traditional and Online 4 Formal Methods Before University 5 Related Work 6 Conclusion References Author Index