1 citations · 2 across the 7 of their papers we have counts for
7 papers
Deciding Boolean Separation Logic via Small Models (Technical Report)
Tomáš Dacík, Adam Rogalewicz, Tomáš Vojnar +1
We present a novel decision procedure for a fragment of separation logic (SL) with arbitrary nesting of separating conjunctions with boolean conjunctions, disjunctions, and guarded…
Tree-Verifiable Graph Grammars
Mark Chimes, Radu Iosif, Florian Zuleger
Hyperedge-Replacement grammars (HR) have been introduced by Courcelle in order to extend the notion of context-free sets from words and trees to graphs of bounded tree-width. While…
Effective MSO-Definability for Tree-width Bounded Models of an Inductive Separation Logic of Relations
Lucas Bueri, Radu Iosif, Florian Zuleger
A class of graph languages is definable in Monadic Second-Order logic (MSO) if and only if it consists of sets of models of MSO formulæ. If, moreover, there is a computable bound o…
On the Expressiveness of a Logic of Separated Relations
Radu Iosif, Florian Zuleger
We compare the model-theoretic expressiveness of the existential fragment of Separation Logic over unrestricted relational signatures (SLR) -- with only separating conjunction as l…
Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic
Christina Jansen, Jens Katelaan, Christoph Matheja +2
We introduce heap automata, a formalism for automatic reasoning about robustness properties of the symbolic heap fragment of separation logic with user-defined inductive predicates…
On the automated verification of web applications with embedded SQL
Shachar Itzhaky, Tomer Kotek, Noam Rinetzky +4
A large number of web applications is based on a relational database together with a program, typically a script, that enables the user to interact with the database through embedd…