Number representation
The mCRL2 toolset uses abstract data types to represent numbers. A number is either @c1 or it is @cDub(b,n) where b is boolean and n a number. If the boolean is true this represents 2n+1 and otherwise it represents 2n. Previous experiments have shown that it is very beneficial to replace these booleans by 64 bits machine numbers, which allows a substantial performance gain without loosing that mCRL2 allows arbitrarily large numbers.
The question is to describe a new number system together with all the operations that are currently available on numbers. The enumeration of numbers satisfying a certain condition is an important functionality of the toolset and should also be solved. A typical example is to find all positive numbers n satisfying n<17. A prototype implementation would be valued allowing to assess the obtainable performance gain.

Quantum protocols
In the recent paper Ebrahim Ardeshir-Larijani, Simon Gay and Rajagopal Nagarajan. Verification of Concurrent Quantum Protocols by Equivalence Checking, published at TACAS2014, quantum protocols are described by simple process algebra's. Quantum protocols can be characterised by a simple abstract data type: there are some operations that are allowed and there are certain data elements that can be communicated between different processes.
The goal of this assignment is to model quantum protocols in mCRL2, with as simple purpose to understand what the essence of quantum computing is. We have been contacted by Ebrahim Ardeshir-Larijani who wanted to start to experiment with the modelling of these protocols in mCRL2.

For more information contact Jan Friso Groote, email: J.F.Groote@tue.nl

Bas Luttik

Pushdown automata up to behavioural equivalence
A pushdown automaton is a finite automaton that may use an unbounded stack as auxiliary memory. The semantics of pushdown automata is usually defined directly in terms of the languages they accept. But there is also an approach in which one first associates an intermediate transition system with a pushdown automaton. The advantage of this approach is that one can consider pushdown automata modulo at a more refined level, modulo any of the many behavioural equivalences known from the literature on concurrency theory. It turns out that the familiar equivalences (e.g., termination on empty stack is equivalent to termination on final state, pushdown automata are equivalent to context-free grammars) fail modulo the finer equivalences of the spectrum.
Paul van Tilburg has made a partial inventory of the state-of-affairs for pushdown automata modulo behavioural equivalences finer than language equivalence, and reports about it in his PhD thesis, but the inventory is somewhat scattered and incomplete. The assignment would consists of first systematically determining what is known and what is not yet known about pushdown automata modulo finer behavioural equivalences, and then perhaps solve one or two open issues in the area.

Adding sequential composition to the "Axiomatisability of Priority II" In an article by Aceto, Chen, Ingolfsdottir, Luttik and van de Pol it was proved that order-insensitive bisimilarity is not finitely axiomatisable in the setting of minimal process algebra. It is, moreover, conjectured that the result generalises to basic process algebra, which includes termination and sequential composition. The assignment is to prove or refute the conjecture.

For more information on a topic in process algebra contact Bas Luttik, email: S.P.Luttik@tue.nl

Julien Schmaltz
The research of Julien Schmaltz is concerned with the applications of formal methods to systems of practical interests. For this a broad spectrum of techniques is being used, including, model checking, SAT/SMT, interactive theorem proving, model-based testing. These techniques are applied to a wide range of software and hardware systems. In particular, the focus is on on-chip networks for more than a decade now. Still, this topic is fascinating and largely open. For the Seminar 2015, there are the following conceivable topics. following topics.

Message ordering models Cooperation with Ruud Koolen, Sanne Wouda, and Freek Verbeek.
One open issue in the analysis of networks is a formal technique to find violation of producer-consumer relations. The idea is that a producer is sending data to a node. A consumer is then sending read requests to this node. The property we want to ensure is that data are received before they are produced. There is today no theoretical foundations for checking such properties.
In this seminar assignment, you will study the feasibility of one possible solution. Recently, Alglave proposed a theory of weak memory models based on relations defining orderings between read and write events to memory. Alglave developed a tool automatically generating test cases stimulating possible violations of the ordering relations. Your task will be to investigate the possibility of extending this theory to "send" and "receive" events. This assignment involves both theoretical developments and practical implementation. The goals of this assignment are among others to adapt the theory and generate a few test cases for small networks.

Theory of Productive Networks in Isabelle/HOL Cooperation with Ruud Koolen, Sanne Wouda, and Freek Verbeek.
Another open issue is a science of networking. Networks are mostly built following ad hoc methodologies and most of the times a "trial and error" one. One of my long term research goal is to change this practice and provide network designers with a foundational theory of networking. The recent result of our theory is the notion of "productivity". A network is productive if and only if all pending messages eventually reach their destination. The theory applies to one network.
A next step is to lift up the theory to networks of networks. We modelled networks by a function in the first order logic of the ACL2 theorem prover. For this next step, we need higher order logics to define functions over functions and reason about them. The task of this assignment will be to investigate the formalisation of our theory in the higher order logic of the theorem prover Isabelle/HOL. The main attractive feature of Isabelle/HOL is a "locale" which allows users to design abstract modules that can be later combined.
In your task, you will study the use of locales to model our theory of networking in a compositional way. The goal of this assignment is to formalise a restricted version of our theory in Isabelle/HOL.

For more information contact Julien Schmaltz, email: J.Schmaltz@tue.nl

Wieger Wesselink

Analyzing pseudocode descriptions of bisimulation algorithms
In many scientific publications, algorithms are presented using pseudocode. There is no standard for pseudocode syntax, and as a result there is a lot of variation in the style of pseudocode that different authors use. Also the quality of the descriptions varies a lot. Common problems are that the description is incomplete, and it does not have the right abstraction level. In practice this makes it hard to implement these algorithms.
The goal of this assignment is to study a number of papers about bisimulation algorithms (but other classes of algorithms are also possible), and to make an assessment of their pseudocode descriptions. For this assessment a number of criteria can be used like completeness, level of detail, level of abstraction, readability etc. This should result in a number of improvements to the pseudocode that makes it possible to implement the algorithms, without needing to extensively study the papers to find all missing pieces of information. As part of this work it may be useful to make an overview of the primitive data types and operations that are commonly used.

Grammar based random testing
The language used in the mCRL2 tool set is very rich. This makes it hard to manually achieve a sufficient coverage rate for testing. To overcome this problem, the mCRL2 tool set contains a framework for random testing. Random instances of mCRL2 data structures are generated, and they are used to verify the correct behaviour of the tools. For example a random boolean equation system can be generated, and its solution can be computed using different algorithms. Or a random process can be generated, and one can verify that the result after a certain transformation on this process is bisimulation equivalent to the original.
In the current approach the random instances are generated in a bottom up manner. This approach has some drawbacks, so the goal is to replace it by a top down approach that takes the grammar of the language as input. An important issue is that not all instances are valid. For example variables need to be bound correctly, and the monotonicity of a boolean equation system needs to be guaranteed, meaning that boolean variables may only appear in the context of an even number of negations. Attribute grammars can be used to model such constraints. The goal of this assignment is to study how certain constraints can be expressed using attribute grammars, and how this can be integrated into existing grammar based random generation algorithms.

For more information contact Wieger Wesselink, email: J.W.Wesselink@tue.nl

Tim Willemse

A Proof System for Consistent Consequence for PBESs
Parameterised Boolean equation systems (PBESs), and their propositional fragment called Boolean equation systems (BESs), can be used to encode model checking problems, behavioural equivalence checking problems and other decision problems. The concept of a consistent consequence for PBESs was introduced to simplify the laborious proofs of correctness required to show soundness of solution preserving/approximating transformations in this setting.
Consistent consequence focusses on relating the equations that occur in PBESs, rather than their solutions. For the closed, simple and recursive fragment of equation systems it was shown that a consistent consequence coincides with direct simulation for parity games. Moreover, a sound and complete proof system for consistent consequence for the setting of BESs was given. It remains open whether a similar proof system can be given for PBESs.
The goal of this assignment is to define such a proof system. Having such a proof system for PBESs would allow for giving syntax-directed proofs (instead of semantics-directed proofs) of PBES transformations.

Robustness in Asynchronous Model-Based Testing Together with Neda Noroozi (NSpyre)
Model-Based Testing (MBT) is an automated solution for testing. In MBT, an MBT tool uses models for automatically constructing test cases, executing these on the system-under-test (SUT) and for judging whether the tests pass or fail. Popular MBT theories such as ioco assume that communication between the test engine and the SUT is synchronous. In the presence of asynchronous communication, the test verdict delivered by MBT tools operating under such assumptions become unreliable.
For a certain class of test models (so called robust models) this is not the case: the verdict they provide remains reliable. However, the complexity of deciding whether a model is robust is unknown and in case a model is not robust, but has a submodel that is robust, it is currently unknown whether this submodel can be extracted effectively. The goal of this assignment is to address these questions.

Besides these assignments, there are many other interesting research topics in parity games and/or PBESs.

For more information contact Tim Willemse, email: T.A.C.Willemse@tue.nl

Hans Zantema

Structure of infinite data
An infinite data object like an infinite sequence of booleans may have a regular/periodic shape, but often has not, even if the object is defined by an extremely simple recursive equation. We want to study properties of such objects, for instance by ways to visualize them (see e.g. turtle.pdf) or by techniques to prove that different specifications define the same object, see [1]. In the latter equational reasoning and term rewriting plays a crucial role.
[1] H. Zantema and J. Endrullis, Proving Equality of Streams Automatically, Proceedings of the 22st International Conference on Rewriting Techniques and Applications (RTA), 2011.

Applying SAT/SMT
Current solvers are remarkably strong in solving SAT/SMT problems: decide whether variables can be assigned in such a way that a given formula yields true. This approach has a wide range of applications. Further exploring possible applications is always possible as a seminar topic.

For more information contact Hans Zantema, Metaforum 7.067, email: H.Zantema@tue.nl

Herman Geuvers
For more information on a topic around proving with computer assistance contact Herman Geuvers, email: herman@cs.ru.nl