Could We Have Chosen a Better Loop Invariant or Method Contract?

DOI10.1007/978-3-642-02949-3_7zbMath1246.68155OpenAlexW2122077094MaRDI QIDQ3637252

Christoph D. Gladisch

Publication date: 7 July 2009

Published in: Tests and Proofs (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-02949-3_7

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (1)

How testing helps to diagnose proof failures

Uses Software

• KRAKATOA
• KeY

Cites Work

• The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML
• Lazy abstraction
• Sequential, Parallel, and Quantified Updates of First-Order Structures
• Proving Programs Incorrect Using a Sequent Calculus for Java Dynamic Logic
• Generating Unit Tests from Formal Proofs
• White-Box Testing by Combining Deduction-Based Specification Extraction and Black-Box Testing
• Finding Counter Examples in Induction Proofs
• Programming Languages and Systems
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Could We Have Chosen a Better Loop Invariant or Method Contract?