KIV

Karlsruhe Interactive Verifier (KIV). KIV is an interactive theorem prover with a user definable object logic. The main applications rely on a definition of dynamic logic, for reasoning about the correctness of software systems. Several other object logics have been defined for experimental pursoses. The core of KIV is implemented in an ML-like functional language called PPL, and interfaces to the outside world via yacc/lex generated parsers and C/Motif. PPL itself is implemented in Lisp. KIV is used, among others, in the Verificaiton Support Environment (VSE) developed for the German Information Security Agency. For this pursose, KIV was integrated with an induction theorem prover and a case tool.


References in zbMATH (referenced in 42 articles , 2 standard articles )

Showing results 1 to 20 of 42.
Sorted by year (citations)

1 2 3 next

  1. Moszkowski, Ben: Compositional reasoning using intervals and time reversal (2014)
  2. Schellhorn, Gerhard; Derrick, John; Wehrheim, Heike: A sound and complete proof technique for linearizability of concurrent data structures (2014)
  3. Schellhorn, Gerhard; Tofan, Bogdan; Ernst, Gidon; Pfähler, Jörg; Reif, Wolfgang: RGITL: a temporal logic framework for compositional reasoning about interleaved programs (2014)
  4. Moszkowski, Ben: A complete axiom system for propositional interval temporal logic with infinite time (2012)
  5. Bäumler, Simon; Schellhorn, Gerhard; Tofan, Bogdan; Reif, Wolfgang: Proving linearizability with temporal logic (2011)
  6. Ernst, Gidon; Schellhorn, Gerhard; Reif, Wolfgang: Verification of $B^ + $ trees: An experiment combining shape analysis and interactive theorem proving (2011)
  7. Maingaud, Séverine; Balat, Vincent; Bubel, Richard; Hähnle, Reiner; Miquel, Alexandre: Specifying imperative ML-like programs using dynamic logic (2011)
  8. Schellhorn, Gerhard: Completeness of fair ASM refinement (2011)
  9. Tofan, Bogdan; Schellhorn, Gerhard; Reif, Wolfgang: Formal verification of a lock-free stack with hazard pointers (2011)
  10. Weiß, Benjamin: Predicate abstraction in a program logic calculus (2011)
  11. Banach, Richard; Schellhorn, Gerhard: Atomic actions, and their refinements to isolated protocols (2010)
  12. Bäumler, Simon; Balser, Michael; Nafz, Florian; Reif, Wolfgang; Schellhorn, Gerhard: Interactive verification of concurrent systems using symbolic execution (2010)
  13. Dunets, Andriy; Schellhorn, Gerhard; Reif, Wolfgang: Automated flaw detection in algebraic specifications (2010)
  14. Boiten, Eerke; Derrick, John; Schellhorn, Gerhard: Relational concurrent refinement. II: Internal operations and outputs (2009)
  15. Bubel, Richard; Hähnle, Reiner; Weiß, Benjamin: Abstract interpretation of symbolic execution with explicit state updates (2009)
  16. Aehlig, Klaus; Haftmann, Florian; Nipkow, Tobias: A compiled implementation of normalization by evaluation (2008)
  17. Banach, Richard; Schellhorn, Gerhard: On the refinement of atomic actions. (2008)
  18. Dunets, Andriy; Schellhorn, Gerhard; Reif, Wolfgang: Automating algebraic specifications of non-freely generated data types (2008)
  19. Dunets, Andriy; Schellhorn, Gerhard; Reif, Wolfgang: Bounded relational analysis of free data types (2008)
  20. Haneberg, Dominik; Schellhorn, Gerhard; Grandy, Holger; Reif, Wolfgang: Verification of mondex electronic purses with KIV: from transactions to a security protocol (2008)

1 2 3 next