KeY: A Formal Method for Object-Oriented Systems

DOI10.1007/978-3-540-72952-5_2MaRDI QIDQ5428904zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• scientific article; zbMATH DE number 1759367
• scientific article; zbMATH DE number 2087530
• Modular specification and verification of object-oriented programs
• scientific article; zbMATH DE number 1706329
• scientific article; zbMATH DE number 1481757

Cites work

• An axiomatic basis for computer programming
• Fundamental Approaches to Software Engineering
• scientific article; zbMATH DE number 4024753 (Why is no real title available?)
• scientific article; zbMATH DE number 3469999 (Why is no real title available?)
• scientific article; zbMATH DE number 1556014 (Why is no real title available?)
• scientific article; zbMATH DE number 1765699 (Why is no real title available?)
• scientific article; zbMATH DE number 837700 (Why is no real title available?)
• Integration of a Security Type System into a Program Logic
• Proving Programs Incorrect Using a Sequent Calculus for Java Dynamic Logic
• White-Box Testing by Combining Deduction-Based Specification Extraction and Black-Box Testing

Cited in

(18)

• A system for deduction-based formal verification of workflow-oriented software models
• KeY
• Proof pearl: The KeY to correct and stable sorting
• Numerically-aided deductive safety proof for a powertrain control system
• scientific article; zbMATH DE number 2040574 (Why is no real title available?)
• scientific article; zbMATH DE number 1487743 (Why is no real title available?)
• scientific article; zbMATH DE number 1759367 (Why is no real title available?)
• A dynamic logic for deductive verification of multi-threaded programs
• scientific article; zbMATH DE number 2087530 (Why is no real title available?)
• On the worst-case complexity of TimSort
• Efficient Verified Implementation of Introsort and Pdqsort
• Specification and runtime verification of Java card programs
• Towards a combination of CafeOBJ and PAT
• An Algebraic Semantics for Contract-Based Software Components
• An automated quantitative information flow analysis for concurrent programs
• Formal verification for event stream processing: model checking of BeepBeep stream processing pipelines
• Verifying traits: an incremental proof system for fine-grained reuse
• Compositional reasoning about active objects with shared futures

Describes a project that uses

Uses Software

• JML
• ASMKeY

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5428904)