9 citations · 36 across the 34 of their papers we have counts for
Showing 2016Show all
3 papers · 1 filter
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.CC2016
How hard is it to verify flat affine counter systems with the finite monoid property ?
Radu Iosif, Arnaud Sangnier
We study several decision problems for counter systems with guards defined by convex polyhedra and updates defined by affine transformations. In general, the reachability problem i…
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…