LFCS
2007
Springer
14 years 5 months ago
2007
Springer
Abstract. In order to verify programs with pointer variables, we introduce a temporal logic LTLmem whose underlying assertion language is the quantifier-free fragment of separatio...