Distilling Programs for Verification

In this paper, we show how our program transformation algorithm called distillation can not only be used for the optimisation of programs, but can also be used to facilitate program verification. Using the distillation algorithm, programs are transformed into a specialised form in which functions are tail recursive, and very few intermediate structures are created. We then show how properties of this specialised form of program can be easily verified by the application of inductive proof rules. We therefore argue that the distillation algorithm is an ideal candidate for inclusion within compilers as it facilitates the two goals of program optimization and verification.     

Deforestation, program transformation, and cut-elimination

The problem of proving that two programs, in any reasonable programming language, are equivalent is well-known to be undecidable. In a formal programming system, in which the rules for equivalence are finitely presented, the problem of provable equivalence is semi-decidable. Despite this improved situation there is a significant lack of generally accepted automated techniques for systematically searching for a proof (or disproof) of program equivalence. Techniques for searching for proofs of equivalence often stumble on the formulation of induction and, of course, coinduction (when it is present) which are often formulated in such a manner as to require inspired guesses.There are, however, well-known program transformation techniques which do address these issues. Of particular interest to this paper are the deforestation techniques introduced by Phil Wadler and the fold/unfold program transformation techniques introduced by Burstall and Darlington. These techniques are shadows of an underlying cut-elimination procedure and, as such, should be more generally recognized as proof techniques.In this paper we show that these techniques apply to languages which have both inductive and coinductive datatypes. The relationship between these program transformation techniques and cut-elimination requires a transformation from initial and final “algebra” proof rules into “circular” proof rules as introduced by Santocanale (and used implicitly in the model checking community). This transformation is only possible in certain proof systems. Here we show that it can be applied to cartesian closed categories with datatypes: closedness is an essential requirement. The cut-elimination theorems and attendant program transformation techniques presented here rely heavily on this alternate presentation of induction and coinduction.     

Property-directed incremental invariant generation

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.     

Recursive Program Optimization through Inductive Synthesis Proof Transformation

The research described in this paper involved developing transformation techniques that increase the efficiency of the original program, the source, by transforming its synthesis proof into one, the target, which yields a computationally more efficient algorithm. We describe a working proof transformation system that, by exploiting the duality between mathematical induction and recursion, employs the novel strategy of optimizing recursive programs by transforming inductive proofs. We compare and contrast this approach with the more traditional approaches to program transformation and highlight the benefits of proof transformation with regards to search, correctness, automatability, and generality.     

Evolutionary program induction directed by logic grammars

Program induction generates a computer program that can produce the desired behavior for a given set of situations. Two of the approaches in program induction are inductive logic programming (ILP) and genetic programming (GP). Since their formalisms are so different, these two approaches cannot be integrated easily, although they share many common goals and functionalities. A unification will greatly enhance their problem-solving power. Moreover, they are restricted in the computer languages in which programs can be induced. In this paper, we present a flexible system called LOGENPRO (The LOgic gramar-based GENetic PROgramming system) that uses some of the techniques of GP and ILP. It is based on a formalism of logic grammars. The system applies logic grammars to control the evolution of programs in various programming languages and represent context-sensitive information and domain-dependent knowledge. Experiments have been performed to demonstrate that LOGENPRO can emulate GP and GP with automatically defined functions (ADFs). Moreover, LOGENPRO can employ knowledge such as argument types in a unified framework. The experiments show that LOGENPRO has superior performance to that of GP and GP with ADFs when more domain-dependent knowledge is available. We have applied LOGENPRO to evolve general recursive functions for the even-n-parity problem from noisy training examples. A number of experiments have been performed to determine the impact of domain-specific knowledge and noise in training examples on the speed of learning.     

Aspects preserving properties

Aspect Oriented Programming can arbitrarily distort the semantics of programs. In particular, weaving can invalidate crucial safety and liveness properties of the base program. In this article, we identify categories of aspects that preserve some classes of properties. Specialized aspect languages are then designed to ensure that aspects belong to a specific category and, therefore, that woven programs will preserve the corresponding properties.Our categories of aspects, inspired by Katz’s, comprise observers, aborters, confiners and weak intruders. Observers introduce new instructions and a new local state but they do not modify the base program’s state and control-flow. Aborters are observers which may also abort executions. Confiners only ensure that executions remain in the reachable states of the base program. Weak intruders are confiners between two advice executions. These categories (along with two others) are defined formally based on a language independent abstract semantics framework. The classes of preserved properties are defined as subsets of LTL for deterministic programs and CTL* for non-deterministic ones. We can formally prove that, for any program, the weaving of any aspect in a category preserves any property in the related class.We present, for most aspect categories, a specialized aspect language which ensures that any aspect written in that language belongs to the corresponding category. It can be proved that these languages preserve the corresponding classes of properties by construction. The aspect languages share the same expressive pointcut language and are designed w.r.t. a common imperative base language.Each category and language is illustrated by simple examples. The appendix provides semantics and two instances of proofs: the proof of preservation of properties by a category and the proof that all aspects written in a language belong to the corresponding category.     

Constructing Induction Rules for Deductive Synthesis Proofs

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.     

On the Formalization of the Modal μ-Calculus in the Calculus of Inductive Constructions

We present a natural deduction proof system for the propositional modal μ-calculus and its formalization in the calculus of inductive constructions. We address several problematic issues, such as the use of higher-order abstract syntax in inductive sets in the presence of recursive constructors, and the formalization of modal (sequent-style) rules and of context sensitive grammars. The formalization can be used in the system Coq, providing an experimental computer-aided proof environment for the interactive development of error-free proofs in the modal μ-calculus. The techniques we adopt can be readily ported to other languages and proof systems featuring similar problematic issues.     

Conjecture Synthesis for Inductive Theories

We have developed a program for inductive theory formation, called IsaCoSy, which synthesises conjectures ‘bottom-up’ from the available constants and free variables. The synthesis process is made tractable by only generating irreducible terms, which are then filtered through counter-example checking and passed to the automatic inductive prover IsaPlanner. The main technical contribution is the presentation of a constraint mechanism for synthesis. As theorems are discovered, this generates additional constraints on the synthesis process. We evaluate IsaCoSy as a tool for automatically generating the background theories one would expect in a mature proof assistant, such as the Isabelle system. The results show that IsaCoSy produces most, and sometimes all, of the theorems in the Isabelle libraries. The number of additional un-interesting theorems are small enough to be easily pruned by hand.     

A Syntactic Approach to Foundational Proof-Carrying Code

Proof-carrying code (PCC) is a general framework for verifying the safety properties of machine-language programs. PCC proofs are usually written in a logic extended with language-specific typing rules; they certify safety but only if there is no bug in the typing rules. In foundational proof-carrying code (FPCC), on the other hand, proofs are constructed and verified by using strictly the foundations of mathematical logic, with no type-specific axioms. FPCC is more flexible and secure because it is not tied to any particular type system and it has a smaller trusted base. Foundational proofs, however, are much harder to construct. Previous efforts on FPCC all required building sophisticated semantic models for types. Furthermore, none of them can be easily extended to support mutable fields and recursive types. In this article, we present a syntactic approach to FPCC that avoids all of these difficulties. Under our new scheme, the foundational proof for a typed machine program simply consists of the typing derivation plus the formalized syntactic soundness proof for the underlying type system. The former can be readily obtained from a type-checker, while the latter is known to be much easier to construct than the semantic soundness proofs. We give a translation from a typed assembly language into FPCC and demonstrate the advantages of our new system through an implementation in the Coq proof assistant.     

Middle-out reasoning for synthesis and induction

We develop two applications of middle-out reasoning in inductive proofs: logic program synthesis and the selection of induction schemes. Middle-out reasoning as part of proof planning was first suggested by Bundy et al. Middle-out reasoning uses variables to represent unknown terms and formulae. Unification instantiates the variables in the subsequent planning, while proof planning provides the necessary search control. Middle-out reasoning is used for synthesis by planning the verification of an unknown logic program: The program body is represented with a meta-variable. The planning results both in an instantiation of the program body and a plan for the verification of that program. If the plan executes successfully, the synthesized program is partially correct and complete. Middle-out reasoning is also used to select induction schemes. Finding an appropriate induction scheme during synthesis is difficult because the recursion of the program, which is unknown at the outset, determines the induction in the proof. In middle-out induction, we set up a schematic step case by representing the constructors that are applied to induction variables with meta-variables. Once the step case is complete, the instantiated variables correspond to an induction appropriate to the recursion of the program. We have implemented these techniques as an extension of the proof planning system CL ^A M, called Periwinkle, and synthesized a variaety of programs fully automatically. Supported by the Swiss National Science Foundation and ARC Project BC/DAAD Grant 438. The work described in this paper was carried out while the first author was at the Department of Artificial Intelligence of the University of Edinburgh. Supported by the German Ministry for Research and Technology (BMFT) under grant ITS 9102 and ARC Project BC/DAAD Grant 438. Responsibility for the contents of this publication lies with the authors. Supported by SERC grant GR/J/80702, ESPRIT BRP grant 6810, ESPRIT BRP grant EC-US 019-76094, and ARC Project BC/DAAD Grant 438.     

Automatic inductive theorem proving using prolog

Although Prolog is a programming language based on techniques from theorem proving, its use as a base for a theorem prover has not been explored until recently (Stickel, 1984). In this paper, we introduce a Prolog-based deductive theorem proving method for proving theorems in a first-order inductive theory representable in Horn clauses. The method has the following characteristics:

• 1.It automatically partitions the domains over which the variables range into subdomains according to the manner in which the predicate symbols in the theorem are defined.
• 2.For each of the subdomains the prover returns a lemma. If the lemma is true, then the target theorem is true for this subdomain. The lemma could also be an induction hypothesis for the theorem.
• 3.The method does not explicitly use any inductive inference rule. The induction hypothesis, if needed for a certain subdomain, will sometimes be generated from a (limited) forward chaining mechanism in the prover and not from employing any particular inference rule.

In addition to the backward chaining and backtracking facilities of Prolog, our method introduces three new mechanism—skolemization by need, suspended evaluation, and limited forward chaining. These new mechanisms are simple enough to be easily implemented or even incorporated into Prolog. We describe how the theorem prover can be used to prove properties of Prolog programs by showing two simple examples.     

The sliding-window protocol revisited

We give a correctness proof of the sliding-window protocol. Both safety and liveness properties are addressed. We show how faulty channels can be represented as nondeterministic programs. The correctness proof is given as a sequence of correctness-preserving transformations of a sequential program that satisfies the original specification, with the exception that it does not have any faulty channels. We work as long as possible with a sequential program, although the transformation steps are guided by the aim of going to a distributed program. The final transformation steps consist in distributing the actions of the sequential program over a number of processes.     

Dialectic proof procedures for assumption-based, admissible argumentation

We present a family of dialectic proof procedures for the admissibility semantics of assumption-based argumentation. These proof procedures are defined for any conventional logic formulated as a collection of inference rules and show how any such logic can be extended to a dialectic argumentation system.The proof procedures find a set of assumptions, to defend a given belief, by starting from an initial set of assumptions that supports an argument for the belief and adding defending assumptions incrementally to counter-attack all attacks.The proof procedures share the same notion of winning strategy for a dispute and differ only in the search strategy they use for finding it. The novelty of our approach lies mainly in its use of backward reasoning to construct arguments and potential arguments, and the fact that the proponent and opponent can attack one another before an argument is completed. The definition of winning strategy can be implemented directly as a non-deterministic program, whose search strategy implements the search for defences.     

A Recursion Theoretic Approach to Program Testing

Inductive inference, the automatic synthesis of programs, bears certain ostensible relationships with program testing. For inductive inference, one must take a finite sample of the desired input/output behavior of some program and produce (synthesize) an equivalent program. In the testing paradigm, one seeks a finite sample for a function such that any program (in a given set) which computes something other than the object function differs from the object function on the finite sample. In both cases, the finite sample embodies sufficient knowledge to isolate the desired program from all other possibilities. These relationships are investigated and general recursion theoretic properties of testable sets of functions are exposed.     

Constraint Solving for Proof Planning

Proof planning is an application of AI planning to theorem proving that employs plan operators that encapsulate mathematical proof techniques. Many proofs require the instantiation of variables; that is, mathematical objects with certain properties have to be constructed. This is particularly difficult for automated theorem provers if the instantiations have to satisfy requirements specific for a mathematical theory, for example, for finite sets or for real numbers, because in this case unification is insufficient for finding a proper instantiation. Often, constraint solving can be employed for this task. We describe a framework for the integration of constraint solving into proof planning that combines proof planners and stand-alone constraint solvers. Proof planning has some peculiar requirements that are not met by any off-the-shelf constraint-solving system. Therefore, we extended an existing propagation-based constraint solver in a generic way. This approach generalizes previous work on tackling the problem. It provides a more principled way and employs existing AI technology.     

Translating Multi-Agent Autoepistemic Logic into Logic Program

In order to develop a proof procedure of multi-agent autoepistemic Logic (MAEL), a natural framework to formalize belief and reasoning including inheritance, persistence, and causality, we introduce a method that translates a MAEL theory into a logic program with integrity constraints. It is proved that there exists one-to-one correspondence between extensions of a MAEL theory and stable models of a logic program translated from it. Our approach has the following advantages: (1) We can obtain all extensions of a MAEL theory if we compute all stable models of the translated logic program. (2) We can fully use efficient techniques or systems for computing stable models of a logic program. We also investigate the properties of reasoning in MAEL through this translation. The fact that the extension computing problem can be reduced to the stable model computing problem implies that there are close relationships between MAEL and other formalizations of nonmonotonic reasoning.     

Light-Weight SMT-based Model Checking

Recently, the notion of an array-based system has been introduced as an abstraction of infinite state systems (such as mutual exclusion protocols or sorting programs) which allows for model checking of invariant (safety) and recurrence (liveness) properties by Satisfiability Modulo Theories (SMT) techniques. Unfortunately, the use of quantified first-order formulae to describe sets of states makes fix-point checking extremely expensive. In this paper, we show how invariant properties for a sub-class of array-based systems can be model-checked by a backward reachability algorithm where the length of quantifier prefixes is efficiently controlled by suitable heuristics. We also present various refinements of the reachability algorithm that allows it to be easily implemented in a client-server architecture, where a “light-weight” algorithm is the client generating proof obligations for safety and fix-point checks and an SMT solver plays the role of the server discharging the proof obligations. We also report on some encouraging preliminary experiments with a prototype implementation of our approach.     

Hierarchical Wrapper Induction for Semistructured Information Sources

With the tremendous amount of information that becomes available on the Web on a daily basis, the ability to quickly develop information agents has become a crucial problem. A vital component of any Web-based information agent is a set of wrappers that can extract the relevant data from semistructured information sources. Our novel approach to wrapper induction is based on the idea of hierarchical information extraction, which turns the hard problem of extracting data from an arbitrarily complex document into a series of simpler extraction tasks. We introduce an inductive algorithm, STALKER, that generates high accuracy extraction rules based on user-labeled training examples. Labeling the training data represents the major bottleneck in using wrapper induction techniques, and our experimental results show that STALKER requires up to two orders of magnitude fewer examples than other algorithms. Furthermore, STALKER can wrap information sources that could not be wrapped by existing inductive techniques.