Linked e-resources
Details
Table of Contents
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
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