29 citations · 102 across the 28 of their papers we have counts for
30 papers
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…
Synthesis and Verification of Transformer Programs (Technical Report)
Hongjian Jiang, Matthew Hague, Philipp Rümmer +1
C-RASP is a simple programming language that was recently shown to capture concepts expressible by transformers. In this paper, we develop new algorithmic techniques for automatica…
Arithmetizing Shape Analysis
Sebastian Wolff, Ekanshdeep Gupta, Zafer Esen +3
Memory safety is an essential correctness property of software systems. For programs operating on linked heap-allocated data structures, the problem of proving memory safety boils…
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…
Automatic Program Instrumentation for Automatic Verification (Extended Technical Report)
Jesper Amilon, Zafer Esen, Dilian Gurov +2
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…
Timing Analysis of Embedded Software Updates
Ahmed El Yaacoub, Luca Mottola, Thiemo Voigt +1
We present RETA (Relative Timing Analysis), a differential timing analysis technique to verify the impact of an update on the execution time of embedded software. Timing analysis i…
Exploring Representation of Horn Clauses using GNNs (Extended Technical Report)
Chencheng Liang, Philipp Rümmer, Marc Brockschmidt
Learning program semantics from raw source code is challenging due to the complexity of real-world programming language syntax and due to the difficulty of reconstructing long-dist…
CertiStr: A Certified String Solver (technical report)
Shuanglong Kan, Anthony W. Lin, Philipp Rümmer +1
Theories over strings are among the most heavily researched logical theories in the SMT community in the past decade, owing to the error-prone nature of string manipulations, which…
Solving String Constraints With Regex-Dependent Functions Through Transducers With Priorities And Variables
Taolue Chen, Alejandro Flores Lamas, Matthew Hague +6
Regular expressions are a classical concept in formal language theory. Regular expressions in programming languages (RegEx) such as JavaScript, feature non-standard semantics of op…
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…
Decision Procedures for Path Feasibility of String-Manipulating Programs with Complex Operations
Taolue Chen, Matthew Hague, Anthony W. Lin +2
The design and implementation of decision procedures for checking path feasibility in string-manipulating programs is an important problem, whose applications include symbolic exec…
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…