SucheHome of KIV
This is the home page of the KIV (Karlsruhe Interactive Verifier) theorem prover. Currently you can download KIV as part of a vmware-image or as a .tgz archive for linux. |
DownloadVMWare-Image
Linux-ArchivePlease request if you need support for java verification in KIV. License AgreementThis license grants the signer a non-transferable and non-exclusive right to use KIV (version 5.1). This license is restricted to noncommercial use and ends one year after downloading the system. KIV is provided on an "as is" basis, without warranty or liability of any kind. Licensee agrees not to distribute, modify, or disassemble any of the software files KIV consists of. This license is free of charge. Licensee will share his experiences using KIV with the developers. Licensee also agrees to respect the license of clisp and uDraw, since both are contained in the distribution of KIV. DescriptionOverviewKIV is a tool for formal systems development. It can be employed, e.g.,
KIV projectsWeb presentations have been prepared for a number of projects that have been done with KIV. A summary is on the KIV projects page.Specification LanguageKIV supports both the functional and the state-based approach to describe hierarchically structured systems. The functional approach uses higher-order algebraic specifications. The first-order part is a subset of CASL. Specifications are built up from elementary specifications with the operations enrichment, union, renaming, parameterization and actualization. Specifications have a loose semantics and may include generation principles to define inductive data types. Specification components can be implemented by stepwise refinement using modules with imperative programs. The designer is subject to a strict decompositional design discipline leading to modular systems with compositional correctness. As a consequence, the verification effort for a modular system becomes linear in the number of its modules. For the state-based approach KIV offers three approaches: Abstract State Machines (ASMs) , parallel programs and state charts. ASMs define rules to describe state transitions. Our variant of ASMs is based on algebraically specified data types. The semantics of an ASM is the set of traces generated by the transition relation defined by the rules of the ASM. ASMs are implemented using a compositional refinement notion. A modularization theorem (see this paper for details) allows to decompose the correctness proofs for a refinement into proofs showing the commutativity of diagrams consisting of m abstract and n concrete steps. Such m:n diagrams generalize the usual 1:1 diagrams used in data refinement (see this paper for details). An important application of ASM refinement is compiler correctness, where we have verified a Prolog compiler (see this paper ). Correctness proofs use Dynamic Logic, a program logic for imperative programs. Parallel Programs extend sequential programs with additional operators to execute programs in parallel: both interleaved as well as asyncronous parallel execution are supported. An await-operator is used for synchronisation. Properties of parallel programs are proved using a powerful Temporal Logic, which extends CTL*. The logic embeds programs directly as formulas, no encoding as e.g. in TLA is necessary. This allows to keep the intuitive principle of symbolic execution from sequential programs, thus allowing for a high degree of automation. State Charts are hierarchical automata. KIV uses a semantics of statecharts with micro and macro steps. Statecharts like programs are embedded in the Temporal Logic of KIV as formulas. In KIV, formal specifications of software and system designs are represented explicitly as directed acyclic graphs called development graphs. Each node corresponds to a specification component, an ASM, a module or an ASM refinement. Each node has a theorem base attached. Theorem bases initially contain axioms, ASM rules, paralle programs, state charts and automatically generated proof obligations for refinements. The theorem base also stores theorems added by the user (proved and yet unproved ones), and manages proofs and their dependencies. Proof SupportIn KIV, proofs for specification validation, design verification, and program verification are supported by an advanced interactive deduction component based on proof tactics. It combines a high degree of automation with an elaborate interactive proof engineering environment. Deduction is based on a sequent calculus with proof tactics like simplification, lemma application, and induction for first-order reasoning and a proof strategy based on symbolic execution and induction for the verification of implementations with imperative programs using Dynamic Logic. To automate proofs, KIV offers a number of heuristics. Among others, heuristics for induction, unfolding of procedure calls and quantifier instantiation are provided. Heuristics can be chosen freely, and changed any time during the proof. Additionally, a `problem specific' heuristic exists which is easily adaptable to specific applications. Usually, the heuristics manage to find 80 - 100 % of the required proof steps automatically. The conditional rewriter in KIV (called simplifier) handles thousands of rules very efficiently by compiling them to executable functional programs. Some extensions of standard rewrite rules are AC-rewriting, elimination rules and forward reasoning. As the structure of a formula helps to understand its meaning, the KIV simplifier always preserves this structure. The user explicitly chooses the rewrite and simplification rules. Different sets of simplification rules can be chosen for different tasks. Frequently, the problem in engineering high assurance systems is not to verify proof obligations affirmatively, but rather to interpret failed proof attempts that may indicate errors in specifications, programs, lemmas etc. Therefore, KIV offers a number of proof engineering facilities to support the iterative process of (failed) proof attempts, error detection, error correction and re-proof. Dead ends in proof trees can be cut off, proof decisions may be withdrawn both chronologically and non-chronologically. Unprovable subgoals can be detected by automatically generating counter examples. This counter example can be traced backwards through the proof to the earliest point of failure. Thereby the user is assisted in the decision whether the goal to prove is not correct, proof decisions were incorrect, or there is a flaw in the specification. After a correction the goal must be re-proved. Here another interesting feature of KIV, the strategy for proof reuse, can be used. Both successful and failed proof attempts are reused automatically to guide the verification after corrections. This goes far beyond proof replay or proof scripts. We found that typically 90% of a failed proof attempt can be recycled for the verification after correction. The correctness management in KIV ensures that changes to or deletions of specifications, modules, and theorems do not lead to inconsistencies, and that the user can do proofs in any order (not only bottom up). It guarantees that only the minimal number of proofs are invalidated after modifications, that there are no cycles in the proof hierarchy and that finally all used lemmas and proof obligations are proved (in some sub-specification). User InterfaceKIV offers a powerful graphical user interface which has been constantly improved over the years. The intuitive user interface allows easy access to KIV for first time users, and is an important prerequisite for managing large applications. The interface is object oriented, and is implemented in Java to guarantee platform independency. The top-level object of a development, the development graph, is displayed using daVinci, a graph visualization tool which automatically arranges large graphs conveniently. The theorem base, which is attached to each development node, is arranged in tables, and context sensitive popup menus are provided for manipulation. While proving a theorem, the user is able to restrict the set of applicable tactics by selecting a context, i.e. a formula or term in the goal, with the mouse. This is extremely helpful for applying rewrite rules, as the set of hundreds of rewrite rules is reduced to a small number of applicable rules for the selected context. Proofs are presented as trees, where the user can click on nodes to inspect single proof steps. In large applications, the plentitude of information may be confusing. Therefore, important information is summarized, and more details are displayed on request. Different colors are used to classify the given information. Additionally a special font allows the use of a large number of mathematical symbols. KIV automatically produces LaTeX documentation for a development on different levels of detail. Specifications, implementations, theorem bases, proof protocols, and various kinds of statistics are pretty printed. The user is encouraged to add comments to specifications, which are also used to automatically produce a data dictionary. As several users may work simultaneously on a large project, the documentation facilities of KIV are very important. The automatically extracted information can also be included into reports. Features
|