Co-Developing Programs and Their Proof of Correctness. - Chapman, Roderick; Dross, Claire; Matthews, Stuart; Moy, Yannick (Communications of the ACM, 2024)
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.