Search

We discuss integrating abstract data types (ADTs) in the KeY theorem prover by a new approach to model data types using Isabelle/HOL as an interactive back-end, and represent Isabelle theorems as user-defined taclets in KeY. As a case study of this new approach, we reason about Java's Collection interface using histories, and we prove the correctness of several clients that operate on multiple objects, thereby significantly improving the state-of-the-art of history-based reasoning. Open Science. Includes video material (Bian and Hiep in FigShare, 2021. https://doi.org/10.6084/m9.figshare.c.5413263) and a source code artifact (Bian et al. in Zenodo, 2022. https://doi.org/10.5281/zenodo.7079126). [ABSTRACT FROM AUTHOR]

In this paper, we consider the problem of model checking fair transition systems expressed symbolically in the framework of Satisfiability Modulo Theories. This problem, referred to as Verification Modulo Theories, is tackled by combining two key elements from the legacy of Ed Clarke: SAT-based verification and abstraction refinement. We show how fundamental SAT-based algorithms have been lifted to deal with the extended expressiveness with a tight integration of abstraction within a CEGAR loop. In turn, the case of nonlinear theories is based on a CEGAR loop over the linear case. These two elements have also deeply impacted the development of the NuSMV model checker, born from a joint project between FBK and CMU, and its successor nuXmv, whose core integrates SMT-based techniques for VMT. [ABSTRACT FROM AUTHOR]

This paper addresses model checking based on SAT solvers and Craig interpolants. We tackle major scalability problems of state-of-the-art interpolation-based approaches, and we achieve two main results: (1) A novel model checking algorithm; (2) A new and flexible way to handle an incremental representation of (over-approximated) forward reachable states. The new model checking algorithm IGR, Interpolation with Guided Refinement, partially takes inspiration from IC3 and interpolation sequences. It bases its robustness and scalability on incremental refinement of state sets, and guided unwinding/simplification of transition relation unrollings. State sets, the central data structure of our algorithm, are incrementally refined, and they represent a valuable information to be shared among related problems, either in concurrent or sequential (multiple-engine or multiple-property) execution schemes. We provide experimental data, showing that IGR extends the capability of a state-of-the-art model checker, with a specific focus on hard-to-prove properties. [ABSTRACT FROM AUTHOR]

This paper describes our experience with symbolic model checking in an industrial setting. We have proved that the initial boot code running in data centers at Amazon Web Services is memory safe, an essential step in establishing the security of any data center. Standard static analysis tools cannot be easily used on boot code without modification owing to issues not commonly found in higher-level code, including memory-mapped device interfaces, byte-level memory access, and linker scripts. This paper describes automated solutions to these issues and their implementation in the C Bounded Model Checker (CBMC). CBMC is now the first source-level static analysis tool to extract the memory layout described in a linker script for use in its analysis. [ABSTRACT FROM AUTHOR]

We study verification problems for autonomous swarms of mobile robots that self-organize and cooperate to solve global objectives. In particular, we focus in this paper on the model proposed by Suzuki and Yamashita of anonymous robots evolving in a discrete space with a finite number of locations (here, a ring). A large number of algorithms have been proposed working for rings whose size is not a priori fixed and can be hence considered as a parameter. Handmade correctness proofs of these algorithms have been shown to be error-prone, and recent attention had been given to the application of formal methods to automatically prove those. Our work is the first to study the verification problem of such algorithms in the parameterized case. We show that safety and reachability problems are undecidable for robots evolving asynchronously. On the positive side, we show that safety properties are decidable in the synchronous case, as well as in the asynchronous case for a particular class of algorithms. Several other properties of the protocol can be decided as well. Decision procedures rely on an encoding in Presburger arithmetics formulae that can be verified by an SMT-solver. Feasibility of our approach is demonstrated by the encoding of several case studies. [ABSTRACT FROM AUTHOR]

Runtime verification is an area of formal methods that studies the dynamic analysis of execution traces against formal specifications. Typically, the two main activities in runtime verification efforts are the process of creating monitors from specifications, and the algorithms for the evaluation of traces against the generated monitors. Other activities involve the instrumentation of the system to generate the trace and the communication between the system under analysis and the monitor. Most of the applications in runtime verification have been focused on the dynamic analysis of software, even though there are many more potential applications to other computational devices and target systems. In this paper we present a collection of challenges for runtime verification extracted from concrete application domains, focusing on the difficulties that must be overcome to tackle these specific challenges. The computational models that characterize these domains require to devise new techniques beyond the current state of the art in runtime verification. [ABSTRACT FROM AUTHOR]

This paper addresses the problem of handling SAT solving in IC3. SAT queries posed by IC3 significantly differ in both character and number from those posed by other SAT-based model checking algorithms. In addition, IC3 has proven to be highly sensitive to the way its SAT solving requirements are handled at the implementation level. The scenario pictured above poses serious challenges for any implementation of the algorithm. Deciding how to manage the SAT solving work required by the algorithm is key to IC3 performance. The purpose of this paper is to determine the best way to handle SAT solving in IC3. First we provide an in-depth characterization of the SAT solving work required by IC3 in order to gain useful insights into how to best handle its queries. Then we propose an experimental comparison of different strategies for the allocation, loading and clean-up of SAT solvers in IC3. Among the compared strategies we include the ones typically used in state-of-the-art model checking tools as well as some novel ones. Alongside comparing multiple versus single SAT solver implementations of IC3, we propose the use of secondary SAT solvers dedicated to handling certain types of queries. Different heuristics for SAT solver clean-up are evaluated, including new ones that follow the locality of the verification process. We also address clause database minimality, comparing different CNF encoding techniques. Though not finding a clear winner among the different sets of strategies compared, we outline several potential improvements for portfolio-based verification tools with multiple engines and tunings. [ABSTRACT FROM AUTHOR]

While SAT-based algorithms have largely displaced BDD-based verification techniques due to their typically higher scalability, there are classes of problems for which BDD-based reachability analysis is the only existing method for an automated solution. Nonetheless, reachability engines require a high degree of tuning to perform well on challenging benchmarks. In addition to clever partitioning and scheduling techniques, the use of hints has been proposed to decompose an otherwise breadth-first fixedpoint computation into a series of underapproximate computations, requiring a larger number of (pre-)image iterations though often significantly reducing peak BDD size and thus resource requirements. In this paper, we introduce a novel approach to boost the scalability of reachability computation: automated netlist-based hint generation. Experiments confirm that this approach can yield significant resource reductions; often over an order of magnitude on complex problems compared to reachability analysis without hints, and even compared to SAT-based proof techniques. [ABSTRACT FROM AUTHOR]

This paper presents the formal verification of start-up for a differential ring-oscillator circuit used in industrial designs. We present an efficient algorithm for finding DC equilibria to establish a condition that ensure the oscillator is free from lock-up. Further, we present a formal verification solution for the problem. Using dynamical systems theory, we show that any oscillator must have a non-empty set of states from which it fails to start properly. However, it is possible to show that these failures only occur with zero probability. To do so, this paper generalizes the 'cone argument' initially presented in (Mitchell and Greenstreet, in Proceedings of the third workshop on designing correct circuits, ) and proves the soundness of this generalization. This paper also shows how concepts from analog design such as differential operation can be soundly incorporated into the verification to produce simpler models and reduce the complexity of the verification task. [ABSTRACT FROM AUTHOR]

Algebraic error correcting codes (ECC) are widely used to implement reliability features in modern servers and systems and pose a formidable verification challenge. We present a novel methodology and techniques for provably correct design of ECC logics. The methodology is comprised of a design specification method that directly exposes the ECC algorithm's underlying math to a verification layer, encapsulated in a tool 'BLUEVERI', which establishes the correctness of the design conclusively by using an apparatus of computational algebraic geometry (Buchberger's algorithm for Gröbner basis construction). We present results from its application to example circuits to demonstrate the effectiveness of the approach. The methodology has been successfully applied to prove correctness of large error correcting circuits on IBM's POWER systems to protect memory storage and processor to memory communication, as well as a host of smaller error correcting circuits. [ABSTRACT FROM AUTHOR]

Verification methods based on SAT, SMT, and theorem proving often rely on proofs of unsatisfiability as a powerful tool to extract information in order to reduce the overall effort. For example a proof may be traversed to identify a minimal reason that led to unsatisfiability, for computing abstractions, or for deriving Craig interpolants. In this paper we focus on two important aspects that concern efficient handling of proofs of unsatisfiability: compression and manipulation. First of all, since the proof size can be very large in general (exponential in the size of the input problem), it is indeed beneficial to adopt techniques to compress it for further processing. Secondly, proofs can be manipulated as a flexible preprocessing step in preparation for interpolant computation. Both these techniques are implemented in a framework that makes use of local rewriting rules to transform the proofs. We show that a careful use of the rules, combined with existing algorithms, can result in an effective simplification of the original proofs. We have evaluated several heuristics on a wide range of unsatisfiable problems deriving from SAT and SMT test cases. [ABSTRACT FROM AUTHOR]

Trigger querying is the problem of finding, given a system M and an LTL formula φ, the set of scenarios that trigger φ in M; that is, the language L of finite computations of M such that all infinite computations that have a prefix in L continue with a suffix that satisfies φ. Trigger querying significantly extends query checking, which seeks propositional solutions, and is an extremely useful methodology for system exploration and understanding. The weakness of trigger querying lies in the fact that the size of the solution is linear in the size of the system. For trigger querying to become feasible in practice, we must offer solutions to cope with systems of big, and possibly infinite, state spaces. In this paper we describe an abstraction-refinement framework for trigger querying. Instead of reasoning about the system M, we reason about an abstraction of it and return to the user two languages that under- and over-approximate the language L of computations that trigger φ in M. We describe an automata-theoretic approach for refining and reducing the gap between the approximations and show how, unlike classical counterexample-based refinement approaches, here it is possible to symbolically handle batches of counterexamples. We show that our framework is robust and can be applied also for classical query checking as well as variants and extensions of trigger querying. [ABSTRACT FROM AUTHOR]

We describe a reduction from temporal property verification to a program analysis problem. First we present a proof system that, unlike the standard formulation, is more amenable to reasoning about infinite-state systems: disjunction is treated by partitioning, rather than enumerating, the state space and temporal operators are characterized with special sets of states called frontiers. We then describe a transformation that, with the use of procedures and nondeterminism, enables off-the-shelf program analysis tools to naturally perform the reasoning necessary for proving temporal properties ( e.g. backtracking, eventuality checking, tree counterexamples for branching-time properties, abstraction refinement, etc.). Using examples drawn from the PostgreSQL database server, Apache web server, and Windows OS kernel, we demonstrate the practical viability of our work. [ABSTRACT FROM AUTHOR]

Abstract microarchitectural models of communication fabrics present a challenge for verification. Due to the presence of deep pipelining, a large number of queues and distributed control, the state space of such models is usually too large for enumeration by protocol verification tools such as Murphi. On the other hand, we find that state-of-the-art rtl model checkers such as abc have poor performance on these models since there is very little opportunity for localization and most of the recent capacity advances in rtl model checking have come from better ways of discarding the irrelevant parts of the model. In this work we explore a new approach for verifying these models where we capture a model at a high level of abstraction by requiring that it be described using a small set of well-defined microarchitectural primitives. We exploit the high level structure present in this description, to automatically strengthen some classes of properties, in order to make them 1-step inductive, and then use an rtl model checker to prove them. In some cases, even if we cannot make the property inductive, we can dramatically reduce the number and complexity of lemmas that are needed to make the property inductive. [ABSTRACT FROM AUTHOR]

When a model does not satisfy a given specification, a counterexample is produced by the model checker to demonstrate the failure. A user must then examine the counterexample trace, in order to visually identify the failure that it demonstrates. If the trace is long, or the specification is complex, finding the failure in the trace becomes a non-trivial task. In this paper, we address the problem of analyzing a counterexample trace and highlighting the failure that it demonstrates. Using the notion of causality introduced by Halpern and Pearl, we formally define a set of causes for the failure of the specification on the given counterexample trace. These causes are marked as red dots and presented to the user as a visual explanation of the failure. We study the complexity of computing the exact set of causes, and provide a polynomial-time algorithm that approximates it. We then analyze the output of the algorithm and compare it to the one expected by the definition. The algorithm is implemented as a feature in the IBM formal verification platform RuleBase PE, where the visual explanations are an integral part of every counterexample trace. Our approach is independent of the tool that produced the counterexample, and can be applied as a light-weight external layer to any model checking tool, or used to explain simulation traces. [ABSTRACT FROM AUTHOR]

We address the problem of verifying programs manipulating one-selector linked data structures. We propose and study in detail an application of counter automata as an accurate abstract model for this problem. We let control states of the counter automata correspond to abstract heap graphs where list segments without sharing are collapsed, and use counters to keep track of the number of elements in these segments. As a significant theoretical result, we show that the obtained counter automata are bisimilar to the original programs. Moreover, from a practical point of view, our translation allows one to apply efficient automatic analysis techniques and tools developed for counter automata (integer programs) in order to verify both safety as well as termination of list-manipulating programs. As another theoretical contribution, we prove that if the control of the generated counter automata does not contain nested loops (i.e., these automata are flat), both safety and termination are decidable for the original programs. Subsequently, we generalise our counter-automata-based model to keep track of ordering properties over lists storing ordered data. Finally, we show effectiveness of our approach by verifying automatically safety as well as termination of several sorting programs. [ABSTRACT FROM AUTHOR]

In this contribution two extensions for an analog equivalence checking method are proposed, enabling the checking of strongly nonlinear circuits with floating nodes such as digital library cells. Therefore, a structural recognition and mapping of eigenvalues, representing the dynamics, to circuit elements via circuit variables is presented. Additionally, the introduction of reachability analysis is significantly restricting the investigated state space to the relevant parts, avoiding false negatives. The newly introduced methods are compared to existing ones by application to industrial examples. [ABSTRACT FROM AUTHOR]

This document describes how the FORTE STE-based formal verification system was used to verify the RTL implementation of an error control code. The error control code considered is linear: its encoder and decoder proceed by matrix multiplication. Although that function is in essence combinational, its implementation in a high-performance microprocessor is done in a pipelined fashion. The additional state elements introduced by the pipelining quickly push an SMV-style model checker to its capacity limits. With the case-study presented in this document, we show that an STE-style model checker is better suited for this problem. We present two instances of the ECC verification problem. For the first we were able to combine an encoder and a decoder into one model for verification. For the second, such a combination was not possible and we resorted to verifying properties of a matrix that we extracted from the implementation. [ABSTRACT FROM AUTHOR]

We discuss the formal verification of some low-level mathematical software for the Intel® Itanium® architecture. A number of important algorithms have been proven correct using the HOL Light theorem prover. After briefly surveying some of our formal verification work, we discuss in more detail the verification of a square root algorithm, which helps to illustrate why some features of HOL Light, in particular programmability, make it especially suitable for these applications. [ABSTRACT FROM AUTHOR]

Over the past nine years, the Formal Methods Group at the IBM Haifa Research Laboratory has made steady progress in developing tools and techniques that make the power of model checking accessible to the community of hardware designers and verification engineers, to the point where it has become an integral part of the design cycle of many teams. We discuss our approach to the problem of integrating formal methods into an industrial design cycle, and point out those techniques which we have found to be especially effective in an industrial setting. [ABSTRACT FROM AUTHOR]

In the last three years or so we at Enterprise Platforms Group at Intel Corporation have been applying formal methods to various problems that arose during the process of defining platform architectures for Intel's processor families. In this paper we give an overview of some of the problems we have worked on, the results we have obtained, and the lessons we have learned. The last topic is addressed mainly from the perspective of platform architects. [ABSTRACT FROM AUTHOR]

Not long ago, completely automatical formal verification of multipliers was not feasible, even for small input word sizes. However, with Multiplicative Binary Moment Diagrams (*BMD), which is a new data structure for representing arithmetic functions over Boolean variables, methods were proposed by which verification of multipliers with input word sizes of up to 256 Bits is now feasible. Unfortunately, only experimental data has been provided for these verification methods until now. In this paper, we give a formal proof that logic verification with *BMDs is polynomially bounded in both, space and time, when applied to the class of Wallace-tree like multipliers. Using this knowledge online detection of design errors becomes feasible during a verification run. [ABSTRACT FROM AUTHOR]

We propose a novel methodology that combines local BDDs with a hash table for very efficient verification of combinational circuits. The main purpose of this technique is to remove the considerable overhead associated with case-by-case verification of internal node pairs in typical internal correspondence based verification methods. Two heuristics based on the number of structural levels of circuitry looked at and the total number of nodes in the BDD manager are used to control the BDD sizes and introduce new cutsets based on already found equivalent nodes. We verify the ISCAS85 benchmark circuits and demonstrate significant speedup over existing methods. We also verify several hard industrial circuits and show our superiority in extracting internal equivalences. [ABSTRACT FROM AUTHOR]

Several types of Decision Diagrams (DDs) have been proposed for the verification of Integrated Circuits. Recently, word-level DDs like BMDs, *BMDs, HDDs, K*BMDs and *PHDDs have been attracting more and more interest, e.g., by using *BMDs and *PHDDs it was for the first time possible to formally verify integer multipliers and floating point multipliers of “significant” bitlengths, respectively. On the other hand, it has been unknown, whether division, the operation inverse to multiplication, can be efficiently represented by some type of word-level DDs. In this paper we show that the representational power of any word-level DD is too weak to efficiently represent integer division. Thus, neither a clever choice of the variable ordering, the decomposition type or the edge weights, can lead to a polynomial DD size for division. For the proof we introduce Word-Level Linear Combination Diagrams (WLCDs), a DD, which may be viewed as a “generic” word-level DD. We derive an exponential lower bound on the WLCD representation size for integer dividers and show how this bound transfers to all other word-level DDs. [ABSTRACT FROM AUTHOR]

We have verified the FM9801, a microprocessor design whose features include speculative execution, out-of-order issue and completion of instructions using Tomasulo's algorithm, and precise exceptions and interrupts. As a correctness criterion, we used a commutative diagram that compares the result of the pipelined execution from a flushed state to another flushed state with that of the sequential execution. Like many pipelined microprocessors, the FM9801 may not operate correctly if the executed program modifies itself. We discuss the condition under which the processor is guaranteed to operate correctly. In order to show that the correctness criterion is satisfied, we introduce an intermediate abstraction that records the history of executed instructions. Using this abstraction, we define a number of invariant properties that must hold during the operation of the FM9801. We verify these invariant properties, and then derive the proof of the commutative diagram from them. The proof has been mechanically checked by the ACL2 theorem prover. [ABSTRACT FROM AUTHOR]

We present an approach for formally verifying that a high-level microprocessor model behaves as defined by an instruction-set architecture. The technique is based on a specialization of self consistency called incremental flushing and reduces the need and effort required to create manually-generated implementation abstractions. Additionally, incremental flushing reduces the computational complexity of the proof obligations generated when reasoning about out-of-order execution. This is accomplished by comparing the functional behavior of the implementation abstraction over two sets of inputs: one that represents normal operation and one that is simpler, but functionally equivalent. The approach is illustrated on a simple out-of-order microprocessor core. [ABSTRACT FROM AUTHOR]

We present a new technique for verification of complex hardware devices that allows both generality and a high degree of automation. The technique is based on our new way of constructing a “light-weight” completion function together with new encoding of uninterpreted functions called reference file representation. Our technique combines our completion function method and reference file representation with compositional model checking and theorem proving. This extends the state of the art in two directions. First, we obtain a more general verification methodology. Second, it is easier to use, since it has a higher degree of automation. As a benchmark, we take Tomasulo's algorithm for scheduling out-of-order instruction execution used in many modern superscalar processors like the Pentium-II and the PowerPC 604. The algorithm is parameterized by the processor configuration, and our approach allows us to prove its correctness in general, independent of any actual design. [ABSTRACT FROM AUTHOR]

With the trend to partially move safety-related features from courtyards into on-board control software, new challenges arise in supporting such designs by formal verification capabilities, essentially entailing the need for a model-based design process. This paper reports on the usage of the STATEMATE Verification Environment to model and verify a radio-based signaling system, a trial case study offered by the German train system company DB. It shows, that industrially sized applications can be modeled and verified with a verification tool to be offered as a commercial product by I-Logix, Inc. [ABSTRACT FROM AUTHOR]

We examine IBM's exploitation of formal verification using RuleBase—a formal verification tool developed by the IBM Haifa Research Laboratory. The goal of the paper is methodological. We identify an integrated methodology for the deployment of formal verification which involves three complementary modes: architectural verification, block-level verification, and design exploration. [ABSTRACT FROM AUTHOR]

The ability to generate a counter-example is an important feature of model checking tools, because a counter-example provides information to the user in the case that the formula being checked is found to be non-valid. In this paper, we turn our attention to providing similar feedback to the user in the case that the formula is found to be valid, because valid formulas can hide real problems in the model. For instance, propositional logic formulas containing implications can suffer from antecedent failure, in which the formula is trivially valid because the pre-condition of the implication is not satisfiable. We call this vacuity, and extend the definition to cover other kinds of trivial validity. For non-vacuously valid formulas, we define an interesting witness as a non-trivial example of the validity of the formula. We formalize the notions of vacuity and interesting witness, and show how to detect vacuity and generate interesting witnesses in temporal model checking. Finally, we provide a practical solution for a useful subset of ACTL formulas. [ABSTRACT FROM AUTHOR]

A state/event model is a concurrent version of Mealy machines used for describing embedded reactive systems. This paper introduces a technique that uses compositionality and dependency analysis to significantly improve the efficiency of symbolic model checking of state/event models. It makes possible automated verification of large industrial designs with the use of only modest resources (less than 5 minutes on a standard PC for a model with 1421 concurrent machines). The results of the paper are being implemented in the next version of the commercial tool visualSTATETM. [ABSTRACT FROM AUTHOR]

State space exploration is often used to prove properties about sequential behavior of Finite State Machines (FSMs). For example, equivalence of two machines is proved by analyzing the reachable state set of their product machine. Nevertheless, reachability analysis is infeasible on large practical examples. Combinational verification is far less expensive, but on the other hand its application is limited to combinational circuits, or particular design schemes. Finally, approximate techniques imply sufficient, not strictly necessary conditions. The purpose of this paper is to extend the applicability of purely combinational checks. This is generally achieved through state minimization, partitioning, and re-encoding the FSMs to factor out their differences. We focus on re-encoding. In particular, we present an incremental approach to re-encoding for verification that transforms the product machine traversal into a combinational verification in the best case, and into a computationally simpler product machine traversal in the general case. Experimental results demonstrate the effectiveness of this technique on medium-large circuits where other techniques may fail. [ABSTRACT FROM AUTHOR]

Classical logic has so far been the logic of choice in formal hardware verification. This paper proposes the application of intuitionistic logic to the timing analysis of digital circuits. The intuitionistic setting serves two purposes. The model-theoretic properties are exploited to handle the second-order nature of bounded delays in a purely propositional setting without need to introduce explicit time and temporal operators. The proof-theoretic properties are exploited to extract quantitative timing information and to reintroduce explicit time in a convenient and systematic way. We present a natural Kripke-style semantics for intuitionistic propositional logic, as a special case of a Kripke constraint model for Propositional Lax Logic (Information and Computation, Vol. 137, No. 1, 1–33, 1997), in which validity is validity up to stabilisation, and implication ⊃ comes out as “ boundedly gives rise to.” We show that this semantics is equivalently characterised by a notion of realisability with stabilisation bounds as realisers. Following this second point of view an intensional semantics for proofs is presented which allows us effectively to compute quantitative stabilisation bounds. We discuss the application of the theory to the timing analysis of combinational circuits. To test our ideas we have implemented an experimental prototype tool and run several examples. [ABSTRACT FROM AUTHOR]

We present a formal model for concurrent systems. The model represents synchronous and asynchronous components in a uniform framework that supports compositional (assume-guarantee) and hierarchical (stepwise-refinement) design and verification. While synchronous models are based on a notion of atomic computation step, and asynchronous models remove that notion by introducing stuttering, our model is based on a flexible notion of what constitutes a computation step: by applying an abstraction operator to a system, arbitrarily many consecutive steps can be collapsed into a single step. The abstraction operator, which may turn an asynchronous system into a synchronous one, allows us to describe systems at various levels of temporal detail. For describing systems at various levels of spatial detail, we use a hiding operator that may turn a synchronous system into an asynchronous one. We illustrate the model with diverse examples from synchronous circuits, asynchronous shared-memory programs, and synchronous message-passing protocols. [ABSTRACT FROM AUTHOR]

An extension to the Murϕ verifier is presented to verify systems with replicated identical components. Although most systems are finite-state in nature, many of them are also designed to be scalable, so that a description gives a family of systems, each member of which has a different number of replicated components. It is therefore desirable to be able to verify the entire family of systems, independent of the exact number of replicated components. The verification is performed by explicit state enumeration in an abstract state space where states do not record the exact numbers of components. We provide an extension to the existing Murϕ language, by which a designer can easily specify a system in its concrete form. Through a new datatype, called RepetitiveID, a designer can suggest the use of this abstraction to verify a family of systems. First of all, Murϕ automatically checks the soundness of this abstraction. Then it automatically translates the system description to an abstract state graph for a system of a fixed size. During the verification of the system of a fixed size, Murϕ uses a simple run-time check to determine if the result can be generalized for a family of systems with sizes larger than the original system, including the system with an unbounded number of components. [ABSTRACT FROM AUTHOR]

Formal proofs generated by mechanised theorem proving systems may consist of a large number of inferences. As these theorem proving systems are usually very complex, it is extremely difficult if not impossible to formally verify them. This calls for an independent means of ensuring the consistency of mechanically generated proofs. This paper describes a method of recording HOL proofs in terms of a sequence of applications of inference rules. The recorded proofs can then be checked by an independent proof checker. Also described in this paper is an implementation of a proof checker which is able to check a practical proof consisting of thousands of inference steps. [ABSTRACT FROM AUTHOR]

Formal verification of computer-based engineering systems is only meaningful if the mathematical models used are derived systematically, recording the assumptions made at each modelling stage. In this paper we give an exposition of research efforts in cooperation with aerospace industries in Sweden. We emphasize the need for modelling techniques and languages covering the whole spectrum from informal engineering documents, to hybrid mathematical models. In this modelling process we give as much weight to the physical environment as to the controlling software. In particular, we report on our experience using switched bond graphs for the modelling of hardware components in hybrid systems. We present the basic ideas underlying bond graphs and illustrate the approach by modelling an aircraft landing gear system. This system consists of actuating hydromechanic and electromechanic hardware, as well as controlling components implemented in software and electronics. We present a detailed analysis of the closed loop system with respect to safety and timeliness properties. The proofs are carried out within the proof system of Extended Duration Calculus. [ABSTRACT FROM AUTHOR]

We present a rigorous mathematical proof of the correctness of the floating point square root instruction of the AMD K5 microprocessor. The instruction is represented as a program in a formal language that was designed for this purpose, based on the K5 microcode and the architecture of its FPU. We prove a statement of its correctness that corresponds directly with the IEEE Standard. We also derive an equivalent formulation, expressed in terms of rational arithmetic, which has been encoded as a formula in the ACL2 logic and mechanically verified with the ACL2 prover. Finally, we describe a microcode modification that was implemented as a result of this analysis in order to ensure the correctness of the instruction. [ABSTRACT FROM AUTHOR]

Proving the equivalence of two Finite State Machines (FSMs) has many applications to synthesis, verification, testing, and diagnosis. Building their product machine is a theoretical framework for equivalence proof. There are some cases where product machine traversal, a necessary and sufficient check, is mandatory. This is much more complex than traversing just one of the component machines. This paper proposes an equivalence-preserving function that transforms the product machine in the General Product Machine (GPM). Using the GPM in symbolic state space traversal reduces the size of the BDDs and makes image computation easier. As a result, GPM traversal is much less expensive than product machine traversal, its cost being close to dealing with a single machine. [ABSTRACT FROM AUTHOR]

A methodology for mechanically verifying generic adder circuits is proposed using the rewrite-rule based theorem prover Rewrite Rule Laboratory ( RRL). Proofs of properties of adder circuit descriptions are done by rewriting and induction. Carry lookahead adder circuit is described using powerlists, a data structure introduced by Misra to support divide-and-conquer strategy used for designing data-parallel algorithms. This description uses an algorithm for parallel prefix computation on powerlists due to Adams. Reasoning about properties of this algorithm can be of independent interest since parallel prefix operator has been found useful in many data-parallel algorithms. The correctness of the carry-lookahead adder (i.e., the adder indeed implements addition on numbers) is established by showing its equivalence to a recursive description of the ripple-carry adder, which is shown to correctly implement addition on natural numbers. The ripple carry adde r circuit is described in two different but equivalent ways: using powerlists employing the divide-and-conquer strategy, as well as using linear lists employing the linear decomposition strategy. The description of the ripple carry adder using powerlists is useful for showing equivalence of its input-output behavior to that of carry lookahead adder, whereas the description using linear lists is useful for showing its correctness with respect to addition on natural numbers. Descriptions of adder circuits using powerlists are based on Adams' work who also gave a hand proof of their correctness using the powerlist algebra. The emphasis in this paper is to generate proofs mechanically by a theorem prover . RRL exploits the algebraic laws of the powerlist algebra as rewrite rules, and uses heuristics for mechanizing proofs by induction using the cover set method to generate such proofs. The regularity in hardware circuits gets refl ected in compact descriptions generated using the divide-and-conquer strategy as well as in mechanically generated proofs by induction. Mechanical proofs generated by RRL closely follow the well-crafted hand-proofs which is quite encouraging. A comparison with Adams' hand generated proof is also made. There is strong evidence that the proposed methodology for generating proofs should scale up for large circuits exhibiting regularity that can be described using divide-and-conquer strategy in terms of powerlists. [ABSTRACT FROM AUTHOR]

We present a verification algorithm for duration properties of real-time systems. While simple real-time properties constrain the total elapsed time between events, duration properties constrain the accumulated satisfaction time of state predicates. We formalize the concept of durations by introducing duration measures for timed automata. A duration measure assigns to each finite run of a timed automaton a real number —the duration of the run— which may be the accumulated satisfaction time of a state predicate along the run. Given a timed automaton with a duration measure, an initial and a final state, and an arithmetic constraint, the duration-bounded reachability problem asks if there is a run of the automaton from the initial state to the final state such that the duration of the run satisfies the constraint. Our main result is an (optimal) PSPACE decision procedure for the duration-bounded reachability problem. [ABSTRACT FROM AUTHOR]

Modeling distributed computer systems is known to be a challenging enterprise. Typically, distributed systems are comprised of large numbers of components whose coordination may require complex interactions. Modeling such systems more often than not leads to the nominal intractability of the resulting state space. Various formal methods have been proposed to address the modeling of coordination among distributed systems components. For the most part, however, these methods do not support formal verification mechanisms. By way of contrast, the L-automata/L-processes model supports formal verification mechanisms which in many examples can successfully circumvent state space explosion problems, and allow verification proofs to be extended to an arbitrary number of components. After reviewing L-automata/L-processes formalisms, we present here the formal specification of a fault-tolerant algorithm for a distributed computer system. We also expose the L-automata/L-processes verification of the distributed system, demonstrating how various techniques such as homomorphic reduction, induction, and linearization, can be used to overcome various problems which surface as one models large, complex systems. [ABSTRACT FROM AUTHOR]