Post date: May 06, 2021 9:44:18 AM
Bryan Parno and colleagues described a new programming language for software verification, named Armada, for high-performance concurrent programs that ensures that programs are mathematically proven to compute correctly. The paper
Lorch et al. 2020. Armada: low-effort verification of high-performance concurrent programs. http://www.andrew.cmu.edu/user/bparno/papers/armada.pdf, https://doi.org/10.1145/3385412.3385971
was presented at last year's Conference on Programming Language Design and Implementation where the paper received a Distinguished Paper award.
See also New programming language and tool ensures code will compute as intended
See also New method ensures complex programs are bug-free without testing