Advancements in automated first-order verification

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.

Name thesis:degree_name

Ph.D.

Level thesis:degree_level

Dissertation

Discipline thesis:degree_discipline

Computer Science

Grantor

University of Illinois at Urbana-Champaign

Year dc:date

2022

Author dc:creator

• Pena, Lucas

Contributors dc:contributor

• Rosu, Grigore
• Parthasarathy, Madhusudan
• Meseguer, José
• Löding, Christof

• first-order logic
• verification
• least fixpoints
• matching logic
• synthesis
• separation logic

Statement dc:rights

• Copyright 2022 Lucas Peña

Language dc:language

en, eng

Handle dc:identifier

https://hdl.handle.net/2142/115485

OAI record oai:identifier

https://www.ideals.illinois.edu/oai-pmh?verb=GetRecord&metadataPrefix=etdms&identifier=oai%3Awww.ideals.illinois.edu%3A2142%2F115485