Abstract Programs that manipulate tree-shaped data structures often require complex, specialized proofs that are difficult to generalize and automate. This paper introduces a unified, foundational approach to verifying such programs. Central to our approach is the knitted-tree encoding , modeling each program execution as a tree structure capturing input, output, and intermediate states. Leveraging the compositional nature of knitted-trees, we encode these structures as constrained Horn clauses (CHC s), reducing verification to CHC satisfiability. To illustrate our approach, we focus on memory safety and show how it naturally leads to simple, modular invariants.

We present a novel automata-based approach to address linear temporal logic modulo theory (LTLfMT) as a specification language for data words. LTLfMT extends LTLf by replacing atomic propositions with quantifier-free multi-sorted first-order formulas interpreted over arbitrary theories. While standard LTLf is reduced to finite automata, we reduce LTLfMT to symbolic data-word automata (SDWAs), whose transitions are guarded by constraints from underlying theories. Both the satisfiability of LTLfMT and the emptiness of SDWAs are undecidable, but the latter can be reduced to a system of constrained Horn clauses, which are supported by efficient solvers and ongoing research efforts. We discuss multiple applications of our approach beyond satisfiability, including model checking and runtime monitoring. Finally, a set of empirical experiments shows that our approach to satisfiability works at least as well as a previous custom solution.

Solving reachability games is a fundamental problem for the analysis, verification, and synthesis of reactive systems. We consider logical reachability games modulo theories (in short, GMTs), i.e., infinite-state games whose rules are defined by logical formulas over a multi-sorted first-order theory. Our games have an asymmetric constraint: the safety player has at most k possible moves from each game configuration, whereas the reachability player has no such limitation. Even though determining the winner of such a GMT is undecidable, it can be reduced to the well-studied problem of checking the satisfiability of a system of constrained Horn clauses (CHCs), for which many off-the-shelf solvers have been developed. Winning strategies for GMTs can also be computed by resorting to suitable CHC queries. We demonstrate that GMTs can model various relevant real-world games, and that our approach can effectively solve several problems from different domains, using Z3 as the backend CHC solver.

Abstract Reasoning about data structures requires powerful logics supporting the combination of structural and data properties. We define a new logic called Mso-D(Monadic Second-Order logic with Data) as an extension of standard Mso on trees with predicates of the desired data logic. We also define a new class of symbolic data tree automata (Sdtas) to deal with data trees using a simple machine. Mso-D and Sdtas are both Turing-powerful, and their high expressiveness is necessary to deal with interesting data structures. We cope with undecidability by encoding Sdta executions as a system of CHCs (Constrained Horn Clauses), and solving the resulting system using off-the-shelf solvers. We also identify a fragment of Mso-D whose satisfiability can be effectively reduced to the emptiness problem for Sdtas. This fragment is very expressive since it allows us to characterize a variety of data trees from the literature, solving certain infinite-state games, etc. We implement this reduction in a prototype tool that combines an Mso decision procedure over trees (Mona) with a CHC engine (Z3), and use this tool to conduct several experiments, demonstrating the effectiveness of our approach across different problem domains.

Dynamic program analysis tools such as Eraser, TaintCheck, or ThreadSanitizer abstract the contents of individual memory locations and store the abstraction results in a separate data structure called shadow memory. They then use this meta-information to efficiently implement the actual analyses. In this paper, we describe the implementation of an efficient symbolic shadow memory extension for the CBMC bounded model checker that can be accessed through an API, and sketch its use in the design of a new data race analyzer that is implemented by a code-to-code translation.

Bounded verification techniques such as bounded model checking (BMC) have successfully been used for many practical program analysis problems, but concurrency still poses a challenge. Here, we describe a new approach to BMC of sequentially consistent imperative programs that use POSIX threads. We first translate the multi-threaded program into a nondeterministic sequential program that preserves reachability for all round-robin schedules with a given bound on the number of rounds. We then reuse existing high-performance BMC tools as backends for the sequential verification problem. Our translation is carefully designed to introduce very small memory overheads and very few sources of nondeterminism, so it produces tight SAT/SMT formulae, and is thus very effective in practice: Our Lazy-CSeq tool implementing this translation for the C programming language won several gold and silver medals in the concurrency category of the Software Verification Competitions (SV-COMP) 2014–2021 and was able to find errors in programs where all other techniques (including testing) failed. In this article, we give a detailed description of our translation and prove its correctness, sketch its implementation using the CSeq framework, and report on a detailed evaluation and comparison of our approach.

Swarm-based verification methods split a verification problem into a large number of independent simpler tasks and so exploit the availability of large numbers of cores to speed up verification. Lazy-CSeq is a BMC-based bug-finding tool for C programs using POSIX threads that is based on sequentialization. Here we present the tool VeriSmart 2.0, which extends Lazy-CSeq with a swarm-based bug-finding method. The key idea of this approach is to constrain the interleaving such that context switches can only happen within selected tiles (more specifically, contiguous code segments within the individual threads). This under-approximates the program's behaviours, with the number and size of tiles as additional parameters, which allows us to vary the complexity of the tasks. Overall, this significantly improves peak memory consumption and (wall-clock) analysis time.

Concurrency poses a major challenge for program verification, but it can also offer an opportunity to scale when subproblems can be analysed in parallel. We exploit this opportunity here and use a parametrizable code-to-code translation to generate a set of simpler program instances, each capturing a reduced set of the original program's interleavings. These instances can then be checked independently in parallel. Our approach does not depend on the tool that is chosen for the final analysis, is compatible with weak memory models, and amplifies the effectiveness of existing tools, making them find bugs faster and with fewer resources. We use Lazy-CSeq as an off-the-shelf final verifier to demonstrate that our approach is able, already with a small number of cores, to find bugs in the hardest known concurrency benchmarks in a matter of minutes, whereas other dynamic and static tools fail to do so in hours.

Lazy sequentialization is one of the most effective approaches for the bounded verification of concurrent programs. Existing tools assume sequential consistency (SC), thus the feasibility of lazy sequentializations for weak memory models (WMMs) remains untested. Here, we describe the first lazy sequentialization approach for the total store order (TSO) and partial store order (PSO) memory models. We replace all shared memory accesses with operations on a shared memory abstraction (SMA), an abstract data type that encapsulates the semantics of the underlying WMM and implements it under the simpler SC model. We give efficient SMA implementations for TSO and PSO that are based on temporal circular doubly-linked lists, a new data structure that allows an efficient simulation of the store buffers. We show experimentally, both on the SV-COMP concurrency benchmarks and a real world instance, that this approach works well in combination with lazy sequentialization on top of bounded model checking.

Lazy-CSeq is a context-bounded verification tool for sequentially consistent C programs using POSIX threads. It first translates a multi-threaded C program into a bounded nondeterministic sequential C program that preserves bounded reachability for all round-robin schedules up to a given number of rounds. It then reuses existing high-performance bounded model checkers as sequential verification backends. Lazy-CSeq handles the full C language and the main parts of the POSIX thread API, such as dynamic thread creation and deletion, and synchronization via thread join, locks, and condition variables. It supports assertion checking and deadlock detection, and returns counterexamples in case of errors. Lazy-CSeq outperforms other concurrency verification tools and has won the concurrency category of the last two SV-COMP verification competitions.

Providing restrictive and secure access to resources is a challenging and socially important problem. Among the many formal security models, Role Based Access Control (RBAC) has become the norm in many of today's organizations for enforcing security. For every model, it is necessary to analyze and prove that the corresponding system is secure. Such analysis helps understand the implications of security policies and helps organizations gain confidence on the control they have on resources while providing access, and devise and maintain policies. In this paper, we consider security analysis for the Temporal RBAC (TRBAC), one of the extensions of RBAC. The TRBAC considered in this paper allows temporal restrictions on roles themselves, user-permission assignments (UA), permission-role assignments (PA), as well as role hierarchies (RH). Towards this end, we first propose a suitable administrative model that governs changes to temporal policies. Then we propose our security analysis strategy, that essentially decomposes the temporal security analysis problem into smaller and more manageable RBAC security analysis sub-problems for which the existing RBAC security analysis tools can be employed. We then evaluate them from a practical perspective by evaluating their performance using simulated data sets.

Sequentialization translates concurrent programs into equivalent nondeterministic sequential programs so that the different concurrent schedules no longer need to be handled explicitly. It can thus be used as a concurrency preprocessing technique for automated sequential program verification tools. Our CSeq tool implements a novel sequentialization for C programs using pthreads, which extends the Lal/Reps sequentialization to support dynamic thread creation. CSeq now works with three different backend tools, CBMC, ESBMC, and LLBMC, and is competitive with state-of-the-art verification tools for concurrent programs.

We propose a novel scheme for proving administrative role-based access control (ARBAC) policies correct with respect to security properties using the powerful abstraction-based tools available for program verification. Our scheme uses a combination of abstraction and reduction to program verification to perform security analysis. We convert ARBAC policies to imperative programs that simulate the policy abstractly, and then utilize further abstract-interpretation techniques from program analysis to analyze the programs in order to prove the policies secure. We argue that the aggressive set-abstractions and numerical-abstractions we use are natural and appropriate in the access control setting. We implement our scheme using a tool called VAC that translates ARBAC policies to imperative programs followed by an interval-based static analysis of the program, and show that we can effectively prove access control policies correct. The salient feature of our approach are the abstraction schemes we develop and the reduction of role-based access control security (which has nothing to do with programs) to program verification problems.

We present a novel fixed-point algorithm to solve reachability of multi-stack pushdown systems restricted to runs where matching push and pop transitions happen within a bounded number of context switches. The followed approach is compositional, in the sense that the runs of the system are summarized by bounded-size interfaces. Moreover, it is suitable for a direct implementation and can be exploited to prove two new results. We give a sequentialization for this class of systems, i.e., for each such multi-stack pushdown system we construct an equivalent single-stack pushdown system that faithfully simulates the behavior of each thread. We prove that the behavior graphs (multiply nested words) for these systems have bounded tree-width, and thus a number of decidability results can be derived from Courcelle's theorem.

Today, Role Based Access Control (RBAC) is the de facto model used for advanced access control, and is widely deployed in diverse enterprises of all sizes. Several extensions to the authorization as well as the administrative models for RBAC have been adopted in recent years. In this paper, we consider the temporal extension of RBAC (TRBAC), and develop safety analysis techniques for it. Safety analysis is essential for understanding the implications of security policies both at the stage of specification and modification. Towards this end, in this paper, we first define an administrative model for TRBAC. Our strategy for performing safety analysis is to appropriately decompose the TRBAC analysis problem into multiple subproblems similar to RBAC. Along with making the analysis simpler, this enables us to leverage and adapt existing analysis techniques developed for traditional RBAC. We have adapted and experimented with employing two state of the art analysis approaches developed for RBAC as well as tools developed for software testing. Our results show that our approach is both feasible and flexible.

We propose a generalization of results on the decidability of emptiness for several restricted classes of sequential and distributed automata with auxiliary storage (stacks, queues) that have recently been proved. Our generalization relies on reducing emptiness of these automata to finite-state graph automata (without storage) restricted to monadic second-order (MSO) definable graphs of bounded tree-width, where the graph structure encodes the mechanism provided by the auxiliary storage. Our results outline a uniform mechanism to derive emptiness algorithms for automata, explaining and simplifying several existing results, as well as proving new decidability results.

We define a new logic, STRAND, that allows reasoning with heap-manipulating programs using deductive verification and SMT solvers. STRAND logic ("STRucture ANd Data" logic) formulas express constraints involving heap structures and the data they contain; they are defined over a class of pointer-structures R defined using MSO-defined relations over trees, and are of the form ∃→x∀→y (→x,→) x" , where "φ" is a monadic second-order logic (MSO) formulawith additional quantification that combines structural constraints as well as data-constraints, but where the data-constraints are only allowed to refer to "→x" and "→y"

We show that recursive programs where variables range over finite domains can be effectively and efficiently analyzed by describing the analysis algorithm using a formula in a fixed-point calculus. In contrast with programming in traditional languages, a fixed-point calculus serves as a high-level programming language to easily, correctly, and succinctly describe model-checking algorithms While there have been declarative high-level formalisms that have been proposed earlier for analysis problems (e.g., Datalog the fixed-point calculus we propose has the salient feature that it also allows algorithmic aspects to be specified.

We define a new class of languages defined by multi-stack automata that forms a robust subclass of context-sensitive languages, with decidable emptiness and closure under boolean operations. This class, called multi-stack visibly pushdown languages (MVPLs), is defined using multi-stack pushdown automata with two restrictions: (a) the pushdown automaton is visible, i.e. the input letter determines the operation on the stacks, and (b) any computation of the machine can be split into k stages, where in each stage, there is at most one stack that is popped. MVPLs are an extension of visibly pushdown languages that captures noncontext free behaviors, and has applications in analyzing abstractions of multithreaded recursive programs, signifi- cantly enlarging the search space that can be explored for them. We show that MVPLs are closed under boolean operations, and problems such as emptiness and inclusion are decidable. We characterize MVPLs using monadic second-order logic over appropriate structures, and exhibit a Parikh theorem for them.