Sciweavers

ICTAC
2010
Springer
13 years 1 months ago
Mechanized Verification with Sharing
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 ...
J. Gregory Malecha, Greg Morrisett
JSC
2010
106views more  JSC 2010»
13 years 2 months ago
Verifying pointer safety for programs with unknown calls
We study the automated verification of pointer safety for heap-manipulating imperative programs with unknown procedure calls. Given a Hoare-style partial correctness specificati...
Chenguang Luo, Florin Craciun, Shengchao Qin, Guan...
ENTCS
2006
189views more  ENTCS 2006»
13 years 3 months ago
Variables as Resource for Shared-Memory Programs: Semantics and Soundness
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...
Stephen D. Brookes
ENTCS
2006
138views more  ENTCS 2006»
13 years 3 months ago
Variables as Resource in Separation Logic
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...
Richard Bornat, Cristiano Calcagno, Hongseok Yang
ENTCS
2008
136views more  ENTCS 2008»
13 years 3 months ago
Multimodal Separation Logic for Reasoning About Operational Semantics
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...
Robert Dockins, Andrew W. Appel, Aquinas Hobor
ENTCS
2008
140views more  ENTCS 2008»
13 years 3 months ago
Higher-Order Separation Logic in Isabelle/HOLCF
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...
Carsten Varming, Lars Birkedal
ENTCS
2008
109views more  ENTCS 2008»
13 years 3 months ago
Separation Logic for Multiple Inheritance
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...
Chenguang Luo, Shengchao Qin
ENTCS
2008
120views more  ENTCS 2008»
13 years 3 months ago
Separation Logic Semantics for Communicating Processes
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...
Tony Hoare, Peter W. O'Hearn
ENTCS
2008
120views more  ENTCS 2008»
13 years 3 months ago
Reasoning about B+ Trees with Operational Semantics and Separation Logic
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...
Alan P. Sexton, Hayo Thielecke
FORTE
2010
13 years 5 months ago
Heap-Dependent Expressions in Separation Logic
Abstract. Separation logic is a popular specification language for imperative programs where the heap can only be mentioned through pointsto assertions. However, separation logic&#...
Jan Smans, Bart Jacobs, Frank Piessens