Logo: to the web site of Uppsala University

We investigate the termination problem of regular transition systems, i.e., of transition systems whose transition relations can be represented by finite-state automata. Leveraging this automata-theoretical perspective, we propose a new, efficient approach to termination analysis. Our method encodes termination arguments, called statements, as words in an auxiliary language, enabling the verification of whether configurations satisfy those termination arguments via an interpretation automaton. The choice of a fixed interpretation automaton enables the synthesis of new automata dedicated to searching for statements and verifying properties within any given regular transition system. The central contribution of this work is the construction of a specialized finite-state automaton that recognizes statements ensuring the system's termination according to predefined conditions. Depending on the fragment of regular transitions considered, we define two sets of sufficient conditions for termination and provide an automata-based method to verify them within a given regular transition system.

In deductive verification and software model checking, dealing with certain specification language constructs can be problematic when the back-end solver is not sufficiently powerful or lacks the required theories. One way to deal with this is to transform, for verification purposes, the program to an equivalent one not using the problematic constructs, and to reason about this equivalent program instead. In this article, we propose program instrumentation as a unifying verification paradigm that subsumes various existing ad-hoc approaches, has a clear formal correctness criterion, can be applied automatically, and can transfer back witnesses and counterexamples. We illustrate our approach on the automated verification of programs that involve quantification and aggregation operations over arrays, such as the maximum value or sum of the elements in a given segment of the array, which are known to be difficult to reason about automatically. We implement our approach in the MonoCera tool, which is tailored to the verification of programs with aggregation, and evaluate it on example programs, including SV-COMP programs.

Parametrized automata (PA) are an extension of two existing kinds of automata, symbolic automata and variable automata. In PA, transitions are labeled with formulas that may contain variables. PA are a powerful tool for modeling systems over infinite alphabets, but complementation of PA has been proven to be challenging: not every PA has a complement, and complementation in general may be non-computable. This paper presents a new notion of normal form for PA, called complementable normal form (CFPA). CFPA is sufficiently expressive to completely characterize the class of PA that can be complemented. We show that all Boolean operations (including complementation) can be computed efficiently on CFPA, and key problems such as the universality and non-emptiness problem are decidable for CFPA. Based on CFPA, we propose a new method for complementing PA.

Verification of programs operating on heap-allocated data structures, for instance lists or trees, poses significant challenges due to the potentially unbounded size of such data structures. We present time-indexed heap invariants, a novel invariant-based heap encoding leveraging uninterpreted predicates and prophecy variables to reduce verification of heap-manipulating programs to verification of programs over integers only. Our encoding of heap is general and agnostic to specific data structures. To the best of our knowledge, our approach is the first heap invariant-based method that achieves both soundness and completeness. We provide formal proofs establishing the correctness of our encodings. Through an experimental evaluation, we demonstrate that time-indexed heap invariants significantly extend the capability of existing verification tools, allowing automatic verification of programs with heap that were previously out of reach for state-of-the-art tools.

Memory safety is a fundamental correctness property of software. For programs that manipulate linked, heap-allocated data structures, ensuring memory safety requires analyzing their possible shapes. Despite significant advances in shape analysis, existing techniques rely on hand-crafted domains tailored to specific data structures, making them difficult to generalize and extend. This paper presents a novel approach that reduces memory-safety proofs to the verification of heap-less imperative programs, enabling the use of off-the-shelf software verification tools. We achieve this reduction through two complementary program instrumentation techniques: space invariants, which enable symbolic reasoning about unbounded heaps, and flow abstraction, which encodes global heap properties as local flow equations. The approach effectively verifies memory safety across a broad range of programs, including concurrent lists and trees that lie beyond the reach of existing shape analysis tools.

This paper introduces a compilation scheme for programs written in the Mimosa programming language, which builds upon the MIMOS model of computation. Mimosa describes embedded systems software as a collection of time-triggered processes which communicate through FIFO queues. We formally describe an adaptation of the Lustre compilation scheme to the semantics of Mimosa and show how the coordination layer can be mapped to real-time operating system primitives.

We report on our experience deploying a CubeSat to study fault and error distributions against different fault tolerance schemes when using Common Off-The-Shelf (COTS) hardware in Low-Earth Orbit (LEO). Space radiation commonly causes faults in COTS hardware, such as bit flips in memory, which can lead to errors in a program's execution. Fault tolerance techniques can prevent faults from turning into errors. Accurately quantifying the fault and error distributions is vital for choosing an appropriate fault tolerance scheme. We equip the CubeSat with heterogeneous hardware combining a regular System on a Chip (SoC) with programmable logic resources. Based on in-orbit experiments and post-processing of logs, we check the validity of two fault models. We find the single fault model to be valid, encouraging the use of techniques such as triple modular redundancy. We also demonstrate, however, that the single-bit error fault model is not valid, which means that common techniques such as Hamming (7,4) codes should not be used. We observe that most errors are short-lived, allowing simple re-executions to correct them. Contrary to intuition, we also conclude that floating-point encodings are more appropriate to build fault-tolerance schemes in our setting, due to faults being easier to detect than in their integer counterparts. Our insights confirm existing findings in the literature while also providing new ones, while providing a foundation to conceive fault tolerance schemes for COTS hardware deployments in space.

A common approach in software verification is to encode a program as a set of Constrained Horn Clauses (CHCs), which are then processed and solved automatically by a CHC solver. To streamline this verification approach for the case of programs operating on mutable linked data-structures, we have in earlier work proposed a theory of heaps, defined within the SMT-LIB framework, which enables us to represent programs as CHCs with minimal loss of structural information. By preserving high-level program information in the encoding, the theory of heaps enables CHC solvers to apply various internal techniques for handling program heap; among others, to encode the heap further using the theory of arrays, to apply shape analysis, or to translate to a heap-less program with the help of invariants. This paper explores the third option, developing transformation rules that rewrite a set of CHCs into an equisatisfiable set of CHCs with additional predicates representing heap invariants. The proposed method generalises the notion of space invariants, which were previously introduced for verifying Java programs, by lifting the entire transformation process to the CHC level. The paper defines the transformation rules, provides detailed correctness proofs, and discusses the strengths and limitations of the approach. We also outline possible extensions of the method.

We present HornStr, the first solver for invariant synthesis for Regular Model Checking (RMC) with the specification provided in the SMT-LIB 2.6 theory of strings. It is well-known that invariant synthesis for RMC subsumes various important verification problems, including safety verification for parameterized systems. To achieve a simple and standardized file format, we treat the invariant synthesis problem as a problem of solving Constrained Horn Clauses (CHCs) over strings. Two strategies for synthesizing invariants in terms of regular constraints are supported: (1) L* automata learning, and (2) SAT-based automata learning. HornStr implements these strategies with the help of existing SMT solvers for strings, which are interfaced through SMT-LIB. HornStr provides an easy-to-use interface for string solver developers to apply their techniques to verification. At the same time, it allows verification researchers to painlessly tap into the wealth of modern string solving techniques. To assess the effectiveness of HornStr, we conducted a comprehensive evaluation using benchmarks derived from applications including parameterized verification and string rewriting tasks. Our experiments highlight HornStr's capacity to effectively handle these benchmarks, e.g., as the first solver to verify the challenging MU puzzle automatically. Finally, HornStr can be used to automatically generate a new class of interesting SMT-LIB 2.6 string constraint benchmarks, which might in the future be used in the SMT-COMP strings track. In particular, our experiments on the above invariant synthesis benchmarks produce more than 30000 new QF_S constraints. We also detail the performance of various integrated string solvers, providing insights into their effectiveness on our new benchmarks.