Repository logo

Infoscience

  • English
  • French
Log In
Logo EPFL, École polytechnique fédérale de Lausanne

Infoscience

  • English
  • French
Log In
  1. Home
  2. Academic and Research Output
  3. Conferences, Workshops, Symposiums, and Seminars
  4. A Conjecture Regarding SMT Instability
 
conference paper

A Conjecture Regarding SMT Instability

Cebeci, Can  
•
Bjørner, Nikolaj
•
Candea, George  
Show more
Hoenicke, Jochen
•
Janota, Mikolas
Show more
2025
23 Joint of the International Workshop on Satisfiability Modulo Theories and the Pragmatics of SAT International Workshop

Automated verifiers rely on SMT solvers as a backend for proof automation. This simplifies verification in the common case, but also creates usability challenges due to instability. Previous work proposes mitigation strategies motivated by the assumption that instability is a fundamental theoretical limitation. We conjecture that the instability experienced by verifiers today is often caused by fixable engineering problems, and is thus not fundamental. Should this be true, the more consequential approach to addressing instability would be to identify root causes and connect them with solver improvements. We conducted case studies on 11 deemed-unstable queries from existing verification projects and from issues reported on the Z3 repository, with the goal of diagnosing the root causes of instability. For all of them, instability is attributable to solver bugs, misconfiguration, or misaligned expectations. We present our analysis and draw conclusions regarding better instability metrics, interfaces that make instability explicit, systematic debugging methods, and easier-to-debug SMT solvers.

  • Files
  • Details
  • Metrics
Loading...
Thumbnail Image
Name

SMT_paper21.pdf

Type

Main Document

Version

Published version

Access type

openaccess

License Condition

CC BY

Size

1.25 MB

Format

Adobe PDF

Checksum (MD5)

50e222eaa59ddbb5b9f36cbf98f6acc3

Logo EPFL, École polytechnique fédérale de Lausanne
  • Contact
  • infoscience@epfl.ch

  • Follow us on Facebook
  • Follow us on Instagram
  • Follow us on LinkedIn
  • Follow us on X
  • Follow us on Youtube
AccessibilityLegal noticePrivacy policyCookie settingsEnd User AgreementGet helpFeedback

Infoscience is a service managed and provided by the Library and IT Services of EPFL. © EPFL, tous droits réservés