Serge Autexier, Dieter Hutter, Heiko Mantel, Axel Schairer, System Description: INKA 5.0 - A Logic Voyager, In Proceedings of CADE-16, Trento, Italy, July, 1999.

Abstract: Originally developed as an automatic inductive theorem prover, we describe a new version INKA 5.0, which is a result from the long experience made in formal software development. This experience led to the integration of a development graph composed of deductive units and relations between them. In order to support the evolutionary aspect of formal software development, INKA supports an efficient management of change. Each deductive unit consists of (local) set of axioms and an individual logic. Hence logic units and relations between them have been developed, in order to support the definition and use of various logics. As a basis for the implementation of logics, INKA provides an annotated lambda-calculus as underlying meta-language. Similarly, INKA supports the definition of different calculi by an explicit representation of calculi by calculus units. Proofs developed wrt. calculus units are explicitely represented in an uniform hierarchical proof datastructure and INKA provides a generic tactic definition mechanism to implement appropriate proof search engines for each calculus unit.

Serge Autexier, Dieter Hutter, Heiko Mantel, Axel Schairer. Towards an Evolutionary Formal Software-Development Using CASL, In WADT99 Selected Papers volume, Springer, LNCS 1827, 2000.

Abstract: In practice, the formal development of software is an evolutionary process. Failed proof attempts give rise to changes in the specification and such changes invalidate proofs which have been previously performed. Clearly, it is very desirable to preserve much of the proof effort after such changes. In this paper, we propose development graphs as a general framework for modular specifications and define a structure preserving translation of CASL specifications into these graphs. The feature of development graphs, which is most important for an evolutionary process, is that they simplify the analysis of changes to the specification such that their negative effects can be kept to a minimum.

Dieter Hutter. Management of change in structured verification. to appear, 2000. NEW: comments are welcome !

Abstract: The use of formal methods in large complex applications implies the need for an evolutionary formal program development in which specification and verification phases are interleaved. But any change of a specification either by adding new parts or by changing erroneous parts affects existing verification work in a subtle way. In this paper we present a truth maintenance system for structured specification and verification. It is based on the simple but powerful notion of a development graph as an underlying datastructure to represent an actual consistent state of a formal development. Based on this notion we try to minimize the consequences of changes of existing verification work.

Serge Autexier, Dieter Hutter. Towards an efficient management of change in an evolutionary formal software development , Abstract for the 2nd Kiel workshop on "Engineering of Software Verification, Validation, and Certification", Kiel, Germany, 2000.

Till Mossakowski, Serge Autexier, Dieter Hutter. Extending Development Graphs With Hiding, In H. Hußmann (Ed.), Proceedings of Fundamental Approaches to Software Engineering (FASE 2001), April 2-6, 2001, Genova, Italy, accepted, forthcoming.

Abstract: Development graphs are a tool for dealing with structured specifications in a way easing management of change and reusing proofs. In this work, we extend development graphs with hiding. Hiding is a particularly difficult to realize operation, s ince it does not admit such a good decomposition of the involved specifications as other structuring operations do. We develop both a semantics and proof rules for development graphs with hiding. The rules are proven to be sound, and also complete relative to an oracle for conservative extensions. We also show that an absolute complete set of rules cannot exist. The whole framework is developed in a way independent of the underlying logical system.

Serge Autexier, A Proof-Planning Framework with explicit Abstractions based on Indexed Formulas, In M.-P. Bonacina and B. Gramlich (Eds.) Proceedings of the 4th workshop on strategies in automated deduction (STRATEGIES'01), Università degli studi di Siena, TR DII 10/01, Siena, Italy, June, 2001.

Abstract: The aim of proof-planning is to bridge the gap between high-level, cognitively adequate reasoning for specific domains, and calculus-level reasoning to ensure soundness. For high reasoning levels the cognitive adequacy of representation and reasoning techniques is a major issue, while for lower reasoning levels the adequacy wrt. the modeled domain is important. Furthermore, proof construction is an engineering task and there is a need to support the design and application of proof-search engineering methods. To this end we present a framework to explicitly support different reasoning levels. To structure reasoning levels the framework allows for the explicit representation of abstractions and proof-search refinement techniques. In order to ensure soundness within a reasoning level, we use techniques developed in the context of matrix characterization relying on the notion of indexed formulas. Furthermore, we introduce a uniform concept for contextual reasoning, and sketch basic tacticals for the definition of tactics to organize the overall proof-search inside and across different reasoning levels.

Axel Schairer, Serge Autexier, Dieter Hutter, A Pragmatic Approach to Reuse in Tactical Theorem Proving, In M.-P. Bonacina and B. Gramlich (Eds.) Proceedings of the 4th workshop on strategies in automated deduction (STRATEGIES'01), Università degli studi di Siena, TR DII 10/01, Siena, Italy, June, 2001.

Abstract: In interactive theorem proving, tactics and tacticals have been introduced to automate proof search. In this scenario, user interaction traditionally is restricted to the mode in which the user decides which tactic to apply on the top-level, without being able to interact with the tactic once it has begun running. We propose a technique to allow for the implementation of derivational analogy in tactical theorem proving. Instead of replaying tactics including backtracked dead ends our framework makes choice points in tactics explicit and thus avoids dead ends when reusing tactics. Additionally users can override choices a tactic has made or add additional steps to a derivation without terminating the tactic. The technique depends on an efficient replay of tactic executions without repeating search that the original computation may have involved.