Selected publications at LSV

We study an extension of propositional separation logic that can specify robustness properties, such as acyclicity and garbage freedom, for automatic verification of stateful programs with singly-linked lists. We show that its satisfiability problem is PSpace-complete, whereas modest extensions of the logic are shown to be Tower-hard. As separating implication, reachability predicates (under some syntactical restrictions) and a unique quantified variable are allowed, this logic subsumes several PSpace-complete separation logics considered in previous works.

   address = {Ahmedabad, India},
   author = {Alessio Mansutti},
   booktitle = {{P}roceedings of the 38th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'18)},
   DOI = {10.4230/LIPIcs.FSTTCS.2018.42},
   editor = {Sumit Ganguly and Paritosh Pandya},
   month = dec,
   pages = {42:1-42:23},
   publisher = {Leibniz-Zentrum f{\"u}r Informatik},
   series = {Leibniz International Proceedings in Informatics},
   title = {Extending propositional separation logic for robustness properties},
   url = {},
   year = {2018},

About LSV

Select by Year