In this work, we present an industrial case study of deadlock avoidance in the context of automated warehouse logistics. In particular, we consider systems of Automated Guided Vehicles (AGVs) in which semi-autonomous robots move inside a facility along a predefined set of paths. The paper introduces a novel formalization of AGV systems that models the physical setup of the AGV system more accurately compared to previous approaches. In particular, our modeling approach captures movement restrictions due to physical proximity of vehicles regardless of the logical connectivity of the guide path network. The paper provides and compares three different encodings of such models as transition systems, which enable symbolic analysis of the system via Binary Decision Diagrams (BDDs). Based on these encodings we perform deadlock avoidance for warehouse layouts of both synthetic and real-world origin.
The Syndrome Decoding Problem (SDP) for a binary linear code consists in finding a particular solution to an underdetermined linear system defined over the finite field of two elements, such that the Hamming weight of this solution is smaller than a given bound. In this paper, we explore several satisfiability-based models for solving this problem relying on XNF and classical CNF representations. We compare these approaches to assess their efficiency in solving SDP. Furthermore, we also introduce a Maximum Satisfiability (MaxSAT) model of the Low-Weight Codeword Problem (LWCP), which consists in finding a word with minimal Hamming weight in a given code. In particular, we introduce three MAX-SAT models for LWCP: an XNF model, which reuses the XOR constraints from the SDP formulations, and two CNF models, which are also based on the CNF formulations from SDP. For all three models, we add soft clauses to minimize the Hamming weight. Finally, we assess the models using state-of-the-art MaxSAT solvers, which apply different solving paradigms to compute optimal codeword weights.
Program verification provides stronger guarantees of correctness than standard testing. The verification process takes a program as input and derives a mathematical formula. Proving that a program is correct then reduces to establishing that this derived formula is unsatisfiable. Traditionally, automated reasoning tools can be used to determine unsatisfiability automatically. Furthermore, modern solvers can also produce a proof of unsatisfiability. However, these techniques typically rely on the proof and the underlying code being publicly available, which may not be desirable for certain applications. This work shows how to address this problem. Our team initially developed a protocol for validating the unsatisfiability of Boolean formulas in privacy-preserving settings. Building on these initial results, we devised ZKSMT, a virtual machine for validating unsatisfiability results produced by SMT solvers in zero-knowledge settings. In this paper we describe the theoretical foundations of such virtual machines and demonstrate how they can be applied to the theories of uninterpreted functions and linear integer arithmetic, two of the most widely used theories in verification. We conclude by outlining how the full formal verification workflow can be adapted to operate in privacy-preserving settings.
To mitigate the state explosion problem in model checking, abstraction techniques provide sound but typically incomplete approximations of a system’s behaviour. While complete abstractions eliminate false alarms, they are often impractical—or even uncomputable—due to their high computational cost. We introduce semi-completeness, a relaxed notion of completeness that retains sufficient precision to capture a system’s behaviour over relevant regions of the domain. Building on this, we develop abstraction refinement algorithms that compute semi-complete abstractions without incurring the cost of full completeness. Furthermore, we present an algorithm that interleaves abstraction refinement with fixed-point computations—specifically reachability analysis. This achieves semi-completeness on-the-fly, without requiring prior knowledge of the region of interest, such as the reachable states. We demonstrate the effectiveness of our approach on fragments of the μ -calculus, showing that our abstractions preserve the validity of formulae over all reachable states.
SEAndroid is deployed on almost all modern Android devices to enforce mandatory access control. The Android Open Source Project regularly publishes a predefined SEAndroid policy that each vendor customises for its devices. These customisations and policy updates may cause security regressions: even small misconfigurations may introduce new information flows leading to exploitable vulnerabilities. We propose a differential verification framework that determines whether security-relevant changes between two SEAndroid configurations affect information-flow properties as intended. Our verification framework is based on the novel comparative modal logic CML interpreted over pairs of Kripke structures. We formalise SEAndroid policies within this logic and define a suitable model-checking algorithm for differential reasoning. We implement our framework in the tool Mordente, and evaluate it on real-world SEAndroid policies.
