arXiv preprint ·
Quantifying SMT Solver Instability for Formal Verification
- Published
- Source
- arXiv preprint, posted before peer review
- Original
- Read it at arXiv
- Topics
Abstract
Program verification has become commonplace in software development projects, and much of its feasibility can be attributed to the potential of SMT solvers to automate model checking and other verification techniques. However, SMT instability, a phenomenon where semantically equivalent permutations of source code take much longer to solve or timeout, has been found to interrupt workflows and make software engineers more likely to avoid verification. Previous efforts to measure SMT instability have had difficulty quantifying it due to the abnormal runtime distributions it produces. In this paper, we use the coefficient of variation to model instability across an extensive dataset of SMT queries from three software domains. Our results show that SMT instability is significant in each area, and that it increases for queries that take longer on average. However, using a novel method to quantify instability, we show that a different approach is possible: if a solution were to optimize the structure of queries for runtime, rather than variance, instability could be mitigated while also improving overall solver performance.
The authors’ abstract, as arXiv lists it. arXiv’s listings, abstracts included, are free for anyone to reuse.
Read it on ReadSearch
Each opens after you create an account, and brings you back to this paper.
More in Software Engineering
Following Breadcrumbs in Code: What Accidentally Committed Ad-Hoc Logs Reveal about Developer Comprehension
Co-Modifying Application Code and Deployment Infrastructure: A Causal Study of AI Agent Pull Requests
IRONPROOF: COBOL-to-Python Transpilation with SMT-Based Equivalence Checking
Evaluation of Software Quality Through Refactoring Commit-Impact Analysis
Skill Constellations: Tracing the Supply Chain of Agent Skills on GitHub
Get the few papers worth your time in Software Engineering every morning.
ReadSearch reads the new papers in your field each day and brings you the few worth reading, each with its key finding in a sentence.