activity
20132021
most citedCompetition Report: CHC-COMP-21

15 citations · 31 across the 11 of their papers we have counts for

collaborators

14 papers

cs.LO202115 cited

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…

cs.LO2021

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…

cs.LO2020

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)…

cs.LO202012 cited

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…

cs.LO2020

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…

cs.LO2020

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…