Stream−based Randomised Language Models for SMT by Levenberg, A, Osborne, M

SMT-based model checking of max-plus linear systems by Mufid, MSU, Micheli, A, Abate, A, Cimatti, A

“…The algorithms are cast in the setting of SMT-based verification of infinite-state transition systems over the reals, with variants depending on the (incremental vs upfront) computation of the bound, and on the (explicit vs implicit) unrolling of the transition relation. …”

SMT-based verification applied to non-convex optimization problems by Araujo, R, Bessa, I, Cordeiro, L, Filho, J

“…This paper presents a novel, complete, and flexible optimization algorithm, which relies on recursive executions that re-constrains a model-checking procedure based on Satisfiability Modulo Theories (SMT). This SMT-based optimization technique is able to optimize a wide range of functions, including non-linear and non-convex problems using fixed-point arithmetic. …”

Computation of the transient in max-plus linear systems via SMT-solving by Abate, A, Cimatti, A, Micheli, A, Mufid, MS

“…This paper proposes a new approach, grounded in Satisfiability Modulo Theories (SMT), to study the transient of a Max-Plus Linear (MPL) system, that is the number of steps leading to its periodic regime. …”

Don't care in SMT—Building flexible yet efficient abstraction/refinement solvers by Bauer, A, Leucker, M, Schallhart, C, Tautschnig, M

On partial order semantics for SAT/SMT-based symbolic encodings of weak memory concurrency by Horn, A, Kroening, D

“…Among these, symbolic techniques have been shown to be particularly effective at finding concurrency-related bugs because they can leverage highly optimized decision procedures such as SAT/SMT solvers. This paper gives new fundamental results on partial order semantics for SAT/SMT-based symbolic encodings of weak memory concurrency. …”

Encoding floating-points using the SMT theory in ESBMC: An empirical evaluation over the SV-COMP benchmarks by Gadelha, M, Cordeiro, L, Nicole, D

“…This paper describes the support for encoding C/C++ programs using the SMT theory of floating-point numbers in ESBMC: an SMT-based context-bounded model checker that provides bit-precise verification of C and C++ programs. …”

Counterexample guided inductive optimization applied to mobile robots path planning by Araújo, R, Ribeiro, A, Bessa, I, Cordeiro, L, Chaves Filho, J

“…In particular, CEGIO has been successfully applied to obtain optimal two-dimensional paths for autonomous mobile robots using off-the-shelf SAT and SMT solvers.…”

Learning probabilistic termination proofs by Abate, A, Giacobbe, M, Roy, D

“…We introduce the neural ranking supermartingale: we let a neural network fit an RSM over execution traces and then we verify it over the source code using satisfiability modulo theories (SMT); if the latter step produces a counterexample, we generate from it new sample traces and repeat learning in a counterexample-guided inductive synthesis loop, until the SMT solver confirms the validity of the RSM. …”

Algebraic Techniques in Software Verification : Challenges and Opportunities by Brain, M, Kroening, D, McCleeary, R

“…One of the main application areas and driving forces behind the development of Satisfiability Modulo Theory (SMT) solvers is software verification. The requirements of software verification are somewhat different to other applications of automated reasoning, posing a number of challenges but also providing some interesting opportunities. …”

PASS: Abstraction Refinement for Infinite Probabilistic Models by Hahn, E, Hermanns, H, Wachter, B, Zhang, L

“…The computational engines we use are SMT solvers to compute finite abstractions, numerical methods to compute probabilities and interpolation as part of abstraction refinement. sf PASS has been successfully applied to network protocols and serves as a test platform for different refinement methods…”

Interpolation-based verification of floating-point programs with abstract CDCL by Brain, M, D'Silva, V, Griggio, A, Haller, L, Kroening, D

“…One approach for smt solvers to improve efficiency is to delegate reasoning to abstract domains. …”

Equivalence checking using trace partitioning by Mukherjee, R, Kroening, D, Melham, T, Srivas, M

“…The approach generates many but tractable SAT/SMT queries. We present experimental data quantifying the benefit of our partitioning method for both combinational and sequential equivalence checking of difficult arithmetic circuits and control-intensive circuits.…”

An abstract interpretation of DPLL(T) by Brain, M, D'Silva, V, Haller, L, Griggio, A, Kroening, D

“…DPLL(T) is a central algorithm for Satisfiability Modulo Theories (SMT) solvers. The algorithm combines results of reasoning about the Boolean structure of a formula with reasoning about conjunctions of theory facts to decide satisfiability. …”

Formal verification of bit-vector invertibility conditions in Coq by Ekici, B, Viswanathan, A, Zohar, Y, Tinelli, C, Barrett, C

“…We prove the correctness of invertibility conditions for the theory of fixed-width bit-vectors—used to solve quantified bit-vector formulas in the Satisfiability Modulo Theories (SMT) solver cvc5— in the Coq proof assistant. Previous work proved many of these in a completely automatic fashion for arbitrary bit-width; however, some were only proved for bit-widths up to 65, even though they are being used to solve formulas over larger bit-widths. …”

Abstract Satisfaction by D'Silva, V, Haller, L, Kroening, D

“…This article introduces an abstract interpretation framework that codifies the operations in SAT and SMT solvers in terms of lattices, transformers and fixed points. …”

Deciding Floating−Point Logic with Systematic Abstraction by Haller, L, Griggio, A, Brain, M, Kroening, D

“…We present a natural-domain SMT approach that lifts the CDCL framework to operate directly over abstractions of floating-point assignments. …”

'Cause I'm Strong Enough: Reasoning about consistency choices in distributed systems by Yang, H, Gotsman, A, Ferreira, C, Najafzadeh, M, Shapiro, M

“…This leads to simple reasoning, which we have automated in an SMT-based tool. We present a nontrivial proof of soundness of our rule and illustrate its use on several examples.…”

Syntax-guided optimal synthesis for chemical reaction networks by Cardelli, L, Ceska, M, Fraenzle, M, Kwiatkowska, M, Laurenti, L, Paoletti, N, Whitby, M

“…We design and implement a novel algorithm for the optimal synthesis of CRNs that employs almost complete refutation procedure for SMT over reals and ODEs, and exploits a meta-sketching abstraction controlling the search strategy. …”

ERODE: A tool for the evaluation and reduction of ordinary differential equations by Cardelli, L, Tribastone, M, Tschaikowski, M, Vandin, A

“…As back-end ERODE uses the well-known Z3 SMT solver to compute the largest equivalence that refines a given initial partition of ODE variables. …”