Semantical proofs of correctness for programs performing non-deterministic tests on real numbers

DOI10.1017/S0960129510000186zbMATH Open1213.68201MaRDI QIDQ3060187FDOQ3060187

Authors: Thomas Anberrée 

Publication date: 1 December 2010

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Recommendations

• A Denotational Semantics for Total Correctness of Sequential Exact Real Programs
• scientific article; zbMATH DE number 4006264
• scientific article; zbMATH DE number 1760049
• Total correctness in nonstandard logics of programs
• scientific article; zbMATH DE number 3936484
• Verification, Model Checking, and Abstract Interpretation
• Partiality and nondeterminacy in program proofs
• Formal verification of numerical programs: from C annotated programs to mechanical proofs
• scientific article; zbMATH DE number 4005583

zbMATH Keywords

denotational semanticsSmyth power domains

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55)

Cites Work

• LCF considered as a programming language
• Domain-Theoretic Foundations of Functional Programming
• Semantics of a sequential language for exact real-number computation
• Recursive characterization of computable real-valued functions and relations

Cited In (4)

• A Denotational Semantics for Total Correctness of Sequential Exact Real Programs
• Semantics of a sequential language for exact real-number computation
• Computable decision making on the reals and other spaces. Via partiality and nondeterminism
• Validating Brouwer's continuity principle for numbers using named exceptions

This page was built for publication: Semantical proofs of correctness for programs performing non-deterministic tests on real numbers

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