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

Thom Badings (Radboud University, NL)
Time: 10:30
Date: 02.12.2020
Room: online
Title: Filter-based abstractions for planning in partially observable dynamical control systems

Abstract: We study planning problems for dynamical control systems with limited sensing and imperfect actuation. Due to the inherent state uncertainty, such systems are only partially observable. Planning for these systems generally involves formulating an optimization problem in the belief space, which is intractable to solve exactly in the continuous domain. One solution is to formulate the problem as a discrete-state partially observable Markov decision process (POMDP), but this still renders the problem computationally expensive. In this work, we propose an alternative filter-based stochastic abstraction for partially observable dynamical control systems. Our abstraction is based on state estimation using Kalman filtering. The resulting model is formulated as an uncertain Markov decision process (uMDP), for which mature tools are available to provide guarantees on the systemís behavior. In this talk, we demonstrate how the proposed abstraction can be used to compute the probability to satisfy reachability specifications for partially observable systems with measurement and process noise. Moreover, we discuss various extensions to the proposed abstraction, including the use of a so-called local information controller as a heuristic to eliminate the history-dependency of optimal policies that may arise in some cases.

Natalia Sidorova (TUE, NL)
Time: 10:30
Date: 13.01.2021
Room: online
Title: TBA

Abstract: TBA

Kousar Aslam (TUE, NL)
Time: 10:30
Date: 20.01.2021
Room: online
Title: TBA

Abstract: TBA

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

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

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.

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.