BZPEERPapers, people, evidence and research paths
Menu

Discover

SearchFind papers, people, topics, institutions and opportunities from one place.GraphSee how papers, authors, topics and evidence connect.

Research tools

HomeContinue from the papers, people and topics that matter now.CollectionsTurn saved papers into reading lists, evidence maps and shareable context.ResearchReconstruct the path that led you from search to paper to question.CollaborationMove from a paper, topic or expert request into a focused thread.PublishCreate full-text research articles with metadata, formulas and versions.

Network

ExpertsFind specialists whose work and reviews explain why they can help.CommunitiesJoin research groups organized around papers, topics and shared evidence.

Opportunities

ListingsBrowse roles, calls and collaborations connected to real research context.

Account

Log inReturn to your saved papers, graph views and active threads.Create accountStart saving papers, building a research trail and joining teams.
Log inCreate account

Source author record

Philipp Rümmer

Philipp Rümmer appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record
Logic in Computer ScienceArtificial IntelligenceMachine LearningProgramming LanguagesSoftware EngineeringSymbolic ComputationSystems and Control

Catalog footprint

What is connected

8works
7topics
4close collaborators

Actions

Connect this record

Log in to claim
Open graphBrowse works

Research graph

See the researcher in context

Open full explorer

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

8 published item(s)

preprint2022arXiv

Exploring Representation of Horn Clauses using GNNs (Extended Technical Report)

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-distance relational information implicitly represented in programs using identifiers. Addressing the first point, we consider Constrained Horn Clauses (CHCs) as a standard representation of program verification problems, providing a simple and programming language-independent syntax. For the second challenge, we explore graph representations of CHCs, and propose a new Relational Hypergraph Neural Network (R-HyGNN) architecture to learn program features. We introduce two different graph representations of CHCs. One is called constraint graph (CG), and emphasizes syntactic information of CHCs by translating the symbols and their relations in CHCs as typed nodes and binary edges, respectively, and constructing the constraints as abstract syntax trees. The second one is called control- and data-flow hypergraph (CDHG), and emphasizes semantic information of CHCs by representing the control and data flow through ternary hyperedges. We then propose a new GNN architecture, R-HyGNN, extending Relational Graph Convolutional Networks, to handle hypergraphs. To evaluate the ability of R-HyGNN to extract semantic information from programs, we use R-HyGNNs to train models on the two graph representations, and on five proxy tasks with increasing difficulty, using benchmarks from CHC-COMP 2021 as training data. The most difficult proxy task requires the model to predict the occurrence of clauses in counter-examples, which subsumes satisfiability of CHCs. CDHG achieves 90.59% accuracy in this task. Furthermore, R-HyGNN has perfect predictions on one of the graphs consisting of more than 290 clauses. Overall, our experiments indicate that R-HyGNN can capture intricate program features for guiding verification problems.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Competition Report: CHC-COMP-20

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 problems in linear integer arithmetic, linear real arithmetic, and arrays. The competition was run in the first week of May 2020 using the StarExec computing cluster. This report gives an overview of the competition design, explains the organisation of the competition, and presents the competition results.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Monadic Decomposition in Integer Linear Arithmetic (Technical Report)

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 predicates in the theory. Recently, Veanes et al. showed the usefulness of monadic decomposability in the context of SMT (i.e. the input formula is quantifier-free), and found various interesting applications including string analysis. However, checking monadic decomposability is undecidable in general. Decidability for certain theories is known (e.g. Presburger Arithmetic, Tarski's Real-Closed Field), but there are very few results regarding their computational complexity. In this paper, we study monadic decomposability of integer linear arithmetic in the setting of SMT. We show that this decision problem is coNP-complete and, when monadically decomposable, a formula admits a decomposition of exponential size in the worst case. We provide a new application of our results to string constraint solving with length constraints. We then extend our results to variadic decomposability, where predicates could admit multiple free variables (in contrast to monadic decomposability). Finally, we give an application to quantifier elimination in integer linear arithmetic where the variables in a block of quantifiers, if independent, could be eliminated with an exponential (instead of the standard doubly exponential) blow-up.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

Proceedings 3rd Workshop on Horn Clauses for Verification and Synthesis

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 as a satellite event of the European Joint Conferences on Theory and Practice of Software (ETAPS 2016). Many program verification and synthesis problems of interest can be modeled directly using Horn clauses and many recent advances in the CLP and CAV communities have centered around efficiently solving problems presented as Horn clauses. The Third Workshop on Horn Clauses for Verification and Synthesis was organised with the aim to bring together researchers working in the two communities of Constraint/Logic Programming and Program Verification on the topic of Horn clause based analysis, verification and synthesis. Horn clauses for verification and synthesis have been advocated by these two communities in different times and from different perspectives, and this workshop is organized to stimulate interaction and a fruitful exchange and integration of experiences.

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

Regular Symmetry Patterns (Technical Report)

Symmetry reduction is a well-known approach for alleviating the state explosion problem in model checking. Automatically identifying symmetries in concurrent systems, however, is computationally expensive. We propose a symbolic framework for capturing symmetry patterns in parameterised systems (i.e. an infinite family of finite-state systems): two regular word transducers to represent, respectively, parameterised systems and symmetry patterns. The framework subsumes various types of symmetry relations ranging from weaker notions (e.g. simulation preorders) to the strongest notion (i.e. isomorphisms). Our framework enjoys two algorithmic properties: (1) symmetry verification: given a transducer, we can automatically check whether it is a symmetry pattern of a given system, and (2) symmetry synthesis: we can automatically generate a symmetry pattern for a given system in the form of a transducer. Furthermore, our symbolic language allows additional constraints that the symmetry patterns need to satisfy to be easily incorporated in the verification/synthesis. We show how these properties can help identify symmetry patterns in examples like dining philosopher protocols, self-stabilising protocols, and prioritised resource-allocator protocol. In some cases (e.g. Gries's coffee can problem), our technique automatically synthesises a safety-preserving finite approximant, which can then be verified for safety solely using a finite-state model checker.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

Horn Clauses for Communicating Timed Systems

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 academic context. Model checking for timed automata has been studied extensively during the last two decades; however, even now industrial-grade model checkers are available only for few timed automata dialects (in particular Uppaal timed automata), exhibit limited scalability for systems with large discrete state space, or cannot handle parametrised systems. We explore the use of Horn constraints and off-the-shelf model checkers for analysis of networks of timed automata. The resulting analysis method is fully symbolic and applicable to systems with large or infinite discrete state space, and can be extended to include various language features, for instance Uppaal-style communication/broadcast channels and BIP-style interactions, and systems with infinite parallelism. Experiments demonstrate the feasibility of the method.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

Disjunctive Interpolants for Horn-Clause Verification (Extended Technical Report)

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 most promising techniques for such verification, and are closely related to solving Horn clause constraints. We introduce a new notion of interpolation, disjunctive interpolation, which solve a more general class of problems in one step compared to previous notions of interpolants, such as tree interpolants or inductive sequences of interpolants. We present algorithms and complexity for construction of disjunctive interpolants, as well as their use within an abstraction-refinement loop. We have implemented Horn clause verification algorithms that use disjunctive interpolants and evaluate them on benchmarks expressed as Horn clauses over the theory of integer linear arithmetic.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

The Relationship between Craig Interpolation and Recursion-Free Horn Clauses

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 include concurrency, and the compositional analysis of programs with procedures. As a promising direction to overcome such difficulties, recently the use of Horn constraints as intermediate representation of software programs has been proposed. Horn constraints are related to Craig interpolation, which is one of the main techniques used to construct and refine abstractions in verification, and to synthesise inductive loop invariants. We give a survey of the different forms of Craig interpolation found in literature, and show that all of them correspond to natural fragments of (recursion-free) Horn constraints. We also discuss techniques for solving systems of recursion-free Horn constraints.

0 citations0 reviewsNo code linkedOpen access