3 papers
cs.FL2026
Passive Learning of Symbolic Automata over Monotonic Algebras
Erwann Loulergue, Peter Habermehl
Symbolic automata extend classical finite-state automata to handle large or infinite alphabets by labeling transitions by predicates coming from a boolean algebra. Many results fro…
cs.PL2025
Data-driven Verification of Procedural Programs with Integer Arrays
Ahmed Bouajjani, Wael-Amine Boutglay, Peter Habermehl
We address the problem of verifying automatically procedural programs manipulating parametric-size arrays of integers, encoded as a constrained Horn clauses solving problem. We pro…
cs.LO2024
Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic (Technical Report)
Peter Habermehl, VojtÄch Havlena, Michal HeÄko +2
We present a new angle on solving quantified linear integer arithmetic based on combining the automata-based approach, where numbers are understood as bitvectors, with ideas from (…