3 papers
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…
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.PL2025
A Formally Verified Robustness Certifier for Neural Networks (Extended Version)
James Tobler, Hira Taqdees Syeda, Toby Murray
Neural networks are often susceptible to minor perturbations in input that cause them to misclassify. A recent solution to this problem is the use of globally-robust neural network…