• Spacer

  • Referenced in 8 articles [sw19496]
  • present an SMT-based symbolic model checking algorithm for safety verification of recursive programs ... modular and analyzes procedures individually. Unlike other SMT-based approaches, it maintains both over...
  • nuXmv

  • Referenced in 20 articles [sw18526]
  • nuXmv with state-of-the-art verification algorithms. For infinite-state systems, it extends ... Reals, and it provides advanced SMT-based model checking techniques. Besides extended functionalities, nuXmv ... been used in several industrial projects as verification back-end, and it is the basis...
  • HyComp

  • Referenced in 1 article [sw20163]
  • system, which can be analyzed using SMT-based verification techniques (e.g. BMC, K-induction...
  • KRATOS

  • Referenced in 7 articles [sw07808]
  • users to explore two directions in the verification. First, by relying on the translation from ... uses state-of-the-art SMT-based techniques for program abstractions and refinements...
  • SYMBA

  • Referenced in 11 articles [sw08528]
  • verification, program synthesis, functional programming, refinement types, etc. In all of these applications, SMT solvers ... SMT solvers offer such optimization capabilities. In this paper, we present SYMBA, an efficient SMT ... based optimization algorithm for objective functions in the theory of linear real arithmetic (LRA). Given...
  • LiquidHaskell

  • Referenced in 2 articles [sw27633]
  • Refinement types for Haskell. SMT-based checking of refinement types for call-by-value languages ... classical translation of refinement types to verification conditions is unsound under lazy evaluation. When checking...
  • Marabou

  • Referenced in 2 articles [sw31368]
  • Marabou Framework for Verification and Analysis of Deep Neural Networks. Deep neural networks are revolutionizing ... deep neural networks. Marabou is an SMT-based tool that can answer queries about...
  • STABLE

  • Referenced in 2 articles [sw11913]
  • verification problems combining Boolean reasoning with computer algebra. This paper presents a new SMT solver ... algebra-based engine which provides algorithms for simplifying arithmetic problems of an SMT instance prior ... domain for STABLE we target an SMT-based property checking flow for System-on-Chip ... SMT solvers on a large collection of SMT formulas describing verification problems of industrial data...
  • Z34Bio

  • Referenced in 1 article [sw25444]
  • Z34Bio (Z3 for Biology), a unified SMT-based framework for the automated analysis of natural ... case-studies which we make available as SMT-LIB benchmarks, to enable comparison of different ... this new domain accessible to the formal verification community...
  • HySAT

  • Referenced in 23 articles [sw01980]
  • HySAT: An efficient proof engine for bounded model...
  • TASS

  • Referenced in 2 articles [sw02740]
  • TASS (Timing Analyzer of Scenario-based Specifications) is...
  • HyTech

  • Referenced in 320 articles [sw04125]
  • HyTech is an automatic tool for the analysis...
  • NuSMV

  • Referenced in 288 articles [sw04131]
  • NuSMV is a symbolic model checker developed as...
  • MathSAT

  • Referenced in 56 articles [sw09449]
  • The MathSAT 4 SMT Solver. We present MathSAT...
  • HyDI

  • Referenced in 3 articles [sw11912]
  • HyDI: a language for symbolic hybrid systems with...
  • Cubicle

  • Referenced in 11 articles [sw13778]
  • Cubicle: a parallel smt-based model checker for...
  • SAFARI

  • Referenced in 8 articles [sw28669]
  • SAFARI: SMT-Based Abstraction for Arrays with Interpolants...