Experience Report on a Student-Organized AI Course
As curricula are mostly centered around the specializations of faculty members, students are often seen purely as consumers of knowledge.
Analyzing Security Aspects of Software Architectures
As the consequences of cyber attacks are becoming increasingly severe, ensuring the security of safety critical embedded software has become a necessity.
Increasing Student Self-Reliance and Engagement in Model-Checking Courses
Courses on formal methods focus on two aspects: teaching formalisms and exemplary applications as well as teaching techniques for implementing tools such as model checkers.
Testing, Model Checking and Static Analysis – Dream Team or Rivals?
Ensuring reliability and quality of software has become a necessity.
Rooting Formal Methods within Higher Education Curricula for Computer Science and Software Engineering
This white paper argues that formal methods need to be better rooted in higher education curricula for computer science and software engineering programmes of study.
Integrating Formal Specifications into Applications - The ProB Java API
The common formal methods workflow consists of formalising a model followed by applying model checking and proof techniques.
The First Twenty-Five Years of Industrial Use of the B Method
The B-Method has an interesting history, where language and tools have evolved over the years.
A Verified Low-Level Implementation of the Adaptive Exterior Light and Speed Control System
In this article, we present an approach to the ABZ 2020 case study, that differs from the ones usually presented at ABZ: Rather than using a (correct-by-construction) pproach following a formal method, we use MISRA C for a low-level implementation instead.
Validation and Real-Life Demonstration of ETCS Hybrid Level 3 Principles Using a Formal B Model
In this article, we present a concrete realisation of the ETCS Hybrid Level 3 concept, whose practical viability was evaluated in a field demonstration in 2017.
Translating Alloy and Extensions to Classical B
In this article, we introduce a denotational translation of the specification language Alloy to classical B.
Embedding SMT-LIB into B for Interactive Proof and Constraint Solving
The SMT-LIB language and the B language are both based on predicate logic and share the definition of several operators.
Inquiry- and Research-based Teaching in a Course on Model Checking
In this presentation, we discuss a recent publication on our course on model checking.
Prototyping Games Using Formal Methods
Courses on formal methods are often based on examples and case studies, supposed to show students how to apply formal methods in practice.
Embedding High-Level Formal Specifications into Applications
The common formal methods workflow consists of formalising a model followed by applying model checking and proof techniques.
Prolog Coding Guidelines: Status and Tool Support
The importance of coding guidelines is generally accepted throughout developers of every programming language.
Towards Constraint Logic Programming over Strings for Test Data Generation
Software is notoriously hard to test.
The History and Evolution of B and Event-B
The B method for software and systems development together with the specification language B and its successor Event-B offer a rich history.
Automated Backend Selection for ProB Using Deep Learning
Employing formal methods for software development usually involves using a multitude of tools such as model checkers and provers.
Experience Report on An Inquiry-Based Course on Model Checking
The development and improvement of model checkers for the validation of hard- and software is an ongoing research topic in computer science.
Measuring Code Coverage of Prolog Programs Using Mutation Testing
Testing is an important aspect in professional software development, both to avoid and identify bugs as well as to increase maintainability.