Search

We present a semantics for architectural specifications in the Common Algebraic Specification Language (Casl), including an extended static analysis compatible with model-theoretic requirements. The main obstacle here is the lack of amalgamation for Casl models. To circumvent this problem, we extend the Casl logic by introducing enriched signatures, where subsort embeddings form a category rather than just a preorder. The extended model functor satisfies the amalgamation property as well as its converse, which makes it possible to express the amalgamability conditions in the semantic rules in static terms. Using these concepts, we develop the semantics at various levels in an institution-independent fashion. Moreover, amalgamation for enriched Casl means that a variety of results for institutions with amalgamation, such as computation of normal forms and theorem proving for structured specifications, can now be used for Casl.

Primitives are basic means provided by a microkernel to implementors of operating system services. Intensively used within every OS and commonly implemented in a mixture of high-level and assembly programming languages, primitives are meaningful and challenging candidates for formal verification. We report on the accomplished correctness proof of academic microkernel primitives. We describe how a novel approach to verification of programs written in C with inline assembler is successfully applied to a piece of realistic system software. Necessary and sufficient criteria covering functional correctness and requirements for the integration into a formal model of memory virtualization are determined and formally proven. The presented results are important milestones on the way to a pervasively verified operating system.

Circus specifications define both data and behavioural aspects of systems using a combination of Z and CSP. Previously, a denotational semantics has been given to Circus; however, as a shallow embedding of Circus in Z, it was not possible to use it to prove properties like the refinement laws that justify the distinguishing development technique associated with Circus. This work presents a final reference for the Circus denotational semantics based on Hoare and He's Unifying Theories of Programming (UTP). Finally, it discusses the library of theorems on the UTP that was created and used in the proofs of the refinement laws.

Maude's language design and implementation make systematic use of the fact that rewriting logic is reflective. This makes the metatheory of rewriting logic accessible to the user in a clear and principled way, and makes possible many advanced metaprogramming applications, including user-definable strategy languages, language extensions by new module composition operations, development of theorem proving tools, and reifications of other languages and logics within rewriting logic. A naive implementation of reflection can be computationally very expensive. We explain the semantic principles and implementation techniques through which efficient ways of performing reflective computations are achieved in Maude through its predefined META-LEVEL module. We are indebted to Jose F. Quesada for his excellent work on the MSCP context-free parser for Maude, that---besides being used for different parsing functions in Maude---is used as a key component of the built-in function meta-parse in META-LEVEL. We cordially thank Carolyn Talcott for many discussions on metalevel issues that have contributed to the development of our ideas.

We present a tool-supported framework for proving that the composition of the behaviors of the separate parts of a complex system ensures a desired global property of the overall system. A compositional inference rule is formally introduced and encoded in the logic of the PVS theorem prover. Methodological considerations on the usage of the inference rule are presented, and the framework is then used to prove a meaningful property of a simple, but significant, control system.

Circus is a refinement language in which specifications define both data and behavioural aspects of concurrent systems using a combination of Z and CSP. Its refinement theory and calculus are distinctive, but since refinements may be long and repetitive, the practical application of this technique can be hard. Useful strategies have been identified, described, and used, and by documenting them as tactics, they can be expressed and repeatedly applied as single transformation rules. Here, we present ArcAngelC, a language for defining such tactics; we present the language, its semantics, and its application in the formalisation of an existing strategy for verification of Ada implementations of control systems specified by Simulink diagrams. We also discuss its mechanisation in a theorem prover, ProofPower-Z.

This paper is a greatly expanded version of a talk I gave in April 2009 at KunenFest. It describes Ken's work in algebra, particularly using automated deduction tools., Comment: 7 pages, to appear in a special issue of Topology and its Applications in honor of Ken Kunen

We describe a tool that combines a general purpose theorem prover and an ofi-theshelf interface for dynamic geometry drawing to enhance man-machine interaction involving geometrical proofs. With our tool, we can edit the statements of geometrical theorems, construct and verify their proofs with the theorem prover, and visualize the statements using the drawing tool. The key component is an algorithm that computes the data needed to draw a construction from the formal statement of the theorem. The paper includes some examples of output from our combined tool, called GeoView.

SOL (Secure Operations Language) is a synchronous programming language for implementing reactive systems. The utility of SOL hinges upon the fact that it is a secure language, i.e., most programs in SOL are amenable to fully automated static analysis techniques, such as automatic theorem proving using decision procedures or model checking. Among the unique features of SOL is the ability to express a wide class of enforceable safety and security policies (including the temporal aspects of software component interfaces) in the language itself, thereby opening up the possibility of eliminating runaway computations and malicious code, such as worms and viruses.

This paper presents some techniques which bound the proof search space in propositional intuitionistic logic. These techniques are justified by Kripke semantics and are the backbone of a tableau based theorem prover (PITP) implemented in C++. PITP and some known theorem provers are compared using the formulas of ILTP benchmark library. It turns out that PITP is, at the moment, the propositional prover that solves most formulas of the library.

We report on an experiment in combining the theorem prover Isabelle with automatic first-order arithmetic provers to increase automation on the verification of distributed protocols. As a case study for the experiment we verify several averaging clock synchronization algorithms. We present a formalization of Schneider's generalized clock synchronization protocol [Schneider, F. B., Understanding protocols for Byzantine clock synchronization, Technical Report TR 87–859, Cornell University (1987). URL citeseer.ist.psu.edu/schneider87understanding.html] in Isabelle/HOL. Then, we verify that the convergence functions used in two clock synchronization algorithms, namely, the Interactive Convergence Algorithm (ICA) of Lamport and Melliar-Smith [Lamport, L. and P. M. Melliar-Smith, Synchronizing clocks in the presence of faults, J. ACM 32 (1985), pp. 52–78] and the Fault-tolerant Midpoint algorithm of Lundelius-Lynch [Lundelius, J. and N. Lynch, A new fault-tolerant algorithm for clock synchronization, in: Proceedings of PODC '84 (1984), pp. 75–88], satisfy Schneider's general conditions for correctness. The proofs are completely formalized in Isabelle/HOL. We identify the parts of the proofs which are not fully automatically proven by Isabelle built-in tactics and show that these proofs can be handled by automatic first-order provers with support for arithmetic like ICS and CVC Lite.

This position paper discusses various issues concerning requirements and design of proof assistant user interfaces (UIs). After a review of some of the diculties faced by UI projects in academia, it presents a high-level description of proof assistant interaction. This is followed by an exposition of use cases and object identification. Several examples demonstrate the usefulness of these requirement elicitation techniques in the theorem proving domain. The second half of the paper begins with a consideration of the “principle of least eort” for the design of theorem prover user interfaces. This is followed by a brief review of the “GUI versus text mode” debate, proposals for better use of GUI facilities and a plea for better support of customisation. The paper ends with a discussion of architecture and system design issues. In particular, it argues for a platform architecture with an extensible set of components and the use of XML protocols for communication between UIs and proof assistant backends.

SystemC is among a group of system level design languages proposed to raise the abstraction level for embedded system design and verification. A straight and sound verification by model checking or theorem proving of SystemC designs is, however, infeasible given the object-oriented nature of this library and the complexity of its simulation environment. We illustrated, in a previous work, the feasibility and success of performing model checking and assertions monitors generation of SystemC using a variant of Abstract State Machines (ASM) languages (AsmL). In this paper, we establish the soundness of our approach by proving the correctness of the transformation from SystemC to AsmL.

We describe novel computational techniques for constructing induction rules for deductive synthesis proofs. Deductive synthesis holds out the promise of automated construction of correct computer programs from specifications of their desired behaviour. Synthesis of programs with iteration or recursion requires inductive proof, but standard techniques for the construction of appropriate induction rules are restricted to recycling the recursive structure of the specifications. What is needed is induction rule construction techniques that can introduce novel recursive structures. We show that a combination of rippling and the use of meta-variables as a least-commitment device can provide such novelty.

ArcAngel is a specialised tactic language devised to facilitate and automate program developments using Morgan's refinement calculus. It is especially well-suited for the specification of high-level strategies to derive programs by construction, and equipped with a formal semantics that enables reasoning about tactics. In this paper, we present an implementation of ArcAngel for the ProofPower theorem prover. We discuss the underlying design, explain how it implements the semantics of ArcAngel, and examine differences in expressiveness and flexibility in comparison to ProofPower's in-built tactic language. ArcAngel supports backtracking through angelic choice; this is beyond the basic capabilities of ProofPower and many other main-stream theorem provers. The implementation is demonstrated with a non-trivial tactic example.

ACL2 is the latest inception of the Boyer-Moore theorem prover, the 2005 recipient of the ACM Software System Award. In the hands of experts it feels like a finely tuned race car, and it has been used to prove some of the most complex theorems ever proved about commercially designed systems. Unfortunately, ACL2 has a steep learning curve. Thus, novices tend have a very different experience: they crash and burn. As part of a project to make ACL2 and formal reasoning safe for the masses, we have developed ACL2s, the ACL2 sedan. ACL2s includes many features for streamlining the learning process that are not found in ACL2. In general, the goal is to develop a tool that is “self-teaching,” i.e., it should be possible for an undergraduate to sit down and play with it and learn how to program in ACL2 and how to reason about the programs she writes.

Eternity variables are introduced to specify and verify serializability of transactions of a distributed database. Eternity variables are a new kind of auxiliary variables. They do not occur in the implementation but are used in specification and verification. Elsewhere it has been proved that eternity variables in combination with history variables are semantically complete for proving refinement relations.An eternity variable can be thought of as an unknown constant that is determined by the behaviour (execution sequence). In the specification of the database, one eternity variable is used to enforce serialization. In the verification, an additional eternity variable is needed for the connection of the local data with the shared database.The formalism is based on linear-time temporal logic, but the analysis of behaviours is completely reduced to the next-state relation together with progress arguments using variant functions. Forward invariants (inductive predicates) are complemented with other, so-called backward, invariants. The proof has been verified with the first-order theorem prover NQTHM to give additional confidence in the result and in the feasibility of the approach.

This paper presents work in the context of the certification of a safety component for autonomous service robots, and investigates the potential advantages offered by formally modelling the domain knowledge, specification and implementation in a theorem prover in higher-order logic. This allows safety properties to be stated in an abstract manner close to textbook mathematics. The automatic proof checking alleviates correctness concerns, and provides a seamless development process from high-level safety requirements down to concrete implementation. Moreover, the formalisation can be checked for correctness automatically, and the certification review process can focus on the correctness of the specification and safety cases.

Lock-freedom is a property of concurrent programs which states that, from any state of the program, eventually some process will complete its operation. Lock-freedom is a weaker property than the usual expectation that eventually all processes will complete their operations. By weakening their completion guarantees, lock-free programs increase the potential for parallelism, and hence make more efficient use of multiprocessor architectures than lock-based algorithms. However, lock-free algorithms, and reasoning about them, are considerably more complex.In this paper we present a technique for proving that a program is lock-free. The technique is designed to be as general as possible and is guided by heuristics that simplify the proofs. We demonstrate our theory by proving lock-freedom of two non-trivial examples from the literature. The proofs have been machine-checked by the PVS theorem prover, and we have developed proof strategies to minimise user interaction.

Narrowing was originally introduced to solve equational E-unification problems. It has also been recognized as a key mechanism to unify functional and logic programming. In both cases, narrowing supports equational reasoning and assumes confluent equations. The main goal of this work is to show that narrowing can be greatly generalized, so as to support a much wider range of applications, when it is performed with rewrite theories (Σ, E, R), where (Σ, E) is an equational theory, and R is a collection of rewrite rules with no restrictions. Such theories axiomatize concurrent systems, whose states are equivalence classes of terms modulo E, and whose transitions are specified by R. In this context, narrowing is generalized from an equational reasoning technique to a symbolic model checking technique for reachability analysis of a, typically infinite, concurrent system. We survey the foundations of this approach, suitable narrowing strategies, and various applications to security protocol verification, theorem proving, and programming languages.

We present a generic congruence closure algorithm for deciding ground formulas in the combination of the theory of equality with uninterpreted symbols and an arbitrary built-in solvable theory X. Our algorithm CC(X) is reminiscent of Shostak combination: it maintains a union-find data-structure modulo X from which maximal information about implied equalities can be directly used for congruence closure. CC(X) diverges from Shostak's approach by the use of semantic values for class representatives instead of canonized terms. Using semantic values truly reflects the actual implementation of the decision procedure for X. It also enforces to entirely rebuild the algorithm since global canonization, which is at the heart of Shostak combination, is no longer feasible with semantic values. CC(X) has been implemented in Ocaml and is at the core of Ergo, a new automated theorem prover dedicated to program verification.

When combining logic level theorem proving with computational methods it is important to identify both functions that can be efficiently computed and the objects they can be applied to. This is generally achieved by mappings of logic level terms and functions to their computational counterparts. However, these mappings are often quite ad hoc and fragile depending very much on the particular logic representations of terms. We present a method of annotating terms in logic proofs with their computational properties. This enables the compact representation of computational objects in deduction systems as well as their connection to functions that can be easily computed for them. This eases the identification of deduction problems that can be treated efficiently by computational methods and also abstracts from trivial properties that are artefacts of a particular representation. We ensure logical correctness of our concepts by providing the possibility to replace terms by their logical representation and by expanding computational procedures by tactic application that can be rigorously checked.

In this article we first show how the functional and the optimized functional translation from modal logic to many-sorted first-order logic can be naturally extended to the hybrid language H(@,↓). The translation is correct not only when reasoning over the class of all models, but for any first-order definable class. We then show that sorts can be safely removed (i.e., without affecting the satisfiability status of the formula) for frame classes that can be defined in the basic modal language, and show a counterexample for a frame class defined using nominals.

In [P. Hancock, A. Setzer, Interactive programs in dependent type theory, in: P. Clote, H. Schwichtenberg (Eds.), Proc. 14th Annu. Conf. of EACSL, CSL’00, Fischbau, Germany, 21–26 August 2000, Vol. 1862, Springer, Berlin, 2000, pp. 317–331, URL 〈citeseer.ist.psu.edu/article/hancock00interactive.html〉; P. Hancock, A. Setzer, Interactive programs and weakly final coalgebras in dependent type theory, in: L. Crosilla, P. Schuster (Eds.), From Sets and Types to Topology and Analysis. Towards Practicable Foundations for Constructive Mathematics, Oxford Logic Guides, Clarendon Press, 2005, URL 〈www.cs.swan.ac.uk/∼csetzer/〉] Hancock and Setzer introduced rules to extend Martin-Löf's type theory in order to represent interactive programming. The rules essentially reflect the existence of weakly final coalgebras for a general form of polynomial functor. The standard rules of dependent type theory allow the definition of inductive types, which correspond to initial algebras. Coalgebraic types are not represented in a direct way. In this article we show the existence of final coalgebras in intensional type theory for these kind of functors, where we require uniqueness of identity proofs (UIP) for the set of states S and the set of commands C which determine the functor. We obtain the result by identifying programs which have essentially the same behaviour, viz. are bisimular. This proves the rules of Setzer and Hancock admissible in ordinary type theory, if we replace definitional equality by bisimulation. All proofs [M. Michelbrink, Verifications of final coalgebra theorem in: Interfaces as Functors, Programs as Coalgebras—A Final Coalgebra Theorem in Intensional Type Theory, 2005, URL 〈www.cs.swan.ac.uk/∼csmichel/〉] are verified in the theorem prover agda [C. Coquand, Agda, Internet, URL 〈www.cs.chalmers.se/∼catarina/agda/〉; K. Peterson, A programming system for type theory, Technical Report, S-412 96, Chalmers University of Technology, Göteborg, 1982], which is based on intensional Martin-Löf type theory.

We present an approach to mathematical assistants which uses readable, executable proof scripts as the central language for interaction. We examine an implementation that combines the Isar language, the Isabelle theorem prover and the IsaPlanner proof planner. We argue that this synergy provides a flexible environment for the exploration, certification, and presentation of mathematical proof.