Selected publications at LSV

Abstract:
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.

@inproceedings{M-fsttcs18,
   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 = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9941},
   year = {2018},
}

About LSV

Select by Year