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

**Jonas Kastberg Hinrichsen** (University of Copenhagen, DK)**Time:** 10:30**Date:** 18.11.2020**Room:** online**Title**: Actris: session-type based reasoning in separation logic

**Abstract**: Message-passing is a principled approach to writing concurrent software.
To verify message-passing behaviour in a scalable fashion,
it is useful to have a first class approach to reasoning about it.
Such an approach should integrate seamlessly with other low-level concurrency
reasoning, as combining message passing with other concurrency mechanisms,
such as locks, is commonplace.

In this talk I will present our work "Actris", a logical framework for thread-local reasoning about message passing, which combines separation logic with session types, originally presented at POPL'20. In doing so, I will cover the Actris protocol mechanism of "dependent separation protocols", showing how they can be used to verify a set of feature-rich examples, including the integration with lock-based concurrency. I will additionally present a recent extension of Actris to Actris 2.0, introducing the novel idea of "subprotocols", inspired by that of asynchronous session subtyping, to fully exploit the expressivity of asynchronous message passing. I will then show how dependent separation protocols have been used to prove type soundness of an expressive session type system, using the technique of semantic typing, to draw a formal connection between the dependent separation protocols and the session types that inspired them. Finally, I will provide insight into the model of Actris, based on step-indexing, and how we managed to fully mechanise it in Coq, by building it on top of the Iris logical framework.

**Dr. Benjamin Kaminski** (University College London (UCL), UK)**Time:** 10:30**Date:** 25.11.2020**Room:** online**Title**: Quantitative Separation Logic

**Abstract**: We present quantitative separation logic (QSL). In contrast to classical separation logic, QSL employs quantities which evaluate to real numbers instead of predicates which evaluate to Boolean values. The connectives of classical separation logic, separating conjunction and separating implication, are lifted from predicates to quantities.
This extension is conservative: Both connectives are backward compatible to their classical analogs and obey the same laws, e.g. modus ponens, adjointness, etc.

Furthermore, we present a weakest precondition calculus for quantitative reasoning about probabilistic pointer programs in QSL. This calculus is a conservative extension of both Ishtiaq's, O'Hearn's and Reynolds' separation logic for heap-manipulating programs and Kozen's / McIver and Morgan's weakest preexpectations for probabilistic programs. Our calculus preserves O'Hearn's frame rule, which enables local reasoning - a key principle of separation logic.

Finally, we briefly touch upon open questions regarding lower bounds on weakest preexpectations and intensional completeness of our calculus.

**Thom Badings** (Radboud University, NL)**Time:** 10:30**Date:** 02.12.2020**Room:** online**Title**: TBA

**Abstract**: TBA

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

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

**Dennis Groß** (Radboud University, NL)**Time:** 10:30**Date:** 09.09.2020**Room:** online**Title**: Robustness Verification for Classifier Ensembles

**Abstract**: We give a formal verification procedure that decides whether a classifier ensemble is robust against arbitrary randomized attacks. Such attacks consist of a set of deterministic attacks and a distribution over this set. The robustness-checking problem consists of assessing, given a set of classifiers and a labelled data set, whether there exists a randomized attack that induces a certain expected loss against all classifiers. We show the NP-hardness of the problem and provide an upper bound on the number of attacks that is sufficient to form an optimal randomized attack. These results provide an effective way to reason about the robustness of a classifier ensemble. We provide SMT and MILP encodings to compute optimal randomized attacks or prove that there is no attack inducing a certain expected loss. In the latter case, the classifier ensemble is provably robust. Our prototype implementation verifies multiple neural-network ensembles trained for image-classification tasks. The experimental results using the MILP encoding are promising both in terms of scalability and the general applicability of our verification procedure.

**Sven Peldszus** (University Koblenz, GER)**Time:** 10:30**Date:** 16.09.2020**Room:** online**Title**: Model-based Security and Software Quality Analysis in Variability-Rich Evolving Systems

**Abstract**: Today’s software systems tend to be used on a long-term basis, are highly interconnected, share many common parts and often process security-critical data, so that keeping up with ever-changing security precautions, attacks and mitigations is vital for preserving a system’s security. Model-based system development enables us to address security issues already in the early phases of the software design, as in UML models. The continuous changes in the security assumptions and the design of software systems — for instance, due to structural decay — have to be reflected in both the system models (e.g., UML models) and the system’s implementation (including program models). The detection of which change is necessary where has currently to be performed manually by developers. The same applies to the interaction of changes with security-related properties. In this talk, I introduce a model-based approach for developing and maintaining secure long-loving systems. The approach supports the continuous synchronization and mapping of models and code and allows developers to apply security checks on all representations utilizing the created mappings.

**Deivid Vale** (Radboud University, NL)**Time:** 10:30**Date:** 23.09.2020**Room:** online**Title**: Tuple interpretations for Higher-Order Rewriting

**Abstract**: We present a style of algebra interpretations for many-sorted and higher-order term rewriting based on interpretations to tuples; intuitively, a term is mapped to a sequence of values identifying for instance its evaluation cost, size and perhaps other values. This can give a more fine grained notion for the complexity of a term or TRS than notions such as runtime or derivational complexity.

**Dr. Robbert Krebbers** (Radboud University, NL)**Time:** 10:30**Date:** 30.09.2020**Room:** online**Title**: Program Verification using Iris

**Abstract**: Over the last 5 years, together with a large network of international collaborators, we have developed *Iris*---a program verification framework based on concurrent separation logic embedded in the Coq proof assistant. Iris is program-language agnostic (it has been applied to e.g., variants of ML, Rust, C, Scala's core calculus DOT), and can be used to verify different properties (e.g., program correctness, data abstraction, security, program refinement, complexity) of both concrete programs and type systems. In this talk I will give an overview of the key ideas behind Iris and my journey as one of the lead developers of Iris.

See https://iris-project.org for more information.

**Prof. Dr. Frits Vaandrager** (Radboud University, NL)**Time:** 10:30**Date:** 07.10.2020**Room:** online**Title**: A Myhill-Nerode Theorem for Register Automata and Symbolic Trace Languages

**Abstract**: We propose a new symbolic trace semantics for register automata (extended finite state machines) which records both the sequence of input symbols that occur during a run as well as the constraints on input parameters that are imposed by this run. Our main result is a generalization of the classical Myhill-Nerode theorem to this symbolic setting. Our generalization requires the use of three relations to capture the additional structure of register automata. Location equivalence ≡l captures that symbolic traces end in the same location, transition equivalence ≡t captures that they share the same final transition, and a partial equivalence relation ≡r captures that symbolic values v and v′ are stored in the same register after symbolic traces w and w′, respectively. A symbolic language is defined to be regular if relations ≡l, ≡t and ≡r exist that satisfy certain conditions, in particular, they all have finite index. We show that the symbolic language associated to a register automaton is regular, and we construct, for each regular symbolic language, a register automaton that accepts this language. Our result provides a foundation for grey-box learning algorithms in settings where the constraints on data parameters can be extracted from code using e.g. tools for symbolic/concolic execution or tainting. We believe that moving to a grey-box setting is essential to overcome the scalability problems of state-of-the-art black-box learning algorithms. (Joint work with Abhisek Midya.)

**Marnix Suilen** (Radboud University, NL)**Time:** 10:30**Date:** 14.10.2020**Room:** online**Title**: Robust Policy Synthesis for Uncertain POMDPs via Convex Optimization

**Abstract**: We study the problem of policy synthesis for uncertain partially observable Markov decision processes (uPOMDPs). The transition probability function of uPOMDPs is only known to belong to a so-called uncertainty set, for instance in the form of probability intervals. Such a model arises when, for example, an agent operates under information limitation due to imperfect knowledge about the accuracy of its sensors. The goal is to compute a policy for the agent that is robust against all possible probability distributions within the uncertainty set. In particular, we are interested in a policy that robustly ensures the satisfaction of temporal logic and expected reward specifications. We state the underlying optimization problem as a semi-infinite quadratically-constrained quadratic program (QCQP), which has finitely many variables and infinitely many constraints. Since QCQPs are non-convex in general and practically infeasible to solve, we resort to the so-called convex-concave procedure to convexify the QCQP. Even though convex, the resulting optimization problem still has infinitely many constraints and is NP-hard. For uncertainty sets that form convex polytopes, we provide a transformation of the problem to a convex QCQP with finitely many constraints. We demonstrate the feasibility of our approach by means of several case studies.)

**Bharat Garhewal** (Radboud University, NL)**Time:** 10:30**Date:** 21.10.2020**Room:** online**Title**: Grey-Box Learning of Register Automata

**Abstract**: Model learning (a.k.a. active automata learning) is a highly
effective technique for obtaining black-box finite state models of software
components. Thus far, generalisation to infinite state systems with in-
puts/outputs that carry data parameters has been challenging. Existing
model learning tools for infinite state systems face scalability problems
and can only be applied to restricted classes of systems (register automata
with equality/inequality). In this article, we show how we can
boost the performance of model learning techniques by extracting the
constraints on input and output parameters from a run, and making
this grey-box information available to the learner. More specifically, we
provide new implementations of the tree oracle and equivalence oracle
from RALib, which use the derived constraints. We extract the constraints
from runs of Python programs using an existing tainting library
for Python, and compare our grey-box version of RALib with the existing
black-box version on several benchmarks, including some data structures
from Python’s standard library. Our proof-of-principle implementation
results in almost two orders of magnitude improvement in terms of numbers
of inputs sent to the software system. Our approach, which can be
generalised to richer model classes, also enables RALib to learn models
that are out of reach of black-box techniques, such as combination locks.

**Jules Jacobs** (Radboud University, NL)**Time:** 10:30**Date:** 28.10.2020**Room:** online**Title**: Paradoxes of probabilistic programming, and how to condition on events of measure zero with infinitesimal probabilities

**Abstract**: Probabilistic programming languages allow programmers to write down conditional probability distributions that represent statistical and machine learning models as programs that use observe statements. These programs are run by accumulating likelihood at each observe statement, and using the likelihood to steer random choices and weigh results with inference algorithms such as importance sampling or MCMC. We argue that naive likelihood accumulation does not give desirable semantics and leads to paradoxes when an observe statement is used to condition on a measure-zero event, particularly when the observe statement is executed conditionally on random data. We show that the paradoxes disappear if we explicitly model measure-zero events as a limit of positive measure events, and that we can execute these type of probabilistic programs by accumulating infinitesimal probabilities rather than probability densities. Our extension improves probabilistic programming languages as an executable notation for probability distributions by making it more well-behaved and more expressive, by allowing the programmer to be explicit about which limit is intended when conditioning on an event of measure zero.

**Dr. Cynthia Kop** (Radboud University, NL)**Time:** 10:30**Date:** 04.11.2020**Room:** online**Title**: Cons-free term rewriting

**Abstract**: Computational complexity is the study of resources (typically time and space) required to algorithmically solve a problem. Rather than analysing programs directly, the area of implicit complexity seeks to encode complexity queries into calculi or logics. One such approach is to use cons-free programming languages. By varying data order, this approach allows you to obtain a characterisation of a hierarchy of complexity classes, both in time and in space. In this talk, I will present the related approach of cons-free term rewriting systems. The additional of non-determinism turns out to have quite unexpected results.

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.