4 papers
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…
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…
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…
Symbol Correctness in Deep Neural Networks Containing Symbolic Layers
Aaron Bembenek, Toby Murray
To handle AI tasks that combine perception and logical reasoning, recent work introduces Neurosymbolic Deep Neural Networks (NS-DNNs), which contain -- in addition to traditional n…