Paper Info
Title
Program Verification with Separation Logic.
Abstract
Separation Logic is a framework for the development of modular program analyses for sequential, inter-procedural and concurrent programs. The first part of the paper introduces Separation Logic first from a historical, then from a program verification perspective. Because program verification eventually boils down to deciding logical queries such as the validity of verification conditions, the second part is dedicated to a survey of decision procedures for Separation Logic, that stem from either SMT, proof theory or automata theory. Incidentally we address issues related to decidability and computational complexity of such problems, in order to expose certain sources of intractability.
Year
DOI
Venue
2018
10.1007/978-3-319-94111-0_3
Lecture Notes in Computer Science
DocType
Volume
ISSN
Conference
10869
0302-9743
Citations 
PageRank 
References 
0
0.34
0
Authors
1
Name
Order
Citations
PageRank
Radu Iosif148342.44