2022

June

Experience Report on a Student-Organized AI Course

Analyzing Security Aspects of Software Architectures

2021

September

Increasing Student Self-Reliance and Engagement in Model-Checking Courses

March

Testing, Model Checking and Static Analysis – Dream Team or Rivals?

2020

October

Rooting Formal Methods within Higher Education Curricula for Computer Science and Software Engineering

September

Integrating Formal Specifications into Applications - The ProB Java API

July

The First Twenty-Five Years of Industrial Use of the B Method

March

A Verified Low-Level Implementation of the Adaptive Exterior Light and Speed Control System

2019

December

Validation and Real-Life Demonstration of ETCS Hybrid Level 3 Principles Using a Formal B Model

Translating Alloy and Extensions to Classical B

November

Embedding SMT-LIB into B for Interactive Proof and Constraint Solving

Inquiry- and Research-based Teaching in a Course on Model Checking

Prototyping Games Using Formal Methods

September

Embedding High-Level Formal Specifications into Applications

July

Prolog Coding Guidelines: Status and Tool Support

Towards Constraint Logic Programming over Strings for Test Data Generation

June

The History and Evolution of B and Event-B

February

Automated Backend Selection for ProB Using Deep Learning

January

Experience Report on An Inquiry-Based Course on Model Checking

2018

August

Measuring Code Coverage of Prolog Programs Using Mutation Testing

July

Repair and Generation of Formal Models Using Synthesis

May

Writing a Model Checker in 80 Days: Reusable Libraries and Custom Implementation

April

From Software Specifications to Constraint Programming

March

A Translation from Alloy to B

Using a Formal B Model at Runtime in a Demonstration of the ETCS Hybrid Level 3 Concept with Real Trains

January

Three is a crowd: SAT, SMT and CLP on a chessboard

2017

September

plspec - A Specification Language for Prolog Data

Proof Assisted Bounded and Unbounded Symbolic Model Checking of Software and System Models

August

Towards Infinite-State Symbolic Model Checking for B and Event-B

January

Contraint Logic Programming over Infinite Domains with an Application to Proof

2016

June

The Burden of High-Level Languages: Complicated Symbolic Model Checking

May

SMT Solvers for Validation of B and Event-B models

Meta-Predicate for Rodin

Interactive Model Repair by Synthesis

Proof Assisted Symbolic Model Checking for B and Event-B

2015

August

Turning Failure into Proof: The ProB Disprover for B and Event-B

May

Inferring Physical Units in Formal Models

2014

July

From Animation to Data Validation: The ProB Constraint Solver 10 Years On

Turning Failure into Proof: The ProB Disprover

April

Who watches the watchers: Validating the ProB Validation Tool

2013

September

Inferring Physical Units in B Models

Turning Failure into Proof: Evaluating the ProB Disprover

July

B constrained