View in EDS PDF Full Text

Co-Developing Programs and Their Proof of Correctness.

Saved in:
Bibliographic Details
Title: Co-Developing Programs and Their Proof of Correctness.
Authors: Chapman, Roderick1 (AUTHOR) rodchap@amazon.co.uk, Dross, Claire2 (AUTHOR), Matthews, Stuart3 (AUTHOR), Moy, Yannick2 (AUTHOR)
Source: Communications of the ACM. Mar2024, Vol. 67 Issue 3, p84-94. 11p.
Subjects: SPARK (Computer program language), Programming languages, Electronic data processing, Computer programming, Computer software development, Computer software correctness
Abstract: The article focuses on the auto-active approach for co-developing programs and their proof of correctness, specifically the open source SPARK technology. The authors discuss the key design and technological choices for SPARK, which made it successful within the industry, and explore the possible future of SPARK and other analyzers of the same family.
Database: Engineering Source
Description
Abstract:The article focuses on the auto-active approach for co-developing programs and their proof of correctness, specifically the open source SPARK technology. The authors discuss the key design and technological choices for SPARK, which made it successful within the industry, and explore the possible future of SPARK and other analyzers of the same family.
ISSN:00010782
DOI:10.1145/3624728