18 citations · 22 across the 16 of their papers we have counts for
7 papers · 1 filter
The Power of Regular Constraint Propagation (Technical Report)
Matthew Hague, Artur Jeż, Anthony W. Lin +2
The past decade has witnessed substantial developments in string solving. Motivated by the complexity of string solving strategies adopted in existing string solvers, we investigat…
HornStr: Invariant Synthesis for Regular Model Checking as Constrained Horn Clauses(Technical Report)
Hongjian Jiang, Anthony W. Lin, Oliver Markgraf +2
We present HornStr, the first solver for invariant synthesis for Regular Model Checking (RMC) with the specification provided in the SMT-LIB 2.6 theory of strings. It is well-known…
A Program Instrumentation Framework for Automatic Verification
Jesper Amilon, Zafer Esen, Dilian Gurov +3
In deductive verification and software model checking, dealing with certain specification language constructs can be problematic when the back-end solver is not sufficiently powerf…
An Encoding for CLP Problems in SMT-LIB
Daneshvar Amrollahi, Hossein Hojjat, Philipp Rümmer
The input language for today's CHC solvers are commonly the standard SMT-LIB format, borrowed from SMT solvers, and the Prolog format that stems from Constraint-Logic Programming (…
Decision Procedures for Sequence Theories (Technical Report)
Artur Jeż, Anthony W. Lin, Oliver Markgraf +1
Sequence theories are an extension of theories of strings with an infinite alphabet of letters, together with a corresponding alphabet theory (e.g. linear integer arithmetic). Sequ…
OptiRica: Towards an Efficient Optimizing Horn Solver
Hossein Hojjat, Philipp Rümmer
This paper describes an ongoing effort to develop an optimizing version of the Eldarica Horn solver. The work starts from the observation that many kinds of optimization problems,…