A Decision Procedure for Bit-Vectors and Arrays
From MaRDI portal
Publication:5429343
DOI10.1007/978-3-540-73368-3_52zbMath1135.68472OpenAlexW2129487583MaRDI QIDQ5429343
Publication date: 29 November 2007
Published in: Computer Aided Verification (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-540-73368-3_52
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (31)
Combining SAT solvers with computer algebra systems to verify combinatorial conjectures ⋮ A layered algorithm for quantifier elimination from linear modular constraints ⋮ Satisfiability Modulo Theories ⋮ MathCheck: A Math Assistant via a Combination of Computer Algebra Systems and SAT Solvers ⋮ Automatic search for bit-based division property ⋮ A bit-vector differential model for the modular addition by a constant and its applications to differential and impossible-differential cryptanalysis ⋮ Simulating circuit-level simplifications on CNF ⋮ Satisfiability Checking: Theory and Applications ⋮ Incremental SAT-Based Method with Native Boolean Cardinality Handling for the Hamiltonian Cycle Problem ⋮ Propagation based local search for bit-precise reasoning ⋮ On the field-based division property: applications to MiMC, Feistel MiMC and GMiMC ⋮ Related-key differential cryptanalysis of GMiMC used in post-quantum signatures ⋮ Parameterized synthesis for fragments of first-order logic over data words ⋮ A bit-vector differential model for the modular addition by a constant ⋮ Efficiently solving quantified bit-vector formulas ⋮ Symbolic Execution as DPLL Modulo Theories ⋮ Local search with a SAT oracle for combinatorial optimization ⋮ Complexity of fixed-size bit-vector logics ⋮ Parallelizing SMT solving: lazy decomposition and conciliation ⋮ Highly Automated Formal Proofs over Memory Usage of Assembly Code ⋮ Z3str2: an efficient solver for strings, regular expressions, and length constraints ⋮ Sharpening constraint programming approaches for bit-vector theory ⋮ Cryptanalysis of Ascon ⋮ The SAT+CAS method for combinatorial search with applications to best matrices ⋮ Optimization modulo the theories of signed bit-vectors and floating-point numbers ⋮ Automatic Differential Analysis of ARX Block Ciphers with Application to SPECK and LEA ⋮ Deciding Bit-Vector Formulas with mcSAT ⋮ Optimization modulo the theory of floating-point numbers ⋮ STP ⋮ Wombit: a portfolio bit-vector solver using word-level propagation ⋮ Array theory of bounded elements and its applications
Uses Software
This page was built for publication: A Decision Procedure for Bit-Vectors and Arrays
