Invariant based programming: Basic approach and teaching experiences

DOI10.1007/s00165-008-0070-yzbMath1178.68334OpenAlexW1965484730MaRDI QIDQ1019025

Ralph-Johan Back

Publication date: 27 May 2009

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-008-0070-y

zbMATH Keywords

program verification

Mathematics Subject Classification ID

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

Related Items

Traits: correctness-by-construction for free, Information Flow Control-by-Construction for an Object-Oriented Language, Flexible Correct-by-Construction Programming, A programming model for BSP with partitioned synchronisation, Reasoning about orchestrations of web services using partial correctness, Verification and code generation for invariant diagrams in Isabelle, Transformational Programming and the Derivation of Algorithms, Provably correct derivation of algorithms using FermaT

Uses Software

• PVS
• JML
• Spec#
• SIMPLIFY
• Python

Cites Work

• Statecharts: a visual formalism for complex systems
• Programming with Verification Conditions
• A constructive approach to the problem of program correctness
• Unnamed Item
• Unnamed Item