Mechanical verification of automatic synthesis of fault-tolerant programs

Full text