Bit-Vector CHC Solving for Binary Analysis and Binary Analysis for Bit-Vector CHC Solving

Aaron Bembenek, Toby Murray

For high-assurance software, source-level reasoning is insufficient: we need binary-level guarantees. Despite constrained Horn clause (CHC) solving being one of the most popular fo…