Validation and Verification (VALVE)

In VALVE, we are interested in checking that programs (and designs) do what we meant them to do. We are interested in testing programs, understanding them, and in proving that they are correct. Our work includes studying models that enable to better represent behaviour of programs, creating techniques for the analysis of programs, and working on new designs of programs that are built with validation in mind.

Learn more about VALVE on our research pages.

Suggested topics

Correct-by-design construction of systems with learning components

Supervisor: Rayna Dimitrova

The goal of this project is to develop synthesis algorithms for automatically constructing autonomous systems control software that ensures that the risk of unsafe behaviors is within acceptable bounds. The developed synthesis algorithms will account for the uncertainty propagating through the pipeline of components in a system, from the sensors to the control layer. To this end, formal interfaces between these components have to be established, in order to translate system-level safety requirements into constraints on the uncertainty associated with individual components.


Controlling epistemic uncertainty

Supervisor: Rayna Dimitrova

Epistemic uncertainty is uncertainty that stems from the lack of knowledge about the system or the environment in which it operates. This type of uncertainty can be reduced, for example by collecting more data or providing more precise sensors. The goal of this research is to investigate the trade-off between reducing uncertainty on one hand, and cost-effectiveness/performance on the other, and based on that, to develop synthesis algorithms that are guided by the systems safety and task specifications in order to efficiently control the mitigation of epistemic uncertainty.


Dynamic Reactive Modules

Supervisor: Nir Peterman

This is an approach for modeling transition systems that support allocation of new processing power (and its deallocation) based on variable sharing (rather than message passing). I find this very exciting as this could be related to ad-hoc networks and such things and hasn't been considered in the past.

See the paper introducing them.


p-Automata and related games

Supervisor: Nir Peterman

These are new automata motivated by probabilistic CTL and alternating tree automata that accept Markov chains. Their study involve issues about automata (conversion between different transition modes of automata (deterministic, nondeterministic, alternating)), algorithmic questions about automata, the introduction of new games (obligation games) and algorithmic questions about such games.

You can have a look on the paper introducing them or the paper on obligation games.


Synthesis of controllers from temporal specifications

Supervisor: Nir Peterman

Synthesis (in my language) is the automatic conversion of a specification in linear temporal logic to an input-enabled program all of whose executions satisfy the specification. 

This is a question that intrigued researchers in verification for many years, getting much attention, but only recently getting actual practical progress. 
The techniques involved in doing this include the study of transition systems, two player games, and construction of strategies. This is also related to automata and temporal logic. 

The approach that I have been advocating calls for restricting the type of specifications to a "reasonable" subset that can be handled in practice.

I have recently considered how to apply this to certain abstract ways of representing the world.

This is also related to questions about games with partial information, their solutions, and strategies controlling them (See survey, not mine).

Test-case generation for safety analysis of automated vehicle functions

Supervisor: Mohammed Mousavi

The introduction of automated and autonomous vehicle functions pose new challenges before traditional safety case analysis and ultimately software and system testing techniques. The complexity of such functions call for a structured method to translate safety goals and driving situations to concrete test cases. The goal of this project is to define and implement a technique that translates structured English safety goals and driving situations into a test-suite and compile the test outcomes into a safety case.


Working with Specifications for Reactive Synthesis

Supervisor: Jan Oliver Ringert

Reactive systems are software systems in an ongoing interaction with the environment as found in the robotics and automotive domain. Reactive synthesis presents the appealing idea of the automated construction of software systems from a reactive specification.

With reactive synthesis the task of software engineers shifts from writing code to writing specifications. Currently, there are still many open questions of how to best work with specifications. This project will address some existing challenges. As an example, one focus will be on techniques for testing and analysing (parts of) specifications against expected or previously observed behaviors. As another example, we will investigate meaningful means for the decomposition and reuse of specifications. The outcome will be integrated and evaluated within a toolset for reactive synthesis with focus on autonomous robotic systems.