Bas Luttik: Revised Semantics for Sequential Composition in the Presence of Intermediate Acceptance
For a smooth integration of classical automata theory and concurrency theory, one would like to consider process algebras including a constant denoting successful termination and binary operations for alternative and sequential composition. Using alternative composition …continue reading
Hans Zantema: Equational reasoning, induction, and infinite data structures
Inductive theorem proving combines equational reasoning and induction to prove properties on ground terms. We present some basics, and show how it also applies in data structures not having a unique representation and in infinite …continue reading
Sofie Haesaert: Robust Dynamic Programming for Temporal Logic Control of Stochastic Systems
Discrete-time stochastic systems are an essential modelling tool for many engineering systems. We consider stochastic control systems that are evolving over continuous spaces. For this class of models, methods for the formal verification and synthesis …continue reading
Maciej Gazda: Logical characterisation of hybrid conformance
The notion of conformance provides a rigorous basis for testing systems. In particular, a notion of hybrid conformance is useful in establishing a formal model-based technique for cyber-physical systems. A logical characterisation of conformance precisely …continue reading
Nobuko Yoshida: Behavioural Type-Based Static Verification Framework for Go
In this talk, first I give an overview of activities in our session type group in Imperial and how mCRL2 is used in our researches. Go is a production-level statically typed programming language whose design …continue reading
Muhammad Osama: SAT Solving using Ant Colony Optimization on GPUs
In this talk, I will discuss how the Boolean Satisfiability (SAT) problem can be solved using a parallel implementation of the Ant Colony Optimization (ACO) algorithm for execution on the Graphics Processing Unit (GPU). We …continue reading
Anton Wijs: The SLCO Framework for Verified, Model-driven Construction of Component Software
I will present the Simple Language of Communicating Objects (\SLCO) framework, which has resulted from our research on applying formal methods for correct and efficient model-driven development of multi-component software. At the core is a …continue reading
Jan Friso Groote: A game that I can win, but don’t know how
After the PhD. defense of Maciej Gazda, I walked back with one of the committee members who explained me a game that he knew he could win, but he would not be able to tell …continue reading
M. Laveaux, T. Neele, O. Bunte: The 201808.0 mCRL2 release
In this talk, we will give an overview of the additions and improvements to mCRL2 from the last couple of years. First, the mCRL2 language has been expanded with the possibility to specify probabilistic behaviour. …continue reading
Rick Erkens: Up-to Techniques for Branching Bisimulation
Branching bisimilarity is a notion of behavioral equivalence between processes. To prove that two processes are branching bisimilar one should provide a relation (a set of pairs) containing the two processes, such that the relation …continue reading