This description was written by a machine and published without a person checking it. It is what the agent made of this grouping, and not a statement anybody has stood behind.
Bernhard Beckert
A grouping.
The KeY system for deductive verification of Java: taclets as the rule mechanism it is built on, and the two book-length accounts of the approach a decade apart. The fifth record stands apart -- 'Lessons Learned From Microkernel Verification' reports the Verisoft XT work on Microsoft's Hyper-V, and is the corpus's other microkernel verification effort beside seL4, written up as what went wrong.
5 references
Deductive Software Verification – The KeY Book
Mattias Ulbrich and others (2016) · Springer
Formal Methods for Components and Objects, 10th International Symposium, FMCO 2011, Turin, Italy, October 3-5, 2011, Revised Selected Papers
Bernhard Beckert and others (2013) · Springer
Lessons Learned From Microkernel Verification — Specification is the New Bottleneck
Christoph Baumann and others (2012) · Systems Software Verification Conference 2012 (SSV 2012) · Open Publishing Association
Verification of object-oriented software: The KeY approach
Bernhard Beckert and others (2007) · Springer-Verlag
Taclets: A New Paradigm for Constructing Interactive Theorem Provers
Bernhard Beckert and others (2004) · RACSAM