We present early results of our new GPUdecide BDD package, which optimizes BDD operations for the GPU. It represents BDDs and computes operations in an unconventional way inspired by Adiar, which was designed to perform BDD operations in external memory. As GPUdecide is not feature complete yet, we do not have a large set of …continue reading

Artificial intelligence (AI) have become rather ubiquitous in the past decade, especially Machine Learning (ML) models. As we accelerate towards a future entangled with such tools, models exhibiting undesired behavior or experiencing catastrophic failures may severely impact human society. In response, there has been an increase in interest towards establishing trust for ML models—a surge …continue reading

There is a noticeable increase in investment towards security in teams building embedded systems driven by regulators in the USA, Europe and Japan that are demanding more attention on security from device vendors. Industry is scrambling for a solution, both downwards starting from requirements as well as upwards starting from an implementation. At the same …continue reading

In April 2024, Hans Zantema told me about a nice coloring problem: if you color the fields of an n^2+n-1-sided square with n colors, then there must be a rectangle that has four equally colored corners. In the talk I will discuss Hans’ proof and his construction of an n^2-sided square without such rectangles, my …continue reading

This talk will give an introduction to Alloy, a formal specification tool for bounded analysis. Originally Alloy was developed as a lightweight approach to formally verify software, and indeed, many case studies show its strength in finding non-trivial bugs. Today we will start small by using Alloy to solve a simple puzzle. Once we are …continue reading

This talk will cover a method to analyze Markov Automata using a dynamic discretization. Markov Automata are continuous models which exhibit both probabilistic and non-deterministic behaviour. Previously, discretization methods have been developed to approximate reachability queries in the continuous model by analyzing its discrete counterpart (MDPs). This approach partitions the time-interval in small, constant size, …continue reading

This talk will provide a brief introduction to probabilistic model checking using the Storm model checker. I will demonstrate how to model a simple board game as a Markov process using the Stormvogel Python library. This interactive library provides user-friendly modeling and visualization capabilities for probabilistic models. Then, we will analyze the game via model …continue reading

It is very hard to determine the reliability of software, given that programmers can make errors, compilers may have flaws or hardware may malfunction. There are many proposed techniques to determine the reliability of software, but none seem to work well. In this talk I propose to use quantitative model checking as a means to …continue reading

Parameterized Boolean equations systems (PBES) are used to verify properties of formal industrial models such as the Princess Marijke lock complex. In this talk, we discuss a technique to simplify these PBES that seems especially effective for verifications problems resulting from large industrial models.

Large Language Models (LLMs) have become increasingly popular for code generation. In particular, smaller tasks such as API development can be effectively delegated to LLMs. However, as task complexity increases, the reliability of LLM-based code generation tends to decrease. To address this limitation, in 2023 we proposed integrating LLM-based code generation into our language-driven software …continue reading