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

MaRDI QIDQ2848685zbMATH OpenFDO

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

Mathematics Subject Classification ID

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

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

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)