2 papers
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.AI2025
Current Practices for Building LLM-Powered Reasoning Tools Are Ad Hoc -- and We Can Do Better
Aaron Bembenek
There is growing excitement about building software verifiers, synthesizers, and other Automated Reasoning (AR) tools by combining traditional symbolic algorithms and Large Languag…