3 papers
cs.SE2026
Neuro-Symbolic Software Verification: Hyper-charging Local Language Models with Symbolic Reasoning at Scale
Muhammad A. A. Pirzada, Julian Parsert, Weiqi Wang +2
Loop invariant synthesis remains a central and pivotal bottleneck in formal software verification. Recent LLM-based Neuro-Symbolic tools have achieved impressive solve rates. Howev…
cs.LO2026
One is all you need: Second-order Unification without First-order Variables
David M. Cerna, Julian Parsert
We introduce a fragment of second-order unification, referred to as \emph{Second-Order Ground Unification (SOGU)}, with the following properties: (i) only one second-order variable…
cs.AI2025
Extracting Robust Register Automata from Neural Networks over Data Sequences
Chih-Duo Hong, Hongjian Jiang, Anthony W. Lin +3
Automata extraction is a method for synthesising interpretable surrogates for black-box neural models that can be analysed symbolically. Existing techniques assume a finite input a…