CIVL Solutions to VerifyThis 2016 Challenges

The VerifyThis 2016 program verification competition was held in April, 2016. The competition presented three verification challenges: the first dealt with matrix multiplication, including the correctness of Strassen's algorithm; the second dealt with Morris' tree traversal algorithm, and the third required verification of a multithreaded tree barrier. In this paper I present solutions using the CIVL (Concurrency Intermediate Verification Language) verifier. CIVL is able to verify each program within small but non–trivial bounds. The solutions are relatively simple, and are presented in full.

@article{Siegel:2017:CSV:3090064.3090070,
 author = {Siegel, Stephen F.},
 title = {CIVL Solutions to Verifythis 2016 Challenges},
 journal = {ACM SIGLOG News},
 issue_date = {April 2017},
 volume = {4},
 number = {2},
 month = may,
 year = {2017},
 issn = {2372-3491},
 pages = {55--75},
 numpages = {21},
 url = {http://doi.acm.org/10.1145/3090064.3090070},
 doi = {10.1145/3090064.3090070},
 acmid = {3090070},
 publisher = {ACM},
 address = {New York, NY, USA},
}