KeY: A Formal Method for Object-Oriented Systems

DOI10.1007/978-3-540-72952-5_2zbMath1202.68092OpenAlexW1561523230MaRDI QIDQ5428904

Wolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt

Publication date: 28 November 2007

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-72952-5_2

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (12)

Efficient Verified Implementation of Introsort and Pdqsort ⋮ Compositional reasoning about active objects with shared futures ⋮ An automated quantitative information flow analysis for concurrent programs ⋮ Formal verification for event stream processing: model checking of BeepBeep stream processing pipelines ⋮ Unnamed Item ⋮ A dynamic logic for deductive verification of multi-threaded programs ⋮ Specification and Runtime Verification of Java Card Programs ⋮ Verifying traits: an incremental proof system for fine-grained reuse ⋮ Numerically-aided deductive safety proof for a powertrain control system ⋮ KeY ⋮ An Algebraic Semantics for Contract-Based Software Components ⋮ Proof pearl: The KeY to correct and stable sorting

Uses Software

• JML
• ASMKeY

Cites Work

• Integration of a Security Type System into a Program Logic
• Fundamental Approaches to Software Engineering
• Proving Programs Incorrect Using a Sequent Calculus for Java Dynamic Logic
• White-Box Testing by Combining Deduction-Based Specification Extraction and Black-Box Testing
• An axiomatic basis for computer programming
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: KeY: A Formal Method for Object-Oriented Systems