{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/95372"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/95372","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Coinductive program verification","abstract":"We present a program-verification approach based on coinduction, which makes it feasible to verify programs given an operational semantics of a programming language, without constructing intermediates like axiomatic semantics or verification-condition generators. Specifications can be written using any state predicates. The key observations are that being able to define the correctness of a style of program specification as a greatest fixpoint means coinduction can be used to conclude that a specification holds, and that the number of cases that need to be enumerated to have a coinductively provable specification can be reduced to a feasible number by using a generalized coinduction principle (based on notions of ``coinduction up to'' developed for proving bisimulation) instead of the simplest statement of coinduction. We implement our approach in Coq, producing a certifying language-independent verification framework. The soundness of the system is based on a single module proving the necessary coinduction theorem, which is imported unchanged to prove programs in any language. We demonstrate the power of this approach by verifying algorithms as complicated as Schorr-Waite graph marking, and the flexibility by instantiating it for language definitions covering several paradigms, and in several styles of semantics. We also demonstrate a comfortable level of proof automation for several languages and domains, using a common overall heuristic strategy instantiated with customized subroutines. Manual assistance is also smoothly integrated where automation is not completely successful.","abstract_html":"We present a program-verification approach based on coinduction, which makes it feasible to verify programs given an operational semantics of a programming language, without constructing intermediates like axiomatic semantics or verification-condition generators. Specifications can be written using any state predicates. The key observations are that being able to define the correctness of a style of program specification as a greatest fixpoint means coinduction can be used to conclude that a specification holds, and that the number of cases that need to be enumerated to have a coinductively provable specification can be reduced to a feasible number by using a generalized coinduction principle (based on notions of ``coinduction up to'' developed for proving bisimulation) instead of the simplest statement of coinduction. We implement our approach in Coq, producing a certifying language-independent verification framework. The soundness of the system is based on a single module proving the necessary coinduction theorem, which is imported unchanged to prove programs in any language. We demonstrate the power of this approach by verifying algorithms as complicated as Schorr-Waite graph marking, and the flexibility by instantiating it for language definitions covering several paradigms, and in several styles of semantics. We also demonstrate a comfortable level of proof automation for several languages and domains, using a common overall heuristic strategy instantiated with customized subroutines. Manual assistance is also smoothly integrated where automation is not completely successful.","abstract_has_math":false,"creators":["Moore, Brandon Michael"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Roşu, Grigore","Gunter, Elsa L.","Meseguer, José","Chlipala, Adam"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2017,"date_issued":"2017-03-01T15:49:19Z","date_published":"2017-03-01T15:49:19Z","updated_at":"2026-07-22T22:26:37Z","subjects":["Program Verification","Coinduction","Operational Semantics","Formal Methods","Software Verification"],"languages":["en"],"rights":["Copyright 2016 Brandon Michael Moore"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/95372","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Roşu, Grigore","Gunter, Elsa L.","Meseguer, José","Chlipala, Adam"]},{"key":"dc:creator","label":"Author","values":["Moore, Brandon Michael"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2017-03-01T15:49:19Z","2016-12-01","2016-12"]},{"key":"dc:type","label":"Dc Type","values":["text"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Dissertation"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Ph.D."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Program Verification","Coinduction","Operational Semantics","Formal Methods","Software Verification"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2016 Brandon Michael Moore"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/95372"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["We present a program-verification approach based on coinduction, which makes it feasible to verify programs given an operational semantics of a programming language, without constructing intermediates like axiomatic semantics or verification-condition generators. Specifications can be written using any state predicates. The key observations are that being able to define the correctness of a style of program specification as a greatest fixpoint means coinduction can be used to conclude that a specification holds, and that the number of cases that need to be enumerated to have a coinductively provable specification can be reduced to a feasible number by using a generalized coinduction principle (based on notions of ``coinduction up to'' developed for proving bisimulation) instead of the simplest statement of coinduction. We implement our approach in Coq, producing a certifying language-independent verification framework. The soundness of the system is based on a single module proving the necessary coinduction theorem, which is imported unchanged to prove programs in any language. We demonstrate the power of this approach by verifying algorithms as complicated as Schorr-Waite graph marking, and the flexibility by instantiating it for language definitions covering several paradigms, and in several styles of semantics. We also demonstrate a comfortable level of proof automation for several languages and domains, using a common overall heuristic strategy instantiated with customized subroutines. Manual assistance is also smoothly integrated where automation is not completely successful.","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2017-02-28 without embargo terms","The student, Brandon Moore, accepted the attached license on 2016-11-30 at 13:16.","The student, Brandon Moore, submitted this Dissertation for approval on 2016-11-30 at 13:45.","This Dissertation was approved for publication on 2016-12-01 at 14:50.","DSpace SAF Submission Ingestion Package generated from Vireo submission #10372 on 2017-02-28 at 14:54:48","Made available in DSpace on 2017-03-01T15:49:19Z (GMT). No. of bitstreams: 4 MOORE-DISSERTATION-2016.pdf: 508032 bytes, checksum: 3e0b5fd64b2ae3c8ffe1878c4ae59545 (MD5) bmmoore-thesis-2016.tgz: 189432 bytes, checksum: 0290ea28f5071daca2f0831353ca4e38 (MD5) LICENSE.txt: 4210 bytes, checksum: 967189421b9d3930725c37004912bbbb (MD5) PROQUEST_LICENSE.txt: 4556 bytes, checksum: 1c61c9ec27e81251e2b4ed9acbb54d84 (MD5) Previous issue date: 2016-12-01"]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Coinductive program verification"]}]}],"canonical_facts":{"dc:contributor":["Roşu, Grigore","Gunter, Elsa L.","Meseguer, José","Chlipala, Adam"],"dc:creator":["Moore, Brandon Michael"],"dc:date":["2017-03-01T15:49:19Z","2016-12-01","2016-12"],"dc:description":["We present a program-verification approach based on coinduction, which makes it feasible to verify programs given an operational semantics of a programming language, without constructing intermediates like axiomatic semantics or verification-condition generators. Specifications can be written using any state predicates. The key observations are that being able to define the correctness of a style of program specification as a greatest fixpoint means coinduction can be used to conclude that a specification holds, and that the number of cases that need to be enumerated to have a coinductively provable specification can be reduced to a feasible number by using a generalized coinduction principle (based on notions of ``coinduction up to'' developed for proving bisimulation) instead of the simplest statement of coinduction. We implement our approach in Coq, producing a certifying language-independent verification framework. The soundness of the system is based on a single module proving the necessary coinduction theorem, which is imported unchanged to prove programs in any language. We demonstrate the power of this approach by verifying algorithms as complicated as Schorr-Waite graph marking, and the flexibility by instantiating it for language definitions covering several paradigms, and in several styles of semantics. We also demonstrate a comfortable level of proof automation for several languages and domains, using a common overall heuristic strategy instantiated with customized subroutines. Manual assistance is also smoothly integrated where automation is not completely successful.","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2017-02-28 without embargo terms","The student, Brandon Moore, accepted the attached license on 2016-11-30 at 13:16.","The student, Brandon Moore, submitted this Dissertation for approval on 2016-11-30 at 13:45.","This Dissertation was approved for publication on 2016-12-01 at 14:50.","DSpace SAF Submission Ingestion Package generated from Vireo submission #10372 on 2017-02-28 at 14:54:48","Made available in DSpace on 2017-03-01T15:49:19Z (GMT). No. of bitstreams: 4 MOORE-DISSERTATION-2016.pdf: 508032 bytes, checksum: 3e0b5fd64b2ae3c8ffe1878c4ae59545 (MD5) bmmoore-thesis-2016.tgz: 189432 bytes, checksum: 0290ea28f5071daca2f0831353ca4e38 (MD5) LICENSE.txt: 4210 bytes, checksum: 967189421b9d3930725c37004912bbbb (MD5) PROQUEST_LICENSE.txt: 4556 bytes, checksum: 1c61c9ec27e81251e2b4ed9acbb54d84 (MD5) Previous issue date: 2016-12-01"],"dc:format":["application/pdf"],"dc:identifier":["http://hdl.handle.net/2142/95372"],"dc:language":["en"],"dc:rights":["Copyright 2016 Brandon Michael Moore"],"dc:subject":["Program Verification","Coinduction","Operational Semantics","Formal Methods","Software Verification"],"dc:title":["Coinductive program verification"],"dc:type":["text"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Dissertation"],"thesis:degree_name":["Ph.D."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:26:37Z"}