University of Illinois Urbana-Champaign

Advancements in automated first-order verification

Pena, Lucas

Content Files
PENA-DISSERTATION-2022.pdf

Permalink

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

Description

Title
Advancements in automated first-order verification
Author(s)
Pena, Lucas
Issue Date
2022-04-19
Director of Research (if dissertation) or Advisor (if thesis)
Rosu, Grigore
Doctoral Committee Chair(s)
Rosu, Grigore
Committee Member(s)
  • Parthasarathy, Madhusudan
  • Meseguer, José
  • Löding, Christof
Department of Study
Computer Science
Discipline
Computer Science
Degree Granting Institution
University of Illinois at Urbana-Champaign
Degree Name
Ph.D.
Degree Level
Dissertation
Keyword(s)
  • first-order logic
  • verification
  • least fixpoints
  • matching logic
  • synthesis
  • separation logic
Abstract
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.
Graduation Semester
2022-05
Type of Resource
Thesis
Handle URL
https://hdl.handle.net/2142/115485
Copyright and License Information
Copyright 2022 Lucas Peña

Owning Collections

Graduate Dissertations and Theses at Illinois PRIMARY
Graduate Theses and Dissertations at Illinois