print · source · login   

Software Science Seminar

Within the Software Science Department, we hold regular talks which are listed here. If you are interested in receiving announcements, please contact Nils Jansen.

Upcoming Talks

Prof. David Parker (University of Birmingham, UK)
Time: 10:30
Date: 11.03.2020
Room: HG00.023
Title: Verification and Strategy Synthesis for Stochastic Games

Abstract: Stochastic multi-player games are a versatile modelling framework for systems that exhibit cooperative and competitive behaviour in the presence of adversarial or uncertain environments. Probabilistic model checking provides a powerful set of techniques to either verify the correct behaviour of such systems or to synthesise controllers that offer guarantees on safe, reliable or timely operation. This talk will provide an overview of work in this direction, implemented within the PRISM-games model checker. This includes recent extensions to concurrent stochastic games and equilibria-based properties, and an applications to a variety of domains, from energy management to communication protocols to robot navigation.

Gerco van Heerdt (University College London, UK)
Time: 10:30
Date: 25.03.2020
Room: HG00.086
Title: Learning Weighted Automata over Principal Ideal Domains

Abstract: In this talk we discuss L*-based automata learning algorithms for weighted automata over a semiring. We provide a general adaptation of the algorithm and show that it works correctly when the semiring is a principal ideal domain. We also show that termination fails in general for an arbitrary semiring, in particular the natural numbers.

This is joint work with Clemens Kupke, Jurriaan Rot and Alexandra Silva.

Dr. Peter Achten (Radboud University)
Time: 10:30
Date: 01.04.2020
Room: HG00.065
Title: Segments: a better Rainfall problem for Functional Programming

Abstract: Elliot Soloway's Rainfall problem (1986) is an extensively studied programming problem, intended to assess students' ability in constructing programs. Many of these studies have used imperative style programming languages. In 2014, Kathi Fisler investigated this problem for students in functional programming, and proposed an adapted, simplified, version of the Rainfall problem. In this talk I briefly recap Fisler's experiment and argue that it actually proves that this version of the Rainfall problem is too easy for students in functional programming and that it uncovers only a small variety of ways to construct a solution to the problem. Instead, I propose another problem, called Segments, that I have been using throughout my courses in Functional Programming (for AI) and I argue that this is a better suited problem for students in functional programming. These results are based on analyzing student assignment results of the past four iterations of the course.

Dr. Freek Verbeek (Open University, Radboud University)
Time: 10:00
Date: 08.04.2020
Room: HG00.217
Title: Formal Proofs of Return Address Integrity

Abstract: We present a methodology for generating a characterization of the memory used by an assembly program, as well as a formal proof that the assembly is bounded to the generated memory regions. A formal proof of memory usage is required for compositional reasoning over assembly programs. Moreover, it can be used to prove low-level security properties, such as integrity of the return address of a function. Our verification method is based on interactive theorem proving, but provides automation by generating pre- and postconditions, invariants, control-flow, and assumptions on memory layout. As a case study, three binaries of the Xen hypervisor are disassembled. These binaries are the result of a complex build-chain compiling production code, and contain various complex and nested loops, large and compound data structures, and functions with over 100 basic blocks. The methodology has been successfully applied to 251 functions, covering 12,252 assembly instructions.

Past talks

Learning and Testing Talks

Previously, this page contained meetings restricted to the Learning and Testing group. The old talks are listed below.

  • Reinier Joosse
    July 5
    Gray-Box Learning of Serial Compositions of Mealy Machines
  • Mahsa Varshosaz
    May 18
    Dynamic Feature Models
  • Lorijn van Rooijen
    January 12th
    Active, Multi-Objective, Coevolutionary Learning of Automata from Examples

In this presentation, I will present our active, coevolutionary and multi-objective approach to learning deterministic finite automata from examples, and its application to requirements engineering. Formal requirements specifications are usually produced, from vague user input, by requirements engineers. It is our aim to automate this process.

From user input in the form of positive and negative example behavior of a desired system, we infer automata that completely describe its behavior. The setting of requirements engineering yields specific challenges, like a small amount of input data and the selection of the right automata from the many automata that are consistent with the input data. Furthermore, the number of queries to the user should be as small as possible.

I will show how our approach deals with these challenges and discuss open questions and future work.

  • Marielle Stoelinga
    September 29th
    Talk as part of SWS seminar
  • Petra van den Bos
    September 22th
    Practising my presentation for ICTSS (and receive some feedback)

Practising my presentation on ICTSS of the paper "n-Complete Test Suites for IOCO"

  • Omar Duhaiby
    June 16th
    Learning an industrial software driver using LearnLib

Omar is a PhD student at the TU/e, applying learning at various companies.

  • SUMBAT meeting
    June 9th
    the SUMBAT project (SUperSizing Model-BAsed Testing) will organize a small workshop

the SUMBAT project (SUperSizing Model-BAsed Testing) will organize a small workshop, presenting first project results.

10:05 Model-Based Testing with TorXakis - Pierre van de Laar (TNO-ESI)

10:30 Model-Based Testing at Oce - Ramon Janssen (RU)

11:10 Model Learning at PANalytical - Jeroen Meijer (UT)

11:35 Model-Based Testing with Complete Test Suites - Petra van den Bos (RU)

  • Alexis Linard
    October 3rd, 14:00 October 4th, 15:00, this is a Tuesday!
    Towards Adaptive Scheduling of Maintenance for Cyber-Physical Systems

Alexis will crash test his presentation for ISoLA conference.

  • Tanja Vos
    September 30th

Tanja Vos will present her testing tool Test*.

  • Petra van den Bos
    August 19th
    Small example and tool demo of ADS algorithm for IOTSes
  • Paul Fiterau
    July 15th
    Tomte determinizer: move to symbolism?

Paul will wish you a very nice holiday, but before that, he will touch on the key aspect of the determinizer in Tomte, how it actually works in the tool, limitations and discuss a move to a more symbolic framework.

  • Ramon Janssen
    July 1st
    Combining Model Learning and Model Checking to Analyze TCP Implementations

Ramon will practice his talk at CAV about learning TCP with abstraction, and model checking with concretization of the abstract models.

  • Jan Friso Groote
    May 27th June 3rd
    An O(m log n) Algorithm for Stuttering Equivalence and Branching Bisimulation

In 1989 Rob van Glabbeek and Peter Weijland defined branching bisimulation as an alternative to weak bisimulation of Robin Milner. Frits Vaandrager and I formulated an algorithm with complexity O(mn) where m is the number of transitions of a labelled transition system and n is the number of states. This was quite a spectacular improvement over weak bisimulation which is cubic due to the transitive tau-closure. At that time there was also the O(mn) algorithm for strong bisimulation, by Kannelakis and Smolka, which was spectacularly improved by Paige and Tarjan to O(mlog n). To me it was open whether the algorithm for branching bisimulation could be improved, until a discussion with Anton Wijs about implementing the algorithms on a GPU, brought me to investigate the paper of Paige and Tarjan in relationship to the branching bisimulation algorithm again. This led to the insight to obtain the current algorithm (except for a small and easily repairable flaw, pointed out by Jansen and Keiren). The algorithm is amazingly complex, but it outperforms existing algorithms by orders of magnitude, especially if systems become large.

A preprint of the paper can be found at

  • Petra van den Bos
    May 27th
    Enhancing Automata Learning by Log-Based Metrics

Petra will practice her talk for iFM 2016

  • MariŽlle Stoelinga
    April 15th Wednesday May 25th 11:00 HG00.086
    Distances on labeled transition systems

In this talk, I will extend the basic system relations of trace inclusion, trace equivalence, simulation, and bisimulation to a quantitative setting in which propositions are interpreted not as boolean values, but as real values in the interval [0,1]. Trace inclusion and equivalence give rise to asymmetrical and symmetrical linear distances, while simulation and bisimulation give rise to asymmetrical and symmetrical branching distances. I will present the relationships among these distances, and we provide a full logical characterization of the distances in terms of quantitative versions of LTL and μ-calculus. I will show that, while trace inclusion (resp. equivalence) coincides with simulation (resp. bisimulation) for deterministic boolean transition systems, linear and branching distances do not coincide for deterministic quantitative transition systems. Finally, I will go into algorithms for computing the distances.

(This work dates back to when I was at UC Santa Cruz and is joint work with Luca de Alfaro and Marco Faella)

  • Mark Janssen
    April 8th
    [Combining active learning with fuzzing]
  • Petra van den Bos
    March 18th

trial presentation ICT.OPEN

  • Rick Smetsers
    March 11th
    Separating sequences for all pairs of states

Rick will practice his talk for LATA 2016 about finding minimal separating sequences for all pairs of state in O(n log n).

  • Jan Tretmans
    March 4th
    Workshop TorXakis
  • David N. Jansen
    January 29th
    An O(m log n) Algorithm for Stuttering Equivalence and Branching Bisimulation

David will talk about a paper by Jan Friso Groote Anton Wijs:

  • Alexander Fedotov
    December 11th
    The hybrid UIO method

I will report on my research internship.

  • Joshua Moerman
    November 27th
    The different learning algorithms for register automata

I will discuss the differences between the various learning algorithms for register automata. This includes the abstract learning algorithm from nominal automata, our tool Tomte and RAlib from Uppsala (and maybe more).

  • Petra van den Bos
    November 6th
    Adaptive distinguishing sequences for deterministic IOTSes

As far as I know, there only exist random test methods to generate test cases from an LTS/IOTS-model. I will discuss an adapted version of the FSM-based Lee and Yannakakis-method to find adaptive distinguishing sequences. These sequences enable a smarter and more directed way of testing.

  • Alexis Linard
    October 30th
    Preliminary work on Printhead Failure Prediction

As part of the Cyber-Physical Systems project in partnership with Ocť, my current goal is to use Machine Learning (and other) techniques in order to predict printers failures. I will present here not only the current achievements or Machine Learning techniques employed, but also the main challenges to be completed. My presentation will also trigger a debate on the multidisciplinarity of the project.

  • Paul Fiterau-Brostean
    October 23th
    Learning Register Automata with Fresh Value Generation

I will give a brief overview on our CEGAR based algorithm and detail on how we have extended this algorithm to handle fresh output values. I will also talk on some of the optimizations we've made to the algorithm, and to the tool implementing it. The presentation is going to be a draft version of what I am going to present in Colombia next week.