Assumption propagation through annotated programs

DOI10.1007/s00165-016-0395-xzbMath1362.68043OpenAlexW2540613508MaRDI QIDQ2628303

Dipak L. Chaudhari, Om P. Damani

Publication date: 1 June 2017

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

Full work available at URL: https://doi.org/10.1007/s00165-016-0395-x

zbMATH Keywords

correct-by-constructionprogram derivationannotated programsassumption propagation

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Uses Software

• Cocktail
• SPASS
• Why3
• cvc3
• z3
• WhyML

Cites Work

• The derivation of systolic computations
• A program refinement tool
• Exercises in Quantifier Manipulation
• Guarded commands, nondeterminacy and formal derivation of programs
• Refinement Calculus
• Why3 — Where Programs Meet Provers
• An axiomatic basis for computer programming
• Combining Top-Down and Bottom-Up Techniques in Program Derivation
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Assumption propagation through annotated programs