This paper presents an upper bound on the number of trajectories needed for computing bounded-time reachable set of linear dynamical systems. The main result of the paper is that for a large class of n-dimensional linear time-invariant systems, only a constant number of trajectories are needed. In fact, only one trajectory is needed; independent of the number of dimensions of the system. This is a strict improvement over the previously presented result where n+1 trajectories were required for reachable set computation. The presented algorithm highlights some of the connections between reachability and controllability. We also give the computational complexity of the algorithm to compute reachable set.
A primary goal of static analysis based on abstract interpretation is to infer invariants to verify programs. Memory safety checks (e.g., proving the absence of out-of-bound accesses) require tracking linear relationships between pointer offsets and object sizes, such as for accessing memory. Choosing the right abstract domain is crucial, as each domain captures different kinds of properties. For example, Zones and Octagons limit themselves to unit coefficients and cannot express the invariants required for memory safety. On the other hand, the Polyhedra domain can capture any linear relation but does not scale in real applications. In this paper, as a compromise between expressiveness and efficiency while still covering our target properties, we introduce Template DBM–a new weakly relational numerical domain for expressing Two Variables per Inequality (TVPI) constraints with fixed coefficients. Template DBM supports efficient join, inclusion, and saturation. It strikes the balance of expressiveness and cost between Zones and TVPI. We implemented Template DBM in the Crab library and evaluated it against Zones and Polyhedra domains for memory safety analysis of aws-c-common from AWS and firedancer from Solana. Our results show that Template DBM maintains its intended level of precision, scales comparably to Zones, and is significantly more efficient than Polyhedra.
The emergence of programmable network elements and their usage in critical infrastructure is increasing the demand for formal guarantees of their correctness. This paper presents the first P4 software switch connected by proof to a formal semantics. This is accomplished by adjusting and optimizing the HOL4P4 semantics to create an efficient interpreter that can be compiled using the verified CakeML compiler. We demonstrate practical performance in a set of experiments, achieving several orders of magnitude improvement in throughput over existing semantics-based interpreters, with only small performance penalties compared to the BMv2 reference switch written in C++.
LiquidHaskell is an extension to Haskell that enhances its type system with refinement types, enabling the integration of formal verification to software development by the introduction of type annotations in the form of logical predicates in data structure and function definitions. In this paper, we explore the specification and verification capabilities of LiquidHaskell by focusing on balanced trees, and more specifically on Braun trees, a data structure used for representing functional arrays. We formalize some properties of balanced trees, concerning the relationship between their height and number of nodes. On top of these properties, we verify the invariants of functional and flexible arrays, resulting in an implementation that encodes most of the pre-conditions and post-conditions that preserve such invariants.
To support rely-guarantee reasoning, we present an extension to Isabelle/HOL’s built-in library, which we use to verify a hierarchy of queue locks. The framework incorporates novel features of Isabelle, and enables flexible syntax, assertion-annotations, and tactics for both automated and structured proofs. Assertion-annotations enable elegant top-down specification from an abstract queue lock to a non-trivial, practical circular-buffer queue lock.
