23 citations · 34 across the 8 of their papers we have counts for
10 papers
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…
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…
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 (…
Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes
Ahmed Bouajjani, Wael-Amine Boutglay, Peter Habermehl
We propose a data-driven algorithm for numerical invariant synthesis and verification. The algorithm is based on the ICE-DT schema for learning decision trees from samples of posit…
On Presburger arithmetic extended with non-unary counting quantifiers
Peter Habermehl, Dietrich Kuske
We consider a first-order logic for the integers with addition. This logic extends classical first-order logic by modulo-counting, threshold-counting and exact-counting quantifiers…
Left-eigenvectors are certificates of the Orbit Problem
Steven de Oliveira, Virgile Prevosto, Peter Habermehl +1
This paper investigates the connexion between the Kannan-Lipton Orbit Problem and the polynomial invariant generator algorithm PILA based on eigenvectors computation. Namely, we re…
Model-checking Counting Temporal Logics on Flat Structures
Normann Decker, Peter Habermehl, Martin Leucker +2
We study several extensions of linear-time and computation-tree temporal logics with quantifiers that allow for counting how often certain properties hold. For most of these extens…
A Robust Class of Data Languages and an Application to Learning
Benedikt Bollig, Peter Habermehl, Martin Leucker +1
We introduce session automata, an automata model to process data words, i.e., words over an infinite alphabet. Session automata support the notion of fresh data values, which are w…
On the Path-Width of Integer Linear Programming
Constantin Enea, Peter Habermehl, Omar Inverso +1
We consider the feasibility problem of integer linear programming (ILP). We show that solutions of any ILP instance can be naturally represented by an FO-definable class of graphs.…
Ordered Navigation on Multi-attributed Data Words
Normann Decker, Peter Habermehl, Martin Leucker +1
We study temporal logics and automata on multi-attributed data words. Recently, BD-LTL was introduced as a temporal logic on data words extending LTL by navigation along positions…