Abstract We present a case study on proof-driven software understanding of mature, security-critical infrastructure. While formal methods are traditionally applied during the design phase, we present our experience applying formal reasoning onto a mature industrial C++ codebase. We focus on a formal analysis of the core algorithm that implements the Stellar blockchain’s order book. By combining large language models (LLMs), Prototype Verification System (PVS), and Seahorn , we are able to prove core properties of the production codebase. Our approach also identified an inconsistency in documentation related to the reachability of an exception location. Most importantly, however, we produce artifacts that make it easy for code changes to be checked against established invariants. This work demonstrates how the strategic combination of theorem proving and model checking provides a path for delivering robust assurance to legacy systems.

Abstract We release the first tool suite implementingMoXI(Model eXchange Interlingua), an intermediate language for symbolic model checking designed to be an international research-community standard and developed by a widespread collaboration under a National Science Foundation (NSF) CISE Community Research Infrastructure initiative. Although we focus here on hardware verification, theMoXIlanguage is useful for software model checking and verification of infinite-state systems in general.MoXIbuilds on elements of SMT-LIB 2; it is easy to add new theories and operators. Our contributions include: (1) introducing the first tool suite of automated translators into and out of the new model-checking intermediate language; (2) composing an initial example benchmark set enabling the model-checking research community to build future translations; (3) compiling details for utilizing, extending, and improving upon our tool suite, including usage characteristics and initial performance data. Experimental evaluations demonstrate that compiling SMV-language models throughMoXIto perform symbolic model checking with the tools from the last Hardware Model Checking Competition performs competitively with model checking directly vianuXmv.

Abstract Search-based satisfiability procedures try to build a model of the input formula by simultaneously proposing candidate models and deriving new formulae implied by the input.Conflict-drivenprocedures perform non-trivial inferences only when resolving conflicts between formulæ and assignments representing the candidate model. CDSAT (Conflict-Driven SATisfiability) is a method for conflict-driven reasoning inunions of theories. It combines inference systems for individual theories astheory moduleswithin a solver for the union of the theories. This article augments CDSAT with a more generallemma learningcapability and withproof generation. Furthermore, theory modules for several theories of practical interest are shown to fulfill the requirements forcompletenessandterminationof CDSAT. Proof generation is accomplished by aproof-carryingversion of the CDSAT transition system that producesproof objectsin memory accommodating multiple proof formats. Alternatively, one can apply to CDSAT theLCF approach to proofsfrom interactive theorem proving, by defining a kernel of reasoning primitives that guarantees the correctness by construction of CDSAT proofs.

Parsing expression grammars (PEGs) offer a natural opportunity for building verified parser interpreters based on higher-order parsing combinators. PEGs are expressive, unambiguous, and efficient to parse in a top-down recursive descent style. We use the rich type system of the PVS specification language and verification system to formalize the metatheory of PEGs and define a reference implementation of a recursive parser interpreter for PEGs. In order to ensure termination of parsing, we define a notion of a well-formed grammar. Rather than relying on an inductive definition of parsing, we use abstract syntax trees that represent the computational trace of the parser to provide an effective proof certificate for correct parsing and ensure that parsing properties including soundness and completeness are maintained. The correctness properties are embedded in the types of the operations so that the proofs can be easily constructed from local proof obligations. Building on the reference parser interpreter, we define a packrat parser interpreter as well as an extension that is capable of semantic interpretation. Both these parser interpreters are proved equivalent to the reference one. All of the parsers are executable. The proofs are formalized in mathematical terms so that similar parser interpreters can be defined in any specification language with a type system similar to PVS.

The recent drive towards achieving greater autonomy and intelligence in robotics has led to high levels of complexity. Autonomous robots increasingly depend on third-party off-the-shelf components and complex machine-learning techniques. This trend makes it challenging to provide strong design-time certification of correct operation. To address these challenges, we present SOTER, a robotics programming framework with two key components: (1) a programming language for implementing and testing high-level reactive robotics software, and (2) an integrated runtime assurance (RTA) system that helps enable the use of uncertified components, while still providing safety guarantees. SOTER provides language primitives to declaratively construct a RTA module consisting of an advanced, high-performance controller (uncertified), a safe, lower-performance controller (certified), and the desired safety specification. The framework provides a formal guarantee that a well-formed RTA module always satisfies the safety specification, without completely sacrificing performance by using higher performance uncertified components whenever safe. SOTER allows the complex robotics software stack to be constructed as a composition of RTA modules, where each uncertified component is protected using a RTA module. To demonstrate the efficacy of our framework, we consider a real-world case-study of building a safe drone surveillance system. Our experiments both in simulation and on actual drones show that the SOTER-enabled RTA ensures the safety of the system, including when untrusted third-party components have bugs or deviate from the desired behavior.

Search-based satisfiability procedures try to construct a model of the input formula by simultaneously proposing candidate models and deriving new formulae implied by the input. When the formulae are satisfiable, these procedures generate a model as a witness. Dually, it is desirable to have a proof when the formulae are unsatisfiable. Conflict-driven procedures perform nontrivial inferences only when resolving conflicts between the formulae and assignments representing the candidate model. CDSAT (Conflict-Driven SATisfiability) is a method for conflict-driven reasoning in combinations of theories. It combines solvers for individual theories as theory modules within a solver for the union of the theories. In this paper we endow CDSAT with lemma learning and proof generation. For the latter, we present two techniques. The first one produces proof objects in memory: it assumes that all theory modules produce proof objects and it accommodates multiple proof formats. The second technique adapts the LCF approach to proofs from interactive theorem proving to conflict-driven SMT-solving and theory combination, by defining a small kernel of reasoning primitives that guarantees that CDSAT proofs are correct by construction.

Cyber-security has emerged as a pressing issue for transportation systems. Studies have shown that attackers can attack modern vehicles from a variety of interfaces and gain access to the most safety-critical components. Such threats become even broader and more challenging with the emergence of vehicle-to-vehicle (V2V) and vehicle-to-infrastructure (V2I) communication technologies. Addressing the security issues in transportation systems requires comprehensive approaches that encompass considerations of security mechanisms, safety properties, resource constraints, and other related system metrics. In this work, we propose an integrated framework that combines hybrid modeling, formal verification, and automated synthesis techniques for analyzing the security and safety of transportation systems and carrying out design space exploration of both in-vehicle electronic control systems and vehicle-to-vehicle communications. We demonstrate the ideas of our framework through a case study of cooperative adaptive cruise control.

Multi-rate systems arise naturally in distributed settings where computing units execute periodically according to their local clocks and communicate among themselves via message passing. We present a systematic way of designing and verifying such systems with the assumption of bounded drift for local clocks and bounded communication latency. First, we capture the system model through an architecture definition language (called RADL) that has a precise model of computation and communication. The RADL paradigm is simple, compositional, and resilient against denial-of-service attacks. Our radler build tool takes the architecture definition and individual local functions as inputs and generate executables for the overall system as output. In addition, we present a modular encoding of multi-rate systems using calendar automata and describe how to verify real-time properties of these systems using SMT-based infinite-state bounded model checking. Lastly, we discuss our experiences in applying this methodology to building high-assurance cyber-physical systems.

The design of a complex cyber-physical system is centered around one or more models of computation (MoCs). These models define the semantic framework within which a network of sensors, controllers, and actuators operate and interact with each other. In this paper, we examine the foundations of a quasi-synchronous model of computation Our version of the quasi-synchronous model is inspired by the Robot Operating System (ROS). It consists of nodes that encapsulate computation and topic channels that are used for communicating between nodes. The nodes execute with a fixed period with possible jitter due to local clock drift and scheduling uncertainties, but are not otherwise synchronized. The channels are implemented through a mailbox semantics. In each execution step, a node reads its incoming mailboxes, applies a next-step operation to update its local state, and writes to all its outgoing mailboxes. The underlying transport mechanism implements the mailbox-to-mailbox data transfer with some bounded latency. Messages can be lost if a mailbox is over-written before it is read. We prove a number of basic theorems that are useful for designing robust high-assurance cyber-physical systems using this simple model of computation. We show that depending on the relative rates of the sender and receiver, there is a bound on the number of consecutive messages that can be lost. By increasing the mailbox queue size to a given bound, message loss can be eliminated. We demonstrate that there is a bound on the age of inputs that are used in any processing step. This in turn can be used to bound the end-to-end sense-control-actuate latency. We illustrate how these theorems are useful in designing and verifying a thermostat-based heating system. Our proofs have been mechanically verified using the Prototype Verification System (PVS).

Robot manipulators are widely used in many industrial automation applications. A robot manipulator moves the end-effector to the configuration instructed by the user. The user input from a master unit is transformed into the desired configuration through forward kinematics. This configuration is communicated to the robot controller, which employs inverse kinematics to transform the configuration into joint angles. The control algorithm is implemented as software and embedded into the robot controller. The software is typically written in traditional programming languages like C or C++. We introduce a Simulink Library ModelRob that provides basic building blocks to model kinematics of a robot manipulator. Availability of such a library enables Model-Based Development (MBD) of robot manipulator software, where the manipulator controller can be modeled using ModelRob library blocks, and production code can be automatically generated using existing code generators for Simulink. We enlist the existing tools that can be useful in the verification and validation stage of the MBD process, and outline the need for tool-support for verification activities specific to building robust robot manipulator software. Using ModelRob library we have modeled Cartesian space motion controller of a robot manipulator in Simulink and successfully generated C code from the model.

Embedded control systems typically comprise continuous control laws combined with discrete mode logic. These systems are modeled using a hybrid automaton formalism, which is obtained by combining the discrete transition system formalism with continuous dynamical systems. This paper develops automated analysis techniques for asserting correctness of hybrid system designs. Our approach is based on symbolic representation of the state space of the system using mathematical formulas in an appropriate logic. Such formulas are manipulated using symbolic theorem proving techniques. It is important that formal analysis should be unobtrusive and acceptable to engineering practice. We motivate a methodology called invisible formal methods that provides a graded sequence of formal analysis technologies ranging from extended typechecking, through approximation and abstraction, to model checking and theorem proving. As an instance of invisible formal methods, we describe techniques to check inductive invariants, or extended types, for hybrid systems and compute discrete finite state abstractions automatically to perform reachability set computation. The abstract system is sound with respect to the formal semantics of hybrid automata. We also discuss techniques for performing analysis on nonstandard semantics of hybrid automata. We also briefly discuss the problem of translating models in Simulink/Stateflow language, which is widely used in practice, into the modeling formalisms, like hybrid automata, for which analysis tools are being developed.

Summary form only given. The automated construction of mathematical proof is a basic activity in computing. Since the dawn of the field of automated reasoning, there have been two divergent schools of thought. One school, best represented by Alan Robinson's resolution method, is based on simple uniform proof search procedures guided by heuristics. The other school, pioneered by Hao Wang, argues for problem-specific combinations of decision and semi-decision procedures. While the former school has been dominant in the past, the latter approach has greater promise. In recent years, several high quality inference engines have been developed, including propositional satisfiability solvers, ground decision procedures for equality and arithmetic, quantifier elimination procedures for integers and reals, and abstraction methods for finitely approximating problems over infinite domains. We describe some of these "little engines of proof" and a few of the ways in which they can be combined. We focus in particular on the combination ground decision procedures and their use in automated verification. We conclude by arguing for a modem reinterpretation and reappraisal of Hao Wang's hitherto neglected ideas on inferential analysis.

Decision procedures for equality in a combination of theories are at the core of a number of verification systems. R.E. Shostak's (J. of the ACM, vol. 31, no. 1, pp. 1-12, 1984) decision procedure for equality in the combination of solvable and canonizable theories has been around for nearly two decades. Variations of this decision procedure have been implemented in a number of specification and verification systems, including STP, EHDM, PVS, STeP and SVC. The algorithm is quite subtle and a correctness argument for it has remained elusive. Shostak's algorithm and all previously published variants of it yield incomplete decision procedures. We describe a variant of Shostak's algorithm, along with proofs of termination, soundness and completeness.

A specification language used in the context of an effective theorem prover can provide novel features that enhance precision and expressiveness. In particular, type checking for the language can exploit the services of the theorem prover. We describe a feature called "predicate subtyping" that uses this capability and illustrate its utility as mechanized in PVS.

The decision problem is studied for fragments of second order linear logic without modalities. It is shown that the structural rules of contraction and weakening may be simulated by second order propositional quantifiers and the multiplicative connectives. Among the consequences are the undecidability of the intuitionistic second order fragment of propositional multiplicative linear logic and the undecidability of multiplicative linear logic with first order and second order quantifiers.

PVS is the most recent in a series of verification systems developed at SRI. Its design was strongly influenced, and later refined, by our experiences in developing formal specifications and mechanically checked verifications for the fault-tolerant architecture, algorithms, and implementations of a model "reliable computing platform" (RCP) for life-critical digital flight-control applications, and by a collaborative project to formally verify the design of a commercial avionics processor called AAMP5. Several of the formal specifications and verifications performed in support of RCP and AAMP5 are individually of considerable complexity and difficulty. But in order to contribute to the overall goal, it has often been necessary to modify completed verifications to accommodate changed assumptions or requirements, and people other than the original developer have often needed to understand, review, build on, modify, or extract part of an intricate verification. We outline the verifications performed, present the lessons learned, and describe some of the design decisions taken in PVS to better support these large, difficult, iterative, and collaborative verifications.>

We present a general framework for proof search in first-order cut-free sequent calculi and apply it to the specific case of linear logic. In this framework, Herbrand functions are used to encode universal quantification, and unification is used to instantiate existential quantifiers so that the eigenvariable conditions are respected. We present an optimization of this procedure that exploits the permutabilities of the subject logic. We prove the soundness and completeness of several related proof search procedures. This proof search framework is used to show that provability for first-order MALL is in NEXPTIME, and first-order MLL is in NP. Performance comparisons based on Prolog implementations of the procedures are also given. The optimization of the quantifier steps in proof search can be combined effectively with a number of other optimizations that are also based on permutability.>

An embedding of the implicational propositional intuitionistic logic (IIL) into the nonmodal fragment of intuitionistic linear logic (IMALL) is given. The embedding preserves cut-free proofs in a proof system that is a variant of IIL. The embedding is efficient and provides an alternative proof of the PSPACE-hardness of IMALL. It exploits several proof-theoretic properties of intuitionistic implication that analyze the use of resources in IIL proofs.>

It is shown that, unlike most other propositional (quantifier-free) logics, full propositional linear logic is undecidable. Further, it is provided that without the model storage operator, which indicates unboundedness of resources, the decision problem becomes PSPACE-complete. Also established are membership in NP for the multiplicative fragment, NP-completeness for the multiplicative fragment extended with unrestricted weakening, and undecidability for certain fragments of noncommutative propositional linear logic.>

The Church-Rosser theorem is a celebrated metamathematical result on the lambda calculus. We describe a formalization and proof of the Church-Rosser theorem that was carried out with the Boyer-Moore theorem prover. The proof presented in this paper is based on that of Tait and Martin-Löf. The mechanical proof illustrates the effective use of the Boyer-Moore theorem prover in proof checking difficult metamathematical proofs.