{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/115485"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/115485","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Advancements in automated first-order verification","abstract":"Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2022-11-11 without embargo terms","abstract_html":"Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2022-11-11 without embargo terms","abstract_has_math":false,"creators":["Pena, Lucas"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Rosu, Grigore","Parthasarathy, Madhusudan","Meseguer, José","Löding, Christof"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2022,"date_issued":"2022-05","date_published":"2022-05","updated_at":"2026-07-22T22:24:54Z","subjects":["first-order logic","verification","least fixpoints","matching logic","synthesis","separation logic"],"languages":["en","eng"],"rights":["Copyright 2022 Lucas Peña"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"https://hdl.handle.net/2142/115485","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Rosu, Grigore","Parthasarathy, Madhusudan","Meseguer, José","Löding, Christof"]},{"key":"dc:creator","label":"Author","values":["Pena, Lucas"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2022-05","2022-04-19"]},{"key":"dc:type","label":"Dc Type","values":["text","Thesis"]},{"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":["first-order logic","verification","least fixpoints","matching logic","synthesis","separation logic"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en","eng"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2022 Lucas Peña"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["https://hdl.handle.net/2142/115485"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2022-11-11 without embargo terms","The student, Lucas Pena, accepted the attached license on 2022-04-18 at 20:03.","The student, Lucas Pena, submitted this Dissertation for approval on 2022-04-18 at 20:11.","This Dissertation was approved for publication on 2022-04-19 at 13:47.","DSpace SAF Submission Ingestion Package generated from Vireo submission #17772 on 2022-11-11 at 13:15:39","In this work, we present advancements in the field of generic automated first-order verification. We focus on quantified first-order logic in the presence of background theories, both with and without least fixpoints (FOL and FO+lfp respectively), and various first- order logic variants. We provide both theoretical advancements via decision procedures and completeness results, as well as tools based on these techniques to demonstrate their efficacy on practical examples. We first develop a systematic quantifier instantiation technique and prove the relative completeness of this technique for a fragment of FOL. We also show how we can introduce induction principles to help bridge the gap between FOL and FO+lfp. Next, we develop a tool called FOSSIL that automatically performs systematic quantifier instantiation on a given quantified formula. Furthermore, FOSSIL includes a lemma synthesis technique for FO+lfp formulas, where we automatically synthesize inductive lemmas from a given theorem. Turning to first-order variants, we develop a tool for automatically verifying formulas in matching logic, a first-order variant with a least fixpoint operator which has a unified frame- work for specifications and proofs. We also present an efficient translation from matching logic (without least fixpoints) to first-order logic. This yields a completeness result for a fragment of matching logic formulas, while also allowing us to apply existing first-order reasoning tools and techniques, including the FOSSIL tool developed for systematic quantifier instantiation. Finally, we introduce a separation logic alternative known as frame logic, an extension of first-order logic with a construct that captures the implicit supports of formulas. Similar to matching logic, we show how frame logic can be converted to first-order logic with recursive definitions, where again we can directly apply other reasoning tools and techniques."]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Advancements in automated first-order verification"]}]}],"canonical_facts":{"dc:contributor":["Rosu, Grigore","Parthasarathy, Madhusudan","Meseguer, José","Löding, Christof"],"dc:creator":["Pena, Lucas"],"dc:date":["2022-05","2022-04-19"],"dc:description":["Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2022-11-11 without embargo terms","The student, Lucas Pena, accepted the attached license on 2022-04-18 at 20:03.","The student, Lucas Pena, submitted this Dissertation for approval on 2022-04-18 at 20:11.","This Dissertation was approved for publication on 2022-04-19 at 13:47.","DSpace SAF Submission Ingestion Package generated from Vireo submission #17772 on 2022-11-11 at 13:15:39","In this work, we present advancements in the field of generic automated first-order verification. We focus on quantified first-order logic in the presence of background theories, both with and without least fixpoints (FOL and FO+lfp respectively), and various first- order logic variants. We provide both theoretical advancements via decision procedures and completeness results, as well as tools based on these techniques to demonstrate their efficacy on practical examples. We first develop a systematic quantifier instantiation technique and prove the relative completeness of this technique for a fragment of FOL. We also show how we can introduce induction principles to help bridge the gap between FOL and FO+lfp. Next, we develop a tool called FOSSIL that automatically performs systematic quantifier instantiation on a given quantified formula. Furthermore, FOSSIL includes a lemma synthesis technique for FO+lfp formulas, where we automatically synthesize inductive lemmas from a given theorem. Turning to first-order variants, we develop a tool for automatically verifying formulas in matching logic, a first-order variant with a least fixpoint operator which has a unified frame- work for specifications and proofs. We also present an efficient translation from matching logic (without least fixpoints) to first-order logic. This yields a completeness result for a fragment of matching logic formulas, while also allowing us to apply existing first-order reasoning tools and techniques, including the FOSSIL tool developed for systematic quantifier instantiation. Finally, we introduce a separation logic alternative known as frame logic, an extension of first-order logic with a construct that captures the implicit supports of formulas. Similar to matching logic, we show how frame logic can be converted to first-order logic with recursive definitions, where again we can directly apply other reasoning tools and techniques."],"dc:format":["application/pdf"],"dc:identifier":["https://hdl.handle.net/2142/115485"],"dc:language":["en","eng"],"dc:rights":["Copyright 2022 Lucas Peña"],"dc:subject":["first-order logic","verification","least fixpoints","matching logic","synthesis","separation logic"],"dc:title":["Advancements in automated first-order verification"],"dc:type":["text","Thesis"],"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:24:54Z"}