Cover Image
QR Code

Co-Developing Programs and Their Proof of Correctness.

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 fut...

Full description

Published in:Communications of the ACM Vol. 67; no. 3; pp. 84 - 95
Main Authors: Chapman, Roderick, Dross, Claire, Matthews, Stuart, Moy, Yannick
Format: Article
Published: Association for Computing Machinery Mar2024
Subjects:
SPARK (Computer program language)
Programming languages
Electronic data processing
Computer programming
Computer software development
Computer software correctness
Online Access:View this record in EBSCOhost
Summary: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.