OpenSMT2: an SMT solver for multi-core and cloud computing

DOI10.1007/978-3-319-40970-2_35MaRDI QIDQ2818042zbMATH OpenOpenAlexFDO

Authors Antti E. J. Hyvärinen, Matteo Marescotti, Leonardo Alt, Natasha Sharygina

Publication date 5 September 2016

Published in Theory and Applications of Satisfiability Testing – SAT 2016 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-40970-2_35

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Parallel algorithms in computer science (68W10) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Search-space partitioning for parallelizing SMT solvers
• Parallelizing SMT solving: lazy decomposition and conciliation
• \texttt{SMT-RAT}: an open source \texttt{C++} toolbox for strategic and parallel SMT solving
• Computer Aided Verification
• The MathSAT5 SMT solver

Cites work

• PeRIPLO: a framework for producing effective interpolants in SAT-based software verification
• Search-space partitioning for parallelizing SMT solvers
• Simplify: a theorem prover for program checking
• eVolCheck: incremental upgrade checker for C

Cited in

(13)

• Farkas-based tree interpolation
• Lattice-based refinement in bounded model checking
• Search-space partitioning for parallelizing SMT solvers
• \texttt{SMT-RAT}: an open source \texttt{C++} toolbox for strategic and parallel SMT solving
• SMT-based verification of program changes through summary repair
• scientific article; zbMATH DE number 7453201 (Why is no real title available?)
• \textsc{Carcara}: an efficient proof checker and elaborator for SMT proofs in the Alethe format
• The \textsc{Golem} Horn solver
• Transition power abstractions for deep counterexample detection
• An interdisciplinary experimental evaluation on the disjunctive temporal problem
• scientific article; zbMATH DE number 7806143 (Why is no real title available?)
• Exploiting partial variable assignment in interpolation-based model checking
• Extending the fundamental theorem of linear programming for strict inequalities

Describes a project that uses

Uses Software

• SIMPLIFY
• FunFrog
• PeRIPLO
• OpenSMT
• eVolCheck
• OpenSMT2

This page was built for publication: OpenSMT2: an SMT solver for multi-core and cloud computing

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2818042)