Flexible Correct-by-Construction Programming

DOI10.46298/lmcs-19(2:16)2023arXiv2211.15261MaRDI QIDQ6135766

Ina Schaefer, Thomas Thüm, Unnamed Author, Tobias Runge, Alex Potanin

Publication date: 26 August 2023

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2211.15261

zbMATH Keywords

traitsformal methodscorrectness-by-constructionpost-hoc verification

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Software engineering and formal methods. 10th international conference, SEFM 2012, Thessaloniki, Greece, October 1--5, 2012. Proceedings
• ArcAngel: a tactic language for refinement
• Verifying traits: an incremental proof system for fine-grained reuse
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Extending FeatherTrait Java with interfaces
• A UTP semantics for \textsf{Circus}
• Invariant based programming: Basic approach and teaching experiences
• Traits: correctness-by-construction for free
• For a few dollars more. Verified fine-grained algorithm analysis down to LLVM
• Applying Data Refinement for Monadic Programs to Hopcroft’s Algorithm
• Refinements for Free!
• Dafny: An Automatic Program Verifier for Functional Correctness
• A Deductive Approach to Program Synthesis
• Guarded commands, nondeterminacy and formal derivation of programs
• Refinement Calculus
• Verification of Concurrent Systems with VerCors
• Data Refinement in Isabelle/HOL
• The Correctness-by-Construction Approach to Programming
• Feature integration using a feature construct

This page was built for publication: Flexible Correct-by-Construction Programming