4 papers
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…
Synthesis and Verification of Register Automata over Data Sequences (Technical Report)
Chih-Duo Hong, Hongjian Jiang, Anthony W. Lin +3
Data sequences, such as time series, traces, and sensor streams, are words over large or infinite data domains. Their properties often depend on comparisons between values at diffe…
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…
Linear Programming in Isabelle/HOL
Julian Parsert
Linear programming describes the problem of optimising a linear objective function over a set of constraints on its variables. In this paper we present a solver for linear programs…