ICTAC
2010
Springer
13 years 9 months ago
2010
Springer
We consider software verification of imperative programs by theorem proving in higher-order separation logic. Of particular interest are the difficulties of encoding and reasoning ...
JSC
2010
13 years 10 months ago
2010
We study the automated verification of pointer safety for heap-manipulating imperative programs with unknown procedure calls. Given a Hoare-style partial correctness specificati...
ENTCS
2006
13 years 11 months ago
2006
Parkinson, Bornat, and Calcagno recently introduced a logic for partial correctness in which program variables are treated as resource, generalizing earlier work based on separati...
ENTCS
2006
13 years 11 months ago
2006
Separation logic [20,21,14] began life as an extended formalisation of Burstall's treatment of list-mutating programs [8]. It rapidly became clear that there was more that it...
ENTCS
2008
13 years 11 months ago
2008
We show how to reason, in the proof assistant Coq, about realistic programming languages using a combination of separation logic and heterogeneous multimodal logic. A heterogeneou...
ENTCS
2008
13 years 11 months ago
2008
We formalize higher-order separation logic for a first-order imperative language with procedures and local variables in Isabelle/HOLCF. The assertion language is modeled in such a...
ENTCS
2008
13 years 11 months ago
2008
As an extension to Floyd-Hoare logic, separation logic has been used to facilitate reasoning about imperative programs manipulating shared mutable data structures. Recently, it ha...
ENTCS
2008
13 years 11 months ago
2008
This paper explores a unification of the ideas of Concurrent Separation Logic with those of Communicating Sequential Processes. It extends separation logic by an operator for sepa...
ENTCS
2008
13 years 11 months ago
2008
The B+ tree is an ordered tree structure with a fringe list. It is the most widely used data structure for data organisation and searching in database systems specifically, and, p...
FORTE
2010
14 years 27 days ago
2010
Abstract. Separation logic is a popular specification language for imperative programs where the heap can only be mentioned through pointsto assertions. However, separation logic&#...