Abstract We present PyCaliper : a Python-embedded framework to formulate, verify, and auto-synthesize specifications for hardware designs at the register transfer level (RTL). By being Python-embedded, PyCaliper is easy to use and benefits from object-oriented principles and Python’s rich ecosystem. Further, PyCaliper is a common platform that integrates novel research techniques such as specification synthesis and mature, industry-scale tooling, thus allowing them to benefit from each other. We discuss the system and implementation of PyCaliper and demonstrate its use in two case studies: in the first we compare a custom verification backend with a commercial tool and gain insights about the former, and in the second we demonstrate invariant synthesis for an RTL design.

Many software systems are polyglot; that is, they comprise programs implemented in a combination of programming languages. Program verifiers, however, tend to be customized for individual languages. Verification by compiling to a common encoding requires supporting full language syntax and semantics which is prohibitive for modern languages. We present POLYVER, an alternative compositional approach to polyglot verification that bootstraps off-the-shelf language-specific verifiers with abstraction and synthesis. POLYVER uses contracts written in an intermediate language to abstract individual procedures in the system. Our verification approach uses language-specific verifiers (e.g., for C or Rust) to validate these contracts and the UCLID5 model checker for com- positionally verifying a temporal property on the overall system using the contracts. The intermediate language sidesteps the need for compiling implementation languages to a common encoding, a key obstacle with polyglot verification. Finally, POLYVER automates the generation of contracts using synthesis oracles such as large-language-models (LLMs). Overall POLYVER performs contract synthesis and verification in a counterexample-guided abstraction refinement and inductive synthesis (CEGIS-CEGAR) loop to verify the system-level property. We use POLYVER to verify programs in the Lingua Franca polyglot language. We are able to verify systems with C and Rust procedures, as well as C language fragments that were unsupported in previous work.

Hardware execution attacks exploit subtle microarchitectural interactions to leak secret data. While checking programs for the existence of such attacks is essential, verification of software against the full hardware implementation does not scale. Verification using abstract formal models of the hardware can help provide strong security guarantees while leveraging abstraction to achieve scalability. However, handwriting accurate abstract models is tedious and error-prone. Hence, we need techniques to generate models that enable sound yet scalable security analysis automatically.

Formal verification can help ensure the correctness of today’s processors. However, such formal verification requires formal specifications of the processors being verified. Today, these specifications are mostly written by hand, which is tedious and error-prone. Furthermore, architects and hardware engineers generally do not have formal methods experience, making it even harder for them to write formal specifications. Existing methods for the automated synthesis of formal microarchitectural specifications utilise RTL implementations of processors for their synthesis, preventing their usage until RTL implementation of the processor has completed. This hampers the effectiveness of formal verification for processors, as catching design bugs pre-RTL can reduce verification overhead and overall development time.

Abstract We consider the verification of liveness properties for concurrent programs running on weak memory models. To that end, we identify notions of fairness that preclude demonic non-determinism, are motivated by practical observations, and are amenable to algorithmic techniques. We provide both logical and stochastic definitions of our fairness notions, and prove that they are equivalent in the context of liveness verification. In particular, we show that our fairness allows us to reduce the liveness problem (repeated control state reachability) to the problem of simple control state reachability. We show that this is a general phenomenon by developing a uniform framework which serves as the formal foundation of our fairness definition, and can be instantiated to a wide landscape of memory models. These models include SC, TSO, PSO, (Strong/Weak) Release-Acquire, Strong Coherence, FIFO-consistency, and RMO.

We present a scalable approach for formally verifying the correctness of the Compute Engine (CE) against its ISA (Instruction Set Architecture) specification in an FHE (Fully Homomorphic Encryption) accelerator, critical to many applications where safety and security of information is of vital importance. It combines algorithmic verification of the micro-architecture modules in the CE against their functional specifications and implementation verification of the CE hardware against its micro-architecture algorithmic specifications. The correctness of the CE is guaranteed by treating micro-architecture modules as semantic-preserving program transformations and leveraging the composability of the semantic-preserving properties well established in compiler design and verification.

Abstract We consider parameterized verification of systems executing according to the total store ordering (TSO) semantics. The processes manipulate abstract data types over potentially infinite domains. We present a framework that translates the reachability problem for such systems to the reachability problem for register machines enriched with the given abstract data type.

Abstract UCLID5 is a tool for the multi-modal formal modeling, verification, and synthesis of systems. It enables one to tackle verification problems for heterogeneous systems such as combinations of hardware and software, or those that have multiple, varied specifications, or systems that require hybrid modes of modeling. A novel aspect of UCLID5 is an emphasis on the use of syntax-guided and inductive synthesis to automate steps in modeling and verification. This tool paper presents new developments in the UCLID5 tool including new language features, integration with new techniques for syntax-guided synthesis and satisfiability solving, support for hyperproperties and combinations of axiomatic and operational modeling, demonstrations on new problem classes, and a robust implementation.

Abstract We present Probabilistic Total Store Ordering (PTSO) – a probabilistic extension of the classical TSO semantics. For a given (finite-state) program, the operational semantics of PTSO induces an infinite-state Markov chain. We resolve the inherent non-determinism due to process schedulings and memory updates according to given probability distributions. We provide a comprehensive set of results showing the decidability of several properties for PTSO, namely (i) Almost-Sure (Repeated) Reachability: whether a run, starting from a given initial configuration, almost surely visits (resp. almost surely repeatedly visits) a given set of target configurations. (ii) Almost-Never (Repeated) Reachability: whether a run from the initial configuration, almost never visits (resp. almost never repeatedly visits) the target. (iii) Approximate Quantitative (Repeated) Reachability: to approximate, up to an arbitrary degree of precision, the measure of runs that start from the initial configuration and (repeatedly) visit the target. (iv) Expected Average Cost: to approximate, up to an arbitrary degree of precision, the expected average cost of a run from the initial configuration to the target. We derive our results through a nontrivial combination of results from the classical theory of (infinite-state) Markov chains, the theories of decisive and eager Markov chains, specific techniques from combinatorics, as well as, decidability and complexity results for the classical (non-probabilistic) TSO semantics. As far as we know, this is the first work that considers probabilistic verification of programs running on weak memory models.

We study the safety verification problem for parameterized systems under the release-acquire (RA) semantics. In the non-parameterized setting, access to atomic compare-and-swap (CAS) instructions renders the safety verification problem undecidable. In the light of this result, we consider parameterized systems consisting of an unbounded number of environment threads executing identical but CAS-free programs combined with a fixed number of distinguished threads that are unrestricted. Our first contribution is an effective and simplified RA semantics for such systems. We leverage the simplified semantics to show that safety verification becomes PSPACE in the parameterized case, an optimistic result for algorithmic verification. Our proof uses an encoding to Datalog which, in addition to the complexity upper bound, suggests a verification algorithm based on Horn clause solvers. We also provide a matching lower bound showing that safety verification is PSPACE-hard.

Abstract We consider the reachability problem for finite-state multi-threaded programs under the promising semantics () of Lee et al., which captures most common program transformations. Since reachability is already known to be undecidable in the fragment of with only release-acquire accesses (-), we consider the fragment with only relaxed accesses and promises (). We show that reachability under is undecidable in general and that it becomes decidable, albeit non-primitive recursive, if we bound the number of promises. Given these results, we consider a bounded version of the reachability problem. To this end, we bound both the number of promises and of “view-switches”, i.e., the number of times the processes may switch their local views of the global memory. We provide a code-to-code translation from an input program under (with relaxed and release-acquire memory accesses along with promises) to a program under SC, thereby reducing the bounded reachability problem under to the bounded context-switching problem under SC. We have implemented a tool and tested it on a set of benchmarks, demonstrating that typical bugs in programs can be found with a small bound.

Testing containment of queries is a fundamental reasoning task in knowledge representation. We study here the containment problem for Conjunctive Regular Path Queries (CRPQs), a navigational query language extensively used in ontology and graph database querying. While it is known that containment of CRPQs is EXPSPACE-complete in general, we focus here on severely restricted fragments, which are known to be highly relevant in practice according to several recent studies. We obtain a detailed overview of the complexity of the containment problem, depending on the features used in the regular expressions of the queries, with completeness results for NP, Pi2p, PSPACE or EXPSPACE.

We introduce a new setting where a population of agents, each modelled by a finite-state system, are controlled uniformly: the controller applies the same action to every agent. The framework is largely inspired by the control of a biological system, namely a population of yeasts, where the controller may only change the environment common to all cells. We study a synchronisation problem for such populations: no matter how individual agents react to the actions of the controller, the controller aims at driving all agents synchronously to a target state. The agents are naturally represented by a non-deterministic finite state automaton (NFA), the same for every agent, and the whole system is encoded as a 2-player game. The first player (Controller) chooses actions, and the second player (Agents) resolves non-determinism for each agent. The game with m agents is called the m -population game. This gives rise to a parameterized control problem (where control refers to 2 player games), namely the population control problem: can Controller control the m-population game for all m in N whatever Agents does? Comment: This is a journal version of the extended abstract arXiv:1707.02058 which appeared in Concur 2017, together with proofs