Advancements in automated first-order verification

Pena, Lucas

Permalink

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

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

Copyright and License Information

Copyright 2022 Lucas Peña

Owning Collections