29 citations · 102 across the 28 of their papers we have counts for
22 papers · 1 filter
Symbolic Execution of Constrained Horn Clauses
Johannes Weiser, Zafer Esen, Philipp Rümmer
Constrained Horn clauses (CHCs) are a fragment of first-order logic widely used as an intermediate language for verification. We study constrained resolution as a calculus for reas…
Craig Interpolation in Program Verification
Philipp Rümmer
Craig interpolation is used in program verification for automating key tasks such as the inference of loop invariants and the computation of program abstractions. This chapter cove…
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…
Competition Report: CHC-COMP-21
Grigory Fedyukovich, Philipp Rümmer
CHC-COMP-21 is the fourth competition of solvers for Constrained Horn Clauses. In this year, 7 solvers participated at the competition, and were evaluated in 7 separate tracks on p…
A Theory of Heap for Constrained Horn Clauses (Extended Technical Report)
Zafer Esen, Philipp Rümmer
Constrained Horn Clauses (CHCs) are an intermediate program representation that can be generated by several verification tools, and that can be processed and solved by a number of…
String Constraints with Concatenation and Transducers Solved Efficiently (Technical Report)
Lukas Holik, Petr Janku, Anthony W. Lin +2
String analysis is the problem of reasoning about how strings are manipulated by a program. It has numerous applications including automatic detection of cross-site scripting (XSS)…
Competition Report: CHC-COMP-20
Philipp Rümmer
CHC-COMP-20 is the third competition of solvers for Constrained Horn Clauses. In this year, 9 solvers participated at the competition, and were evaluated in four separate tracks on…
A Decision Procedure for Path Feasibility of String Manipulating Programs with Integer Data Type
Taolue Chen, Matthew Hague, Jinlong He +4
Strings are widely used in programs, especially in web applications. Integer data type occurs naturally in string-manipulating programs, and is frequently used to refer to lengths…
Regular Model Checking Revisited (Technical Report)
Anthony W. Lin, Philipp Rümmer
In this contribution we revisit regular model checking, a powerful framework that has been successfully applied for the verification of infinite-state systems, especially parameter…
Monadic Decomposition in Integer Linear Arithmetic (Technical Report)
Matthew Hague, Anthony Widjaja Lin, Philipp Rümmer +1
Monadic decomposability is a notion of variable independence, which asks whether a given formula in a first-order theory is expressible as a Boolean combination of monadic predicat…
Deciding and Interpolating Algebraic Data Types by Reduction (Technical Report)
Hossein Hojjat, Philipp Rümmer
Recursive algebraic data types (term algebras, ADTs) are one of the most well-studied theories in logic, and find application in contexts including functional programming, modellin…
Exploring Approximations for Floating-Point Arithmetic using UppSAT
Aleksandar Zeljic, Peter Backeman, Christoph M. Wintersteiger +1
We consider the problem of solving floating-point constraints obtained from software verification. We present UppSAT --- a new implementation of a systematic approximation refineme…
Fair Termination for Parameterized Probabilistic Concurrent Systems (Technical Report)
Ondrej Lengal, Anthony W. Lin, Rupak Majumdar +1
We consider the problem of automatically verifying that a parameterized family of probabilistic concurrent systems terminates with probability one for all instances against adversa…
Learning to Prove Safety over Parameterised Concurrent Systems (Full Version)
Yu-Fang Chen, Chih-Duo Hong, Anthony W. Lin +1
We revisit the classic problem of proving safety over parameterised concurrent systems, i.e., an infinite family of finite-state concurrent systems that are represented by some fin…
Proceedings 3rd Workshop on Horn Clauses for Verification and Synthesis
John P. Gallagher, Philipp Rümmer
This volume contains the proceedings of HCVS 2016, the Third Workshop on Horn Clauses for Verification and Synthesis which was held on April 3, 2016 in Eindhoven, The Netherlands a…
Liveness of Randomised Parameterised Systems under Arbitrary Schedulers (Technical Report)
Anthony W. Lin, Philipp Ruemmer
We consider the problem of verifying liveness for systems with a finite, but unbounded, number of processes, commonly known as parameterised systems. Typical examples of such syste…
Regular Symmetry Patterns (Technical Report)
Anthony W. Lin, Truong Khanh Nguyen, Philipp Rümmer +1
Symmetry reduction is a well-known approach for alleviating the state explosion problem in model checking. Automatically identifying symmetries in concurrent systems, however, is c…
Horn Clauses for Communicating Timed Systems
Hossein Hojjat, Philipp Rümmer, Pavle Subotic +1
Languages based on the theory of timed automata are a well established approach for modelling and analysing real-time systems, with many applications both in industrial and academi…
The Relationship between Craig Interpolation and Recursion-Free Horn Clauses
Philipp Rümmer, Hossein Hojjat, Viktor Kuncak
Despite decades of research, there are still a number of concepts commonly found in software programs that are considered challenging for verification: among others, such concepts…
Disjunctive Interpolants for Horn-Clause Verification (Extended Technical Report)
Philipp Rümmer, Hossein Hojjat, Viktor Kuncak
One of the main challenges in software verification is efficient and precise compositional analysis of programs with procedures and loops. Interpolation methods remain one of the m…
Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic (Extended Technical Report)
Angelo Brillout, Daniel Kroening, Philipp Ruemmer +1
Craig interpolation has emerged as an effective means of generating candidate program invariants. We present interpolation procedures for the theories of Presburger arithmetic comb…