Cover Image

Invariant Checking for SMT-based Systems with Quantifiers

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Redondi, Gianluca, Cimatti, Alessandro, Griggio, Alberto, McMillan, Kenneth
Format:	Preprint
Published:	2024
Subjects:	Logic in Computer Science
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Towards the verification of a generic interlocking logic: Dafny meets parameterized model checking
by: Cimatti, Alessandro, et al.
Published: (2024)

Verification of Configurable SRA Systems
by: Cimatti, Alessandro, et al.
Published: (2026)

Complexity of the Model Checking problem for inquisitive propositional and modal logic
by: Grilletti, Gianluca, et al.
Published: (2024)

Lean-SMT: An SMT tactic for discharging proof goals in Lean
by: Mohamed, Abdalrhman, et al.
Published: (2025)

Property Checking Without Inductive Invariants
by: Goldberg, Eugene
Published: (2016)

System ASPMT2SMT:Computing ASPMT Theories by SMT Solvers
by: Bartholomew, Michael, et al.
Published: (2025)

SMT-based Symbolic Model-Checking for Operator Precedence Languages
by: Chiari, Michele, et al.
Published: (2024)

SMT with Uninterpreted Functions and Monotonicity Constraints in Systems Biology
by: Huvar, Ondřej, et al.
Published: (2026)

LLM2SMT: Building an SMT Solver with Zero Human-Written Code
by: Janota, Mikoláš, et al.
Published: (2026)

MCSat-based Finite Field Reasoning in the Yices2 SMT Solver
by: Hader, Thomas, et al.
Published: (2024)

An SMT Theory for n-Indexed Sequences
by: Hara, Hichem Rami Ait El, et al.
Published: (2024)

An SMT-LIB Theory of Finite Fields
by: Hader, Thomas, et al.
Published: (2024)

On SMT Theory Design: The Case of Sequences
by: Hara, Hichem Rami Ait El, et al.
Published: (2024)

Efficient Volume Computation for SMT Formulas
by: Shaw, Arijit, et al.
Published: (2025)

Hint-Based SMT Proof Reconstruction
by: Clune, Joshua, et al.
Published: (2026)

Number theory combination: natural density and SMT
by: Toledo, Guilherme V., et al.
Published: (2025)

Integer Reasoning Modulo Different Constants in SMT
by: Pertseva, Elizaveta, et al.
Published: (2025)

Project and Conquer: Fast Quantifier Elimination for Checking Petri Net Reachability
by: Amat, Nicolas, et al.
Published: (2024)

SMT-Layout: A MaxSMT-based Approach Supporting Real-time Interaction of Real-world GUI Layout
by: Li, Bohan, et al.
Published: (2024)

Towards SMT Solver Stability via Input Normalization
by: Amrollahi, Daneshvar, et al.
Published: (2024)

Towards Learning Infinite SMT Models (Work in Progress)
by: Janota, Mikoláš, et al.
Published: (2025)

Disjoint Projected Enumeration for SAT and SMT without Blocking Clauses
by: Spallitta, Giuseppe, et al.
Published: (2024)

A Relational Theory of Grounding and a new Grounder for SMT
by: Carbonnelle, Pierre
Published: (2026)

Synthesiz3 This: an SMT-Based Approach for Synthesis with Uncomputable Symbols
by: Hozzová, Petra, et al.
Published: (2025)

Portus: Linking Alloy with SMT-based Finite Model Finding
by: Dancy, Ryan, et al.
Published: (2024)

Loop Invariant Generation: A Hybrid Framework of Reasoning optimised LLMs and SMT Solvers
by: Bharti, Varun, et al.
Published: (2025)

SMT and Functional Equation Solving over the Reals: Challenges from the IMO
by: Brown, Chad E., et al.
Published: (2025)

A rewriting-logic-with-SMT-based formal analysis and parameter synthesis framework for parametric time Petri nets
by: Arias, Jaime, et al.
Published: (2024)

An Encoding for CLP Problems in SMT-LIB
by: Amrollahi, Daneshvar, et al.
Published: (2024)

SMT(LIA) Sampling with High Diversity
by: Lai, Yong, et al.
Published: (2025)

A Local Search Algorithm for MaxSMT(LIA)
by: He, Xiang, et al.
Published: (2024)

Logic-Parametric Neuro-Symbolic NLI: Controlling Logical Formalisms for Verifiable LLM Reasoning
by: Farjami, Ali, et al.
Published: (2026)

'Put the Car on the Stand': SMT-based Oracles for Investigating Decisions
by: Judson, Samuel, et al.
Published: (2023)

Multi-Structural Games and Number of Quantifiers
by: Fagin, Ronald, et al.
Published: (2021)

Beyond Eager Encodings: A Theory-Agnostic Approach to Theory-Lemma Enumeration in SMT
by: Civini, Emanuele, et al.
Published: (2026)

Approximate SMT Counting Beyond Discrete Domains
by: Shaw, Arijit, et al.
Published: (2025)

CIll: CTI-Guided Invariant Generation via LLMs for Model Checking
by: Su, Yuheng, et al.
Published: (2026)

Regular Model Checking Upside-Down: An Invariant-Based Approach
by: Esparza, Javier, et al.
Published: (2022)

Simplifying Safety Proofs with Forward-Backward Reasoning and Prophecy
by: Frenkel, Eden, et al.
Published: (2026)

Finding Photonics Circuits via $δ$-weakening SMT
by: Lewis, Marco, et al.
Published: (2025)