3 papers
cs.LO2017
Complete Cyclic Proof Systems for Inductive Entailments
Radu Iosif, Cristina Serban
In this paper we develop cyclic proof systems for the problem of inclusion between the least sets of models of mutually recursive predicates, when the ground constraints in the ind…
cs.LO2016
Reasoning in the Bernays-Schoenfinkel-Ramsey Fragment of Separation Logic
Andrew Reynolds, Radu Iosif, Cristina Serban
Separation Logic (SL) is a well-known assertion language used in Hoare-style modular proof systems for programs with dynamically allocated data structures. In this paper we investi…
cs.LO2016
A Decision Procedure for Separation Logic in SMT
Andrew Reynolds, Radu Iosif, Tim King
This paper presents a complete decision procedure for the entire quantifier-free fragment of Separation Logic ($\seplog$) interpreted over heaplets with data elements ranging over…