Browse Proceedings

This paper focuses on the work of the Autonomy and Verification Network (). In particular it will look at the use of model-checking to verify the choices made by a cognitive agent in control of decision ...

Event-B offers a rigorous state-based framework for designing critical systems. Models describe state changes (transitions), and invariant preservation is ensured by inductive proofs over execution traces. In a correct model, such changes ...

Verifying that autonomous space robotic software behaves correctly is crucial, particularly since such software is often mission-critical, that is, a software failure can lead to mission failure. In this paper, we describe the process that we used ...

Hash maps are a common and important data structure in efficient algorithm implementations. Despite their wide-spread use, real-world implementations are not regularly verified.

In this paper, we present the first case study of the IdentityHashMap ...

Software verification allows one to examine the reliability of software. Thereby, analyses exchange information to become more effective, more efficient, or to eliminate false results and increase trust in the analysis result. One type of ...

The use of function contracts to specify the behavior of functions often remains limited to the scope of a single function call. Relational properties link several function calls together within a single specification. They can express more ...

The development of cyber-physical systems has become one of the biggest challenges in the field of model-based system engineering. The difficulty stems from the complex nature of cyber-physical systems which have deeply intertwined physical ...

A lot of techniques try to improve the performance of explicit state model checking. Some techniques, like partial order reduction, are hard to apply effectively to high-level models, while others, like symmetry reduction, rarely apply to more ...$$$$

We present the first review of methods to overapproximate the set of reachable states of linear time-invariant systems subject to uncertain initial states and input signals for short time horizons. These methods are fundamental to state-of-the-art ...

For timed automata, the question of whether the number of clocks can be decreased without violating the semantics is known to be undecidable. It is, however, possible to obtain a number of clocks that is optimal, in a well-defined sense, for a ...

Business Process Model and Notation (BPMN) is a standard business process modelling language that allows users to describe a set of structured tasks, which results in a service or product. Before running a BPMN process, the user often has no clear ...

Probabilistic hyperproperties describe system properties involving probability measures over multiple runs and have numerous applications in information-flow security. However, the poor scalability of existing model checking algorithms for ...

Explaining and verifying the behavior of recurrent neural networks (RNNs) is an important step towards achieving confidence in machine learning. The extraction of finite state models, like deterministic automata, has been shown to be a promising ...

Modern computer networks are becoming increasingly complex and for dependability reasons require frequent configuration changes. It is essential that forwarding policies are preserved not only before and after the configuration update but also at ...

Password managers (PMs) are important tools that enable the use of stronger passwords, freeing users from the cognitive burden of remembering them. Despite this, there are still many users who do not fully trust PMs. In this paper, we focus on a ...

From the very outset of the digital era, the protection of personal data against unauthorized usage and distribution has been one of the most significant challenges in distributed services. For this reason, new regulations such as the European ...

This paper presents a new data flow coverage criterion for a deeper analysis of possible refinements to the constraints on paths unfolding of software program’s behavior. Such refinements represent a feasible chain of usages of the same variable ...

Static analyses based on typestates are important in certifying correctness of code contracts. Such analyses rely on Deterministic Finite Automata (DFAs) to specify properties of an object. We target the analysis of contracts in low-latency ...

Password Managers (PMs) help users manage their passwords safely but many users do not trust them. To mitigate users’ doubts, formal verification can be used. Formal verification can guarantee the absence of errors and make PMs more reliable. ...