Abstract A fundamental method of analyzing a system such as a program or a circuit is invariance analysis, in which one proves that an assertion holds on all reachable states. Typically, the proof is performed via induction; however, an assertion, while invariant, may not be inductive (provable via induction). Invariant generation procedures construct auxiliary inductive assertions for strengthening the assertion to be inductive. We describe a general method of generating invariants that is incremental and property-directed. Rather than generating one large auxiliary inductive assertion, our method generates many simple assertions, each of which is inductive relative to those generated before it. Incremental generation is amenable to parallelization. Our method is also property-directed in that it generates inductive assertions that are relevant for strengthening the given assertion. We describe two instances of our method: a procedure for generating clausal invariants of finite-state systems and a procedure for generating affine inequalities of numerical infinite-state systems. We provide evidence that our method scales to checking safety properties of some large finite-state systems.

Abstract Alternating systems are models of computer programs whose behavior is governed by the actions of multiple agents with, potentially, different goals. Examples include control systems, resource schedulers, security protocols, auctions and election mechanisms. Proving properties about such systems has emerged as an important new area of study in formal verification, with the development of logical frameworks such as the alternating temporal logic ATL *. Techniques for model checking ATL * over finite-state systems have been well studied, but many important systems are infinite-state and thus their verification requires, either explicitly or implicitly, some form of deductive reasoning. This paper presents a theoretical framework for the analysis of alternating infinite-state systems. It describes models of computation, of various degrees of generality, and alternating-time logics such as ATL * and its variations. It then develops a proof system that allows to prove arbitrary ATL * properties over these infinite-state models. The proof system is shown to be complete relative to validities in the weakest possible assertion language. The paper then derives auxiliary proof rules and verification diagrams techniques and applies them to security protocols, deriving a new formal proof of fairness of a multi-party contract signing protocol where the model of the protocol and of the properties contains both game-theoretic and infinite-state (parameterized) aspects.

Scaling verification to large circuits requires some form of abstraction relative to the asserted property. We describe a safety analysis of finite-state systems that generalizes from counterexamples to the inductiveness of the safety specification to inductive invariants. It thus abstracts the system's state space relative to the property. The analysis either strengthens a safety specification to be inductive or discovers a counterexample to its correctness. The analysis is easily made parallel. We provide experimental data showing how the analysis time decreases with the number of processes on several hard problems.

General solutions to deadlock avoidance in distributed systems are considered impractical due to the high communication overhead. In previous work we showed that practical solutions exist when all possible sequences of resource requests are known a priori in the form of call graphs; in this case protocols can be constructed that involve no communication. These run-time protocols make use of annotations of the call graph that are computed statically based on the structure of the call graph. If the annotations are acyclic, then deadlocks are unreachable. This paper focuses on the computation of these annotations. We first show that our algorithm for computing acyclic annotations is complete: every optimal annotation can be generated. We then show that, given a cyclic annotation and a fixed set of resources, checking whether deadlocks are reachable is NP-complete. Finally, we consider the problem of computing minimal annotations that satisfy given constraints on the number of available resources. We show that the problem is NP-complete in the general case, but that it can be solved in polynomial time if the only restrictions are that the number of certain resources is 1, that is, these resources are binary semaphores.

We present a deadlock avoidance algorithm for distributed systems that guarantees liveness. Deadlock avoidance in distributed systems is a hard problem and general solutions are considered impractical due to the high communication overhead. In previous work, however, we showed that practical solutions exist when all possible sequences of resource requests are known a priori in the form of call graphs; in this case protocols can be constructed that perform safe resource allocation based on local data only, that is, no communication between components is required. While avoiding deadlock, those protocols, however, did not avoid starvation: they guaranteed that some process could always make progress, but did not guarantee that every individual process would always eventually terminate. In this paper we present a resource allocation mechanism that avoids deadlock and guarantees absence of starvation, without undue loss of concurrency. The only assumption we make is that the local scheduler is fair. We prove the correctness of the algorithm and show how it can be implemented efficiently.

Thread allocation is an important problem in distributed real-time and embedded (DRE) systems. A thread allocation policy that is too liberal may cause deadlock, while a policy that is too conservative limits potential parallelism, thus wasting resources. However, achieving (globally) optimal thread utilization, while avoiding deadlock, has been proven impractical in distributed systems: it requires too much communication between components. In previous work we showed that efficient local thread allocation protocols are possible if the protocols are parameterized by global static data, in particular by an annotation of the global call graph of all tasks to be performed by the system. We proved that absence of cyclic dependencies in this annotation guarantees absence of deadlock. In this paper we present an algorithm to compute optimal annotations, that is annotations that maximize parallelism while satisfying the condition of acyclicity. Moreover, we show that the condition of acyclicity is in fact tight and exhibits a rather surprising anomaly: if a cyclic dependency is present in the annotation of the call graph and a certain minimum number of threads is provided, deadlock is reachable. Thus, in the presence of cyclic dependencies, increasing the number of threads may introduce the possibility of deadlock in an originally deadlock free system.

We present a specification language and algorithms for the online and offline monitoring of synchronous systems including circuits and embedded systems. Such monitoring is useful not only for testing, but also under actual deployment. The specification language is simple and expressive; it can describe both correctness/failure assertions along with interesting statistical measures that are useful for system profiling and coverage analysis. The algorithm for online monitoring of queries in this language follows a partial evaluation strategy: it incrementally constructs output streams from input streams, while maintaining a store of partially evaluated expressions for forward references. We identify a class of specifications, characterized syntactically, for which the algorithm's memory requirement is independent of the length of the input streams. Being able to bound memory requirements is especially important in online monitoring of large input streams. We extend the concepts used in the online algorithm to construct an efficient offline monitoring algorithm for large traces. We have implemented our algorithm and applied it to two industrial systems, the PCI bus protocol and a memory controller. The results demonstrate that our algorithms are practical and that our specification language is sufficiently expressive to handle specifications of interest to industry.

We present a new technique for the generation of non-linear (algebraic) invariants of a program. Our technique uses the theory of ideals over polynomial rings to reduce the non-linear invariant generation problem to a numerical constraint solving problem. So far, the literature on invariant generation has been focussed on the construction of linear invariants for linear programs. Consequently, there has been little progress toward non-linear invariant generation. In this paper, we demonstrate a technique that encodes the conditions for a given template assertion being an invariant into a set of constraints, such that all the solutions to these constraints correspond to non-linear (algebraic) loop invariants of the program. We discuss some trade-offs between the completeness of the technique and the tractability of the constraint-solving problem generated. The application of the technique is demonstrated on a few examples.

Abstract. STeP, the Stanford Temporal Prover, supports the computer-aided formal verification of concurrent and reactive systems based on temporal specifications [MBB99]. Automated model checking is combined with computer-aided deductive methods to allow for the verification of a broad class of systems, including parameterised ( N -component) circuit designs, parameterised ( N -process) programs, and programs with infinite data domains.

Verifying temporal specifications of reactive and concurrent systems commonly relies on generating auxiliary assertions and on strengthening given properties of the system. This can be achieved by two dual approaches: The bottom-up method performs an abstract forward propagation (computation) of the system, generating auxiliary assertions; the top-down method performs an abstract backward propagation to strengthen given properties. Exact application of these methods is complete but is usually infeasible for large-scale verification. Approximation techniques are often needed to complete the verification. We give an overview of known methods for generation of auxiliary invariants in the verification of invariance properties. We extend these methods, by formalizing and analyzing a general verification rule that uses assertion graphs to generate auxiliary assertions for the verification of general safety properties.

Presents a compositional proof system for the verification of real-time systems. Real-time systems are modeled as timed transition modules, which explicitly model interaction with the environment and may be combined using composition operators. Composition rules are devised such that the correctness of a system may be determined from the correctness of its components. These proof rules are demonstrated on Fischer's mutual exclusion algorithm, for which mutual exclusion and bounded response are proven.>

We extend the specification language of temporal logic, the corresponding verification framework, and the underlying computational model to deal with real-;time properties of reactive systems. The abstract notion of timed transition systems generalizes traditional transition systems conservatively: qualitative fairness requirements are replaced (and superseded) by quantitative lower-bound and upper-bound timing constraints on transitions. This framework can model real-time systems that communicate either through shared variables or by message passing and real-time issues such as timeouts, process priorities (interrupts), and process scheduling. We exhibit two styles for the specification of real-time systems. While the first approach uses time-bounded versions of the temporal operators, the second approach allows explicit references to time through a special clock variable. Corresponding to the two styles of specification, we present and compare two different proof methodologies for the verification of timing requirements that are expressed in these styles. For the bounded-operator style, we provide a set of proof rules for establishing bounded-invariance and bounded-responce properties of timed transition systems. This approach generalizes the standard temporal proof rules for verifying invariance and response properties conservatively. For the explicit-clock style, we exploit the observation that every time-bounded property is a safety property and use the standard temporal proof rules for establishing safety properties.

An informal tutorial for program synthesis is presented, with an emphasis on deductive methods. According to this approach, to construct a program meeting a given specification, the authors prove the existence of an object meeting the specified conditions. The proof is restricted to be sufficiently constructive, in the sense that, in establishing the existence of the desired output, the proof is forced to indicate a computational method for finding it. That method becomes the basis for a program that can be extracted from the proof. The exposition is based on the deductive-tableau system, a theorem-proving framework particularly suitable for program synthesis. The system includes a nonclausal resolution rule, facilities for reasoning about equality, and a well-founded induction rule.>

. We extend the specification language of temporal logic, the corresponding verification framework, and the underlying computational model to deal with real-time properties of concurrent and reactive systems. A global, discrete, and asynchronous clock is incorporated into the model by defining the abstract notion of a real-time transition system as a conservative extension of traditional transition systems: qualitative fairness requirements are replaced (and superseded) by quantitative lower-bound and upperbound real-time requirements for transitions. We show how to model real-time systems that communicate either through shared variables or by message passing, and how to represent the important real-time constructs of priorities (interrupts), scheduling, and timeouts in this framework. Two styles for the specification of real-time properties are presented. The first style uses bounded versions of the temporal operators; the real-time requirements expressed in this style are classified ...

We propose a classification of temporal properties into a hierarchy.The classes of the hierarchy are characterized through four views: a language-theoretic view, a topologica1 view, the temporal logic view, and an automata view.In the topological view, the considered hierarchy coincides with the two lower levels of the Bore1 hierarchy, starting with the closed and open sets.For properties that are expressible by temporal logic and predicate automata, we provide a syntactic characterization of the formulae and automata that specify properties in the different classes.We relate this classification to the well known safety-[iweness classification, and show that in some sense the two are orthogonal to one another.

This paper presents a proof system for first-order temporal logic. The system extends the nonclausal resolution method for ordinary first-order logic with equality, to handle quantifiers and temporal operators. Soundness and completeness issues are considered. The use of the system for verifying concurrent programs is discussed and variants of the system for other modal logics are also described.

Temporal logic, often used as a specification language for programs, can serve directly as a programming language. We propose a specific programming language TEMPLOG, which extends the classical PROLOG-like languages to include temporal operators. PROLOG progams are collections of classical Horn clauses and they are efficiently interpreted by SLD-resolution. Similarly, TEMPLOG programs are collections of temporal Horn clauses and we interpret them with temporal SLD-resolution, a restricted form of a general temporal resolution method.

We propose a classification of temporal properties into a hierarchy which refines the known safety-liveness classification of properties. The new classification recognizes the classes of safety, guarantee, persistence, fairness, and hyper-fairness. The classification suggested here is based on the different ways a property of finite computations can be extended into a property of infinite computations. For properties that are expressible by temporal logic and predicate automata, we provide a syntactic characterization of the formulae and automata that specify properties in the different classes. We consider the verification of properties over a given program, and provide a unique proof principle for each class.

∀-automata are non-deterministic finite-state automata over infinite sequences. They differ from conventional automata in that a sequence is accepted if all runs of the automaton over the sequence are accepting. These automata are suggested as a formalism for the specification and verification of temporal properties of concurrent programs. It is shown that they are as expressive as extended-temporal-logic (ETL), and in some cases provide a more compact representation of properties than temporal logic. A structured diagram notation is suggested for the graphical representation of these automata. A single sound and complete proof rule is presented for proving that all computations of a program have the property specified by a ∀-automaton.

Two deduction rules are introduced to give streamlined treatment to relations of special importance in an automated theorem-proving system. These rules, the relation replacement and relation matching rules, generalize to an arbitrary binary relation the paramodulation and E-resolution rules, respectively, for equality, and may operate within a nonclausal or clausal system. The new rules depend on an extension of the notion of polarity to apply to subterms as well as to subsentences, with respect to a given binary relation. The rules allow us to eliminate troublesome axioms, such as transitivity and monotonicity, from the system; proofs are shorter and more comprehensible, and the search space is correspondingly deflated.

In this paper, Propositional Temporal Logic (PTL) is applied to the specification and synthesis of the synchronization part of communicating processes.To specify a process, a PTL formula that describes its sequence of communications is given.The synthesis is done by constructing a model of the given specifications using a tableau-like satisfiability algorithm for PTL.This model can then be interpreted as a program.

An abstract temporal proof system is presented whose program-dependent part has a high-level interface with the programming language actually studied. Given a new language, it is sufficient to deline the interface notions of atomic transitions, justice, and fairness in order to obtain a full temporal proof system for this language. This construction is particularly useful for the analysis of concurrent systems. We illustrate the construction on the shared-variable model and on CSP. The generic proof system is shown to be relatively complete with respect to pure first-order temporal logic.

A temporal language and system are presented which are based on branching time structure. By the introduction of symmetrically dual sets of temporal operators, it is possible to discuss properties which hold either along one path or along all paths. Consequently it is possible to express in this system all the properties that were previously expressible in linear time or branching time systems. We present an exponential decision procedure for satisfiability in the language based on tableaux methods, and a complete deduction system. As associated temporal semantics is illustrated for both structured and graph representation of programs.

Methods are presented whereby an Algol-like program given together with its specifications can be documented automatically. The program is incrementaly annotated with invariant relations that hold between program variables at intermediate points in the program text and explain the actual workings of the program regardless of whether it is correct. Thus, this documentation can be used for proving correctness of programs or may serve as an aid in debugging incorrect programs.

A class of schemes called synchronous schemes is defined. A synchronous scheme can have several variables, but all the active ones are required to keep a synchronized rate of computation as measured by the height of their respective Herbrand values. A "reset" statement, which causes all the variables to restart a new computation, is admitted. It is shown that equivalence, convergence, and other properties are decidable for schemes in this class. The class of synchronous schemes contains, as special cases, the known decidable classes of Ianov schemes, one-variable schemes with resets, and progressive schemes.

Program synthesis is the systematic derivation of a program from a given specification. A deductive approach to program synthesis is presented for the construction of recursive programs. This approach regards program synthesis as a theorem-proving task and relies on a theorem-proving method that combines the features of transformation rules, unification, and mathematical induction within a single framework.

Deductive techniques are presented for deriving programs systematically from given specifications. The specifications express the purpose of the desired program without giving any hint of the algorithm to be employed. The basic approach is to transform the specifications repeatedly according to certain rules, until a satisfactory program is produced. The rules are guided by a number of strategic controls. These techniques have been incorporated in a running program-synthesis system, called DEDALUS.

Techniques derived from mathematical logic promise to provide an alternative to the conventional methodology for constructing, debugging, and optimizing computer programs. Ultimately, these techniques are intended to lead to the automation of many of the facets of the programming process.

An attempt is made to formulate techniques of program modification, whereby a given program that achieves one goal can be transformed into a new program that uses the same principles to achieve a different goal. For example, a program that uses the binary search paradigm to calculate the square root of a number may be modified to divide two numbers in a similar manner, or vice versa. The essence of the approach is to find an analogy between the specifications of the given and desired programs, and then to transform the given program accordingly.

In this paper we define a new type of fixedpoint of recursive definitions and investigate some of its properties. This optimal fixedpoint (which always uniquely exists) contains, in some sense, the maximal amount of “interesting” information which can be extracted from the recursive definition, and it may be strictly more defined than the program’s least fixedpoint. This fixedpoint can be the basis for assigning a new semantics to recursive programs.

In this paper a new fixedpoint approach towards the semantics of recursive programs is presented. The fixedpoint defined by a recursive program under this semantics contains, in some sense, the maximal amount of “interesting” information which can be extracted from the program. This optimal fixedpoint (which always uniquely exists) may be strictly more defined than the program's least fixedpoint. We consider both the theoretical and the computational aspects of the approach, as well as some techniques for proving properties of the optimal fixedpoint of a given recursive program.

While-schemas are defined as program schemas without goto statements, in which iteration is achieved using while statements. We present two translations of program schemas into equivalent while-schemas, the first one by adding extra program variables, and the second one by adding extra logical variables. In both cases we aim to preserve as much of the structure of the original program schemas as possible. We also show that, in general, any translation must add variables.

A class of (monadic) functional schemas which properly includes “Ianov” flowchart schemas is defined. It is shown that the termination, divergence, and freedom problems for functional schemas are decidable. Although it is possible to translate a large class of non-free functional schemas into equivalent free functional schemas, it is shown that in general this cannot be done. It is also shown that the equivalence problem for free functional schemas is decidable. Most of the results are obtained from well-known results in formal languages and automata theory.

We discuss the class of program schemas augmented with equality tests, that is, tests of equality between terms.

In this work we show that it is possible to formalize all properties regularly observed in (deterministic and non-deterministic) algorithms in second-order predicate calculus. Moreover, we show that for any given algorithm it suffices to know how to formalize its 'partial correctness' by a second-order formula in order to formalize all other properties by second-order formulas. This result is of special interest since 'partial correctness' has already been formalized in second-order predicate calculus for many classes of algorithms.

The problems of convergence, correctness, and equivalence of computer programs can be formulated by means of the satisfiability or validity of certain first-order formulas. An algorithm is presented for constructing such formulas for functional programs, i.e. programs defined by LISP-like conditional recursive expressions.

This paper is concerned with the relationship between the convergence, correctness and equivalence of recursively defined functions and the satisfiability (or unsatisfiability) of certain first-order formulas.

This paper is concerned with the relationship of the termination problem for programs and abstract programs to the validity of certain formulas in the first-order predicate calculus. By exploiting this relationship, subclasses of abstract programs for which the termination problem is decidable can be isolated. Moreover, known proof procedures for the first-order predicate calculus (e.g. resolution) can be applied to prove the termination of both programs and abstract programs. The correctness and equivalence problems of abstract programs are shown to be reducible to the termination problem.