On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic

DOI10.1007/978-3-662-44465-8_41MaRDI QIDQ2922635zbMATH OpenOpenAlexFDO

Authors Gergely Kovásznai, Helmut Veith, Andreas Fröhlich, Armin Biere

Publication date 14 October 2014

Published in Mathematical Foundations of Computer Science 2014 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-662-44465-8_41

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Logic in computer science (03B70) Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Analysis of algorithms and problem complexity (68Q25) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Complexity of fixed-size bit-vector logics
• Termination and complexity analysis for programs with bitvector arithmetic by symbolic execution
• More on the complexity of quantifier-free fixed-size bit-vector logics with binary encoding
• Proof Complexity of Quantified Boolean Logic — A Survey
• Towards satisfiability modulo parametric bit-vectors
• Proving termination of programs with bitvector arithmetic by symbolic execution
• Proof complexity of symbolic QBF reasoning
• Solving quantified bit-vector formulas using binary decision diagrams
• scientific article; zbMATH DE number 5917352

Cited in

(4)

• On the complexity of the quantified bit-vector arithmetic with binary encoding
• Deciding Bit-Vector Formulas with mcSAT
• More on the complexity of quantifier-free fixed-size bit-vector logics with binary encoding
• Complexity of fixed-size bit-vector logics

This page was built for publication: On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic

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