Herman Geuvers: “Computer Assisted Mathematical Proofs: using the computer to verify computers”
A “Proof Assistant” is a computer program that allows users to create complete mathematical proofs, interactively with the computer, where the computer checks each small reasoning step. In this way one obtains the utmost guarantee of correctness. I will outline how Proof Assistants work, how they are used to verify mathematical proofs and computer systems. Verifying a proof with a …continue reading
Olav Bunte: Asynchronously communicating OIL components
In this presentation we focus on how we envision OIL components to communicate with each other. We define the behaviour of communicating OIL components using a formalism found in literature, namely the FIFO system, and we show how this can be modelled in mCRL2. Also, we show some typical unwanted behaviour in asynchronous communication and …continue reading
Jeroen Keiren: Understanding Mutual Exclusion Algorithms using mCRL2’s counterexamples
Last week, Myrthe Spronck discussed mutual exclusion algorithms when using safe registers. In this week’s talk, I will stick with the topic of mutual exclusion algorithms, but switch back to using atomic registers. I will introduce Dekker’s algorithm for mutual exclusion. According to Dijkstra, this is the first algorithm to solve mutual exclusion between two …continue reading
Myrthe Spronck: Safe registers and Aravind’s BLRU algorithm in mCRL2
For my bachelor research project, supervised by Bas Luttik, I set out to verify Aravind’s bounded least recently used (BLRU) algorithm for mutual exclusion using mCRL2. An interesting property of Aravind’s algorithm is that it can ensure mutual exclusion even when the registers used are safe, rather than atomic. In order to verify this property, …continue reading
Mark Bouwman: A formalisation of SysML state machines in mCRL2
My talk this Thursday will consist of three parts. (10 -15 min) I will practice my talk for FORTE, where I will present the paper “A formalisation of SysML state machines in mCRL2”. This paper reports on a formalisation of the semi-formal modelling language SysML in the formal language mCRL2. The formalisation focuses on a …continue reading
Alexander Fedotov: McMillan’s algorithm for SAT-based unbounded model checking.
In this talk, I will discuss McMillan’s algorithm for fully SAT-based unbounded symbolic model checking. The method is based on computing Craig interpolants. In terms of performance, the algorithm is substantially more efficient than BDD-based model checking. I will also explain how we modify McMillan’s algorithm to analyze the backward reachability of initial states from …continue reading
Flip van Spaendonck: Understanding std::memory_order in C++11 using MCA semantics
C++11 introduced many tools to write safe multi threaded code. One of those tools are the std::memory_orders, which specify how memory accesses, including regular, non-atomic memory accesses, are to be ordered around atomic operations. Understanding these memory orders can be quite a complex situation, specifically when different memory orders are combined. We will try to make …continue reading
Geert van Ieperen: Visualisation of large Labelled Transition Systems
A formal model describes the behaviour of a program, protocol or other system. The properties of this model can be verified, such that we can prove these properties with absolute certainty. Visualising the state space of a formal model is an important tool for their development. This thesis focuses on visualising such a state space …continue reading
Anna Stramaglia: Deadlock in packet switching networks
A deadlock in a packet switching network is a state in which one or more messages have not yet reached their target, yet cannot progress any further. We formalize three different notions of deadlock in the context of packet switching networks, to which we refer as global, local and weak deadlock. We establish the precise …continue reading
Muhammad Osama: SAT Solving with GPU Accelerated Inprocessing
Since 2013, the leading SAT solvers in the SAT competition all use inprocessing, which unlike preprocessing, interleaves search with simplifications. However, applying inprocessing frequently can still be a bottle neck, i.e., for hard or large formulas. In this work, we introduce the first attempt to parallelize inprocessing on GPU architectures. As memory is a scarce …continue reading