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 51 articles , 2 standard articles )

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

1 2 3 next

  1. Apt, Krzysztof R.; Olderog, Ernst-Rüdiger: Fifty years of Hoare’s logic (2019)
  2. Derrick, John; Doherty, Simon; Dongol, Brijesh; Schellhorn, Gerhard; Travkin, Oleg; Wehrheim, Heike: Mechanized proofs of opacity: a comparison of two techniques (2018)
  3. Derrick, John; Dongol, Brijesh; Schellhorn, Gerhard; Travkin, Oleg; Wehrheim, Heike: Verifying opacity of a transactional mutex lock (2015)
  4. Amighi, Afshin; Blom, Stefan; Darabi, Saeed; Huisman, Marieke; Mostowski, Wojciech; Zaharieva-Stojanovski, Marina: Verification of concurrent systems with VerCors (2014)
  5. Moszkowski, Ben: Compositional reasoning using intervals and time reversal (2014)
  6. Schellhorn, Gerhard; Derrick, John; Wehrheim, Heike: A sound and complete proof technique for linearizability of concurrent data structures (2014)
  7. Schellhorn, Gerhard; Tofan, Bogdan; Ernst, Gidon; Pfähler, Jörg; Reif, Wolfgang: RGITL: a temporal logic framework for compositional reasoning about interleaved programs (2014)
  8. Filliâtre, Jean-Christophe: One logic to use them all (2013)
  9. Moszkowski, Ben: A complete axiom system for propositional interval temporal logic with infinite time (2012)
  10. Bäumler, Simon; Schellhorn, Gerhard; Tofan, Bogdan; Reif, Wolfgang: Proving linearizability with temporal logic (2011)
  11. Ernst, Gidon; Schellhorn, Gerhard; Reif, Wolfgang: Verification of B(^ + ) trees: an experiment combining shape analysis and interactive theorem proving (2011) ioport
  12. Maingaud, Séverine; Balat, Vincent; Bubel, Richard; Hähnle, Reiner; Miquel, Alexandre: Specifying imperative ML-like programs using dynamic logic (2011)
  13. Schellhorn, Gerhard: Completeness of fair ASM refinement (2011)
  14. Tofan, Bogdan; Schellhorn, Gerhard; Reif, Wolfgang: Formal verification of a lock-free stack with hazard pointers (2011)
  15. Weiß, Benjamin: Predicate abstraction in a program logic calculus (2011)
  16. Banach, Richard; Schellhorn, Gerhard: Atomic actions, and their refinements to isolated protocols (2010)
  17. Bäumler, Simon; Balser, Michael; Nafz, Florian; Reif, Wolfgang; Schellhorn, Gerhard: Interactive verification of concurrent systems using symbolic execution (2010)
  18. Dunets, Andriy; Schellhorn, Gerhard; Reif, Wolfgang: Automated flaw detection in algebraic specifications (2010)
  19. Piskac, Ruzica; Kuncak, Viktor: MUNCH -- automated reasoner for sets and multisets (2010)
  20. Tofan, Bogdan; Bäumler, Simon; Schellhorn, Gerhard; Reif, Wolfgang: Temporal logic verification of lock-freedom (2010)

1 2 3 next