Proving LTL Properties of Bitvector Programs and Decompiled Binaries

DOI10.1007/978-3-030-89051-3_16MaRDI QIDQ6488162zbMATH OpenFDO

Authors Daniel Dietsch, Eric Koskinen, Ton Chanh Le, Georgios Portokalidis, Jun Xu

Publication date 29 March 2023

Full work available at URL https://doi.org/10.1007/978-3-030-89051-3_16

Mathematics Subject Classification ID

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

Recommendations

• Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic
• LCF-style bit-blasting in HOL4
• Deciding Bit-Vector Arithmetic with Abstraction
• A Decision Procedure for Bit-Vectors and Arrays
• Mind the gap: bit-vector interpolation recast over linear integer arithmetic

Cites work

• scientific article; zbMATH DE number 1903378 (Why is no real title available?)
• Analyzing program termination and complexity automatically with \textsf{AProVE}
• Deciding Bit-Vector Arithmetic with Abstraction
• Efficiently solving quantified bit-vector formulas
• Geometric nontermination arguments
• Hoare Logic for Realistically Modelled Machine Code
• Making prophecies with decision predicates
• Proving termination of programs with bitvector arithmetic by symbolic execution
• Ranking function synthesis for bit-vector relations
• Tools and Algorithms for the Construction and Analysis of Systems
• Towards bit-width-independent proofs in SMT solvers

Cited in

(1)

• Commutativity for concurrent program termination proofs

This page was built for publication: Proving LTL Properties of Bitvector Programs and Decompiled Binaries

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