Automatic abstraction for bit-vectors using decision procedures

MaRDI QIDQ5248942zbMATH OpenFDO

Authors Jörg Brauer

Publication date 28 April 2015

Full work available at URL http://d-nb.info/1051415233/34

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to computer science (68-02) General topics in the theory of software (68N01) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Automatic abstraction for intervals using Boolean formulae
• Deciding Bit-Vector Arithmetic with Abstraction
• Automating abstract interpretation
• scientific article; zbMATH DE number 1953018
• Sound bit-precise numerical domains

Cited in

(7)

• Abstract interpretation of microcontroller code: intervals meet congruences
• Range and set abstraction using SAT
• Verified abstract interpretation techniques for disassembling low-level self-modifying code
• Block-wise abstract interpretation by combining abstract domains with SMT
• Sound bit-precise numerical domains
• Automatic abstraction for intervals using Boolean formulae
• Transfer function synthesis without quantifier elimination

This page was built for publication: Automatic abstraction for bit-vectors using decision procedures

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