1 citations · 2 across the 7 of their papers we have counts for
7 papers
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…
Probabilistic Bisimulation for Parameterized Anonymity and Uniformity Verification
Chih-Duo Hong, Anthony W. Lin, Philipp Rümmer +1
Bisimulation is crucial for verifying process equivalence in probabilistic systems. This paper presents a novel logical framework for analyzing bisimulation in probabilistic parame…
Sound and Complete Invariant-Based Heap Encodings (Technical Report)
Zafer Esen, Philipp Rümmer, Tjark Weber
Verification of programs operating on heap-allocated data structures, for instance lists or trees, poses significant challenges due to the potentially unbounded size of such data s…
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…
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,…