Showing 2026Show all
2 papers · 1 filter
cs.PL2026
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…
cs.LG2026
Lipschitz-Based Robustness Certification Under Floating-Point Execution
Toby Murray
Lipschitz-based robustness certification bounds a network's sensitivity through concrete numerical computation rather than symbolic reasoning, and so scales efficiently. It is incr…