Holistic Specifications for Robust Programs

DOI10.1007/978-3-030-45234-6_21MaRDI QIDQ5039542zbMATH OpenOpenAlexFDO

Authors Sophia Drossopoulou, Julian Mackay, Susan Eisenbach, James Noble

Publication date 13 October 2022

Published in Fundamental Approaches to Software Engineering (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

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

Mathematics Subject Classification ID

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

Recommendations

• Specifications, programs, and total correctness
• A unified approach of program verification
• A framework to measure the robustness of programs in the unpredictable environment
• scientific article; zbMATH DE number 2079677
• Specification and verification of concurrent programs through refinements

Cites work

• An axiomatic basis for computer programming
• Automatic verification of Java programs with dynamic frames
• Behavioral interface specification languages
• Considerate reasoning and the Composite design pattern
• Dafny: an automatic program verifier for functional correctness
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 108549 (Why is no real title available?)
• scientific article; zbMATH DE number 1304000 (Why is no real title available?)
• scientific article; zbMATH DE number 517385 (Why is no real title available?)
• scientific article; zbMATH DE number 1105469 (Why is no real title available?)
• scientific article; zbMATH DE number 1759364 (Why is no real title available?)
• Modular invariants for layered object structures
• Ownership confinement ensures representation independence for object-oriented programs
• Programming semantics for multiprogrammed computations
• Protection in programming languages
• State-dependent representation independence
• The type and effect discipline
• Using History Invariants to Verify Observers

Describes a project that uses

Uses Software

• Dafny
• Spec#
• VerX
• Eiffel
• LARCH

This page was built for publication: Holistic Specifications for Robust Programs

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