Recent advancements in the fabrication of Resistive Random Access Memory (ReRAM) devices have led to the development of large-scale crossbar structures. In-memory computing architectures relying on ReRAM crossbars aim to mitigate the processor-memory ...

Verifying properties and interpreting the behaviour of deep neural networks (DNN) is an important task given their ubiquitous use in applications, including safety-critical ones, and their black-box nature. We propose an automata-theoretic ...

Procedure contracts are a well-known approach for specifying programs in a modular way. We investigate a new contract theory for collective procedures in parallel message-passing programs. As in the sequential setting, one can verify that a ...

Well-structured transition systems (WSTS) are an abstract family of systems that encompasses a vast landscape of infinite-state systems. By requiring a well-quasi-ordering (wqo) on the set of states, a WSTS enables generic algorithms for classic ...

Based on the logic of non-deterministic Abstract State Machines (ASMs) we define a modal extension $\mathcal{M}{\mathcal{L}}_{\text{ASM}}$  by first introducing multi-step predicates and then adding quantification over the number of steps. We show that liveness conditions such as ...$\mathcal{}{\mathcal{}}_{}$

Data oversharing is a critical issue in today's technologically driven society. Numerous entities, i.e., corporations, governments, criminal groups, are collecting individuals' data. One potential cause is that current systems, such as verification ...

We introduce meta-configuration tracking: a simple, universal, sound, and complete proof method for producing machine-verifiable proofs of linearizability. Universality means that our method works for any object type; soundness means that an algorithm ...

We consider two natural variants of the problem of minimum spanning tree (MST) of a graph in the parallel setting: MST verification (verifying if a given tree is an MST) and the sensitivity analysis of an MST (finding the lowest cost replacement edge for ...

Designing new input devices and associated interaction techniques is a key contribution in order to increase the bandwidth between users and interactive applications. In the field of Human-Computer Interaction, research and development services in ...

A stochastic network simulation is verified when its distribution of outputs is aligned with the ground truth, while tolerating deviations due to variability in real-world measurements and the randomness of a stochastic simulation. However, comparing ...

We optimise the verification of the SQIsign signature scheme. By using field extensions in the signing procedure, we are able to significantly increase the amount of available rational 2-power torsion in verification, which achieves a significant ...

The evolving landscape of manipulated media, including the threat of deepfakes, has made information verification a daunting challenge for journalists. Technologists have developed tools to detect deepfakes, but these tools can sometimes yield ...

Recently developed pretrained models can encode rich world knowledge expressed in multiple modalities, such as text and images. However, the outputs of these models cannot be integrated into algorithms to solve sequential decision-making tasks. We ...

Concurrent objects form the foundation of many applications that exploit multicore architectures and their importance has lead to informal correctness arguments, as well as formal proof systems. Correctness arguments (as found in the distributed ...

This paper describes ongoing work on developing a formal specification of a database backend. We present the formalisation of the expected behaviour of a basic transactional system that calls into a simple store API, and instantiate in two semantic ...

Snapshot Isolation (SI) is a popular isolation level, supported by many databases and is widely used by applications. Understanding and checking SI is essential. However, today's SI definitions can be obscure for non-experts to understand, or inefficient ...

Verification of hardware design code is crucial for the quality assurance of hardware products. Being an indispensable part of verification, localizing bugs in the hardware design code is significant for hardware development but is often regarded as a ...

The need to assess and validate the trustworthiness of AI (robustness, transparency, safety, security, etc.,) has been the subject of considerable academic work for some time now. A natural evolution of such research efforts is to have a tangible impact ...

Opacity is a powerful confidentiality property that holds if a system cannot leak secret information through observable behavior. In recent years, time has become an increasingly popular attack vector. The notion of opacity has therefore been extended to ...

Software scientists and practitioners have criticized Model-driven engineering (MDE) for lacking effective tooling. Although progress has been made, most MDE analysis tools rely on complex, heavyweight mathematical techniques that are not based on UML. ...