Encoding RTL constructs for \textsc{MathSAT}: a preliminary report

zbMATH Open1272.68230MaRDI QIDQ2848685FDOQ2848685

Authors: Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Ziyad Hanna, Amit Palti, Roberto Sebastiani, Zurab Khasidashvili 

Publication date: 26 September 2013

Full work available at URL: http://www.sciencedirect.com/science/article/pii/S157106610600003X

Recommendations

• M\textbf{ath}SAT: Tight integration of SAT and mathematical decision procedures
• Using word-level information in formal hardware verification
• scientific article; zbMATH DE number 2084774
• Verifying industrial hybrid systems with \textsc{MathSAT}
• The MathSAT5 SMT solver

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Cited In (3)

• Towards satisfiability modulo parametric bit-vectors
• Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis
• Optimization modulo the theories of signed bit-vectors and floating-point numbers

This page was built for publication: Encoding RTL constructs for \textsc{MathSAT}: a preliminary report

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