- Safety, Risk, Reliability and Quality
- Software
First-order logic, and quantifiers in particular, are widely used in deductive verification of
programs and systems. Quantifiers are essential for describing systems with unbounded domains,
but prove difficult for automated solvers. Significant effort has been dedicated to finding quantifier
instantiations that establish unsatisfiability of quantified formulas, thus ensuring validity of a
system’s verification conditions. However, in many cases the formulas are satisfiable—this is
often the case in intermediate steps of the verification process, e.g., when an invariant is not yet
inductive. For such cases, existing tools are limited to finding finite models as counterexamples.
Yet, some quantified formulas are satisfiable but only have infinite models, which current solvers
are unable to find. Such infinite counter-models are especially typical when first-order logic is used
to approximate the natural numbers, the integers, or other inductive definitions such as linked lists,
which is common in deductive verification. The inability of solvers to find infinite models makes
them diverge in these cases, providing little feedback to the user as they try to make progress in
their verification attempts.
In this paper, we tackle the problem of finding such infinite models, specifically, finite representations thereof that can be presented to the user of a deductive verification tool. These models give
insight into the verification failure, and allow the user to identify and fix bugs in the modeling of
the system and its properties. Our approach consists of three parts. First, we introduce symbolic
structures as a way to represent certain infinite models, and show they admit an efficient model
checking procedure. Second, we describe an effective model finding procedure that symbolically
explores a given (possibly infinite) family of symbolic structures in search of an infinite model for
a given formula. Finally, we identify a new decidable fragment of first-order logic that extends
and subsumes the many-sorted variant of EPR, where satisfiable formulas always have a model
representable by a symbolic structure within a known family, making our model finding procedure
a decision procedure for that fragment.
We evaluate our approach on examples from the domains of distributed consensus protocols
and of heap-manipulating programs (specifically, linked lists). Our implementation quickly finds
infinite counter-models that demonstrate the source of verification failures in a simple way, while
state-of-the-art SMT solvers and theorem provers such as Z3, cvc5, and Vampire diverge or return
“unknown”.
Need a simple solution for managing your BibTeX entries? Explore CiteDrive!
- Web-based, modern reference management
- Collaborate and share with fellow researchers
- Integration with Overleaf
- Comprehensive BibTeX/BibLaTeX support
- Save articles and websites directly from your browser
- Search for new articles from a database of tens of millions of references
Try out CiteDrive More from our Archive
-
DOI: 10.1145/3632882 2024
Polymorphic Type Inference for Dynamic Languages
Giuseppe Castagna, Mickaël Laurent, Kim Nguyễn
-
DOI: 10.1111/risa.14272 2024
The 8 billion milestone: Risk perceptions of global population growth among UK and US residents
Ian G. J. Dawson, Danni Zhang
-
DOI: 10.4271/15-17-02-0010 2024
Torque Converter Dynamic Characterization Using Torque
Transmissibility Frequency Response Functions: Locked Clutch
Operation
Luke Jurmu, Darrell Robinette, Jason Blough, Craig Reynolds
-
DOI: 10.3390/fire7010024 2024
Explosive Characteristics Analysis of Gasoline–Air Mixtures within Horizontal Oil Tanks
Xinsheng Jiang, Dongliang Zhou, Peili Zhang, Yunxiong Cai, Ri Chen, Donghai He, Xizhuo Qin, Keyu Lin, Sai Wang
-
DOI: 10.3390/safety10010012 2024
A Cross-Sectional Observational Pilot Study of the Main Risk Factors Related to Lower Back Pain in Spanish Hospitality Workers
Melania Zamorano García, Gema Santamaría, Marina Seco-Casares, Ana M. Celorrio San Miguel, Eva Lantarón-Caeiro, Juan F. García, Diego Fernández-Lázaro
-
DOI: 10.3390/fire7010023 2024
Knowledge Mapping for Fire Risk Assessment: A Scientometric Analysis Based on VOSviewer and CiteSpace
Zhixin Tang, Tianwei Zhang, Lizhi Wu, Shaoyun Ren, Shaoguang Cai
-
DOI: 10.3390/civileng5010003 2024
High Glass Waste Incorporation towards Sustainable High-Performance Concrete
Othon Moreira, Aires Camões, Raphaele Malheiro, Carlos Jesus
-
DOI: 10.3390/civileng5010004 2024
Factors Affecting Properties of Polymer Grouted Sands
Costas A. Anagnostopoulos, Vasilios Aggelidis
-
DOI: 10.3390/safety10010011 2024
Nonlinear Analysis of the Effects of Socioeconomic, Demographic, and Technological Factors on the Number of Fatal Traffic Accidents
Nassim Sohaee, Shahram Bohluli
-
DOI: 10.1002/prs.12563 2024
Damage mitigation method studies through simulation modeling of chemical accidents
Sehyeon Oh, Junseo Lee, Byungchol Ma