Holistic Specifications for Robust Programs

DOI10.1007/978-3-030-45234-6_21OpenAlexW3020179615MaRDI QIDQ5039542

Julian Mackay, Susan Eisenbach, Sophia Drossopoulou, James S. Noble

Publication date: 13 October 2022

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

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)

Uses Software

• Dafny
• LARCH
• Eiffel
• Spec#
• VerX

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Automatic verification of Java programs with dynamic frames
• The type and effect discipline
• Modular invariants for layered object structures
• Behavioral interface specification languages
• Dafny: An Automatic Program Verifier for Functional Correctness
• Ownership confinement ensures representation independence for object-oriented programs
• Considerate Reasoning and the Composite Design Pattern
• State-dependent representation independence
• Programming semantics for multiprogrammed computations
• An axiomatic basis for computer programming
• Protection in programming languages
• Using History Invariants to Verify Observers

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