The Landscape of Formal Verification in APL - A Review with a Case Study in Quantum Computing

Explore a comprehensive review of formal verification in APL, focusing on its potential to address the challenges of building dependable and reliable software in an increasingly complex technological landscape. Delve into the effectiveness of APL as a very high-level language for formal verification, examining its strong research precedents and the correspondence between its abstractions and algorithms specifiable in Hoare logic. Discover a workflow-driven methodology for verifying quantum programs in terms of correctness, safety, and liveness, using recent work in APL for quantum computing as a case study. Gain insights into the opportunities and open questions in formal verification with APL, and consider the potential for APL and other array languages to play a significant role in shaping the future of software development and verification.

[ARRAY24] The Landscape of Formal Verification in APL: a Review with a Case Study in Quantum(…)