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

After Joshua's talk, we will have a summer break and be back mid August.

**Dr. Joshua Moerman** (RWTH Aachen University)**Time:** 10:30**Date:** 15.07.2020**Room:** Virtual**Title**: Residuality and Learning for Nondeterministic Register Automata

**Abstract**: In this research we consider the problem of inferring a register automaton
from observations. This has been done before for deterministic RA, but is
still open for nondeterministic RA. To see why nondeterminism is interesting,
consider the well-known learning algorithms L* and NL* for respectively
deterministic and nondeterministic automata. Although the representation is
different, they operate on the same class of languages (i.e., regular
languages). This is not the case for RA, where nondeterminism gives a strictly
bigger class of languages than determinism. So not only does the
representation changes, so does the class of languages.

Our contributions are as follows. This is joint work with Matteo Sammartino. - We consider \emph{residual automata} for data languages. We show that their languages form a proper subclass of all languages accepted by nondeterministic RA. - we give a \emph{machine-independent characterisation} of this class of languages. For this, we also develop some new results in nominal lattice theory. - We show that for this class of languages, L*-style algorithms exist. - The natural generalisation of NL* does not always terminate, surprisingly. Fortunately, the algorithm can be fixed to always terminate.

**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.

**Dr. Peter Achten** (Radboud University)**Time:** 10:30**Date:** 01.04.2020**Room:** Virtual**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:** Virtual**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.

**Prof. Frits Vaandrager** (Radboud University)**Time:** 10:30**Date:** 22.04.2020**Room:** Virtual**Title**: State Identification for Labeled Transition Systems with Inputs and Outputs

**Abstract**: For Finite State Machines (FSMs), a rich testing theory has been developed to discover aspects of their behavior and ensure their correct functioning. Although this theory is widely used, e.g. to check conformance of protocol implementations, its applicability is limited by restrictions of the FSM framework: the fact that inputs and outputs alternate in an FSM, and outputs are fully determined by the previous input and state. Labeled Transition Systems with inputs and outputs (LTSs), as studied in ioco testing theory, provide a richer framework for testing component oriented systems, but lack the algorithms for test generation from FSM theory. In this article, we propose an algorithm for the fundamental problem of state identification during testing of LTSs. Our algorithm is a direct generalization of the well-known algorithm for computing adaptive distinguishing sequences for FSMs proposed by Lee & Yannakakis. Our algorithm has to deal with so-called compatible states, states that cannot be distinguished in case of an adversarial system-under-test. Analogous to the result of Lee & Yannakakis, we prove that if an (adaptive) test exists that distinguishes all pairs of incompatible states of an LTS, our algorithm will find one. In practice, such adaptive tests typically do not exist. However, in experiments with an implementation of our algorithm on a collection of (both academic and industrial) benchmarks, we find that that tests produced by our algorithm still distinguish more than 99% of the incompatible state pairs.

This is joint work with Petra van den Bos.

**Gerco van Heerdt** (University College London, UK)**Time:** 10:30**Date:** 29.04.2020**Room:** Virtual**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. Daniel Strüber** (Radboud University)**Time:** 10:30**Date:** 13.05.2020**Room:** Virtual**Title**: Towards Model-Driven Search Engineering

**Abstract**: Optimization problems pervade every aspect of our lives, notably in domains such as healthcare, education, logistics, and finance, where limited resources must be distributed efficiently. For instance, a hospital needs to allocate staff, equipment, and beds in a way that ensures economic feasibility as well as patient dignity and privacy. A wealth of optimization techniques is available for addressing such problems. Choosing an optimization technique that matches the assumptions and requirements of a given problem, and applying it in a beneficial way, requires substantial knowledge on optimization techniques. We present our recent work on bridging the gap between high-level optimization requirements and low-level optimization techniques, based on model-driven engineering technology: First, on the automated generation of sound and complete search operators, in the application domain of software product line configuration. Second, on the automated generation of efficient search operators for arbitrary given problem domains. Third, on the automated analysis of search operators w.r.t. their impact on the consistency of solution candidates. Fourth, on first steps towards support for choosing from multiple back-end optimization technologies.

**Dr. Jurriaan Rot** (Radboud University)**Time:** 10:30**Date:** 20.05.2020**Room:** Virtual**Title**: Coalgebra Learning via Duality

**Abstract**: Automata learning is a popular technique for inferring minimal
automata through membership and equivalence queries. We generalise
learning from automata to a large class of state-based systems, using
the theory of coalgebras. The approach relies on the use of logical
formulas as tests, based on a dual adjunction between states and
logical theories. This allows us to learn, e.g., labelled transition
systems.

Joint work with Clemens Kupke and Simone Barlocco.

**Niels van der Weide** (Radboud University)**Time:** 10:30**Date:** 03.06.2020**Room:** Virtual**Title**: Constructing Higher Inductive Types

**Abstract**: Higher inductive types (HITs) provide a way to define data types by describing how to construct inhabitants and when their inhabitants are equal. Examples of HITs include quotient types, finite sets, and finite bags. In this talk, we study HITs more closely in the setting of homotopy type theory, which is a version of type theory with proof relevant equality. More specifically, we show how to construct a certain class of higher inductive types as quotients.

**Dr. Pieter Koopman** (Radboud University)**Time:** 10:30**Date:** 10.06.2020**Room:** Virtual**Title**: Dynamic Editors for Well-Typed Expressions

**Abstract**: Interactive systems can require complex input from their users.
A grammar specifies the allowed expressions in such a Domain Specific Language, DSL.
An algebraic DataType, ADT, is a direct representation of such a grammar.
For most end-users a structured editor with pull-down menus is much easier to use than a free text editor.
The iTask system can derive such structured editors based on an ADT using datatype generic programming.
However, the input DSL has often also semantical constraints, like proper use of types and variables.
A solution is to use a shallow embedded DSL or a DSL based on a Generalized ADT to specify the input.
However, such a specification cannot be handled by datatype generic programming.
Hence, one cannot derive structured editors for such a DSL.

As a solution we introduce structured web-editors that are based on dynamic types. These dynamic types are more expressive; they can express the required DSL constraints. In the new dynamic editor library we need to specify just the dynamic relevant for the DSL. The library takes care of displaying the applicable instances to the user and calls itself recursively to create the arguments of the dynamic functions. In this paper we show how this can be used to enforce the requires constraints on ADTs, to create structured web-editors for shallow embedded DSLS, and to create those editors for GADT based DSLs.

**Prof. Sven-Bodo Scholz** (Radboud University)**Time:** 10:30**Date:** 17.06.2020**Room:** Virtual**Title**: 50 Shades of Laziness

**Abstract**: Lazy evaluation has very appealing properties: it terminates whenever
possible and it evaluates as little as needed for the overall result. The price
for these properties is a loss of concurrency and a potentially uncontrollable need
for space. Consequently, many languages, in particular those aiming for high
parallel performance, employ eager evaluation. Attempts to combine the benefits
of the two approaches are traditionally based on argument-specific annotations,
special data types, or on strictness analyses.
In this talk, we present a new approach to combining the two. The key idea is
to leverage the binding time analyses from offline partial evaluation within
the definition of the language semantics. This allows us to keep the favourable
runtime behaviour of eager evaluation and yet acquire some of the benefits of
lazy evaluation. We present our ideas in the context of the high-performance
array programming language SaC.

**Jana Wagemaker** (Radboud University)**Time:** 10:30**Date:** 24.06.2020**Room:** Virtual**Title**: Partially Observable Concurrent Kleene Algebra

**Abstract**: In this talk I'll start with a general introduction to Kleene algebra and how it can be used to study simple programs. Hopefully, I'll be able to sketch the broader context in which to place the newest edition to the KA-family: Partially Observable Concurrent Kleene Algebra (POCKA), a sound and complete algebraic framework to reason about concurrent programs with control structures, such as conditionals and loops.
POCKA enables reasoning about programs that can access variables and values, which I illustrate with a concrete example. The example revolves around an important check for sequential consistency.

**Markus Klinik** (Radboud University)**Time:** 10:30**Date:** 01.07.2020**Room:** Virtual**Title**: no-bs: how to grade student assignments on Brightspace without using Brightspace

**Abstract**: The course Object Orientation has more than 400 students, who work in teams of
two to hand in one assignment project every week.

In this talk we discuss the workflow and the tool no-bs that we have developed to streamline grading student assignments. no-bs is a command-line program that can interface with the Brightspace web API. It downloads submissions from Brightspace to your computer. You fill in a feedback template text file, and no-bs uploads grades and feedback to Brightspace.

The workflow we use has 17 teaching assistants and one coordinator, and is built around no-bs, the old bb-scripts, and exchanging data on a network share. Only the coordinator has to touch Brightspace, the teaching assistants just have to fill in the feedback template using their favourite text editor. no-bs has been developed to scratch our own itch, but it can be adapted to other workflows as well.

**Dan Frumin** (Radboud University)**Time:** 10:30**Date:** 08.07.2020**Room:** Virtual**Title**: Relational reasoning in Concurrent Separation Logic

**Abstract**: Relational reasoning plays an important role in programming
languages, as many important properties of programs are relational.
For example, contextual equivalence is used to show that optimized
versions of data structures behave the same as their non-optimized
counterparts and that concurrent data structures are linearizable.
Non-interference is used to show that a program does not leak secret
information.

In this talk I will describe recent developments in concurrent separation logic (specifically the Iris framework in the Coq proof assistant), that enable modular and mechanized relational reasoning in the context of higher-order programming languages with fine-grained concurrency.

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.

**Frits Vaandrager**

November 3rd

Learning Mealy machines with timers (practising my presentation for the IPA Fall days)

**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*Test**

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 http://arxiv.org/abs/1601.01478

**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*TBA*

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: http://arxiv.org/abs/1601.01478

**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.