TPHOL
2009
IEEE
14 years 9 months ago
2009
IEEE
Abstract. We present a comprehensive set of tactics that make it practical to use separation logic in a proof assistant. These tactics enable the verification of partial correctne...
TPHOL
2009
IEEE
14 years 9 months ago
2009
IEEE
Abstract. This paper presents a separation-logic framework for reasoning about low-level C code in the presence of virtual memory. We describe ract, generic Isabelle/HOL framework ...
TASE
2009
IEEE
14 years 9 months ago
2009
IEEE
—Formal verification of low-level programs often requires explicit reasoning and specification of runtime stacks. Treating stacks naively as parts of ordinary heaps can lead to...
FOSSACS
2009
Springer
14 years 9 months ago
2009
Springer
Standard analysis on recursive data structures restrict their attention to shape properties (for instance, a program that manipulates a list returns a list), excluding properties t...
ESOP
2009
Springer
14 years 9 months ago
2009
Springer
Abstract. Rely-guarantee is a well-established approach to reasoning about concurrent programs that use parallel composition. However, parallel composition is not how concurrency i...
FASE
2010
Springer
14 years 9 months ago
2010
Springer
This paper describes a compositional analysis algorithm for statically detecting leaks in Java programs. The algorithm is based on separation logic and exploits the concept of bi-a...
POPL
2010
ACM
14 years 11 months ago
2010
ACM
Most systems based on separation logic consider only restricted forms of implication or non-separating conjunction, as full support for these connectives requires a non-trivial no...
ICFP
2006
ACM
15 years 2 months ago
2006
ACM
In previous work, we proposed a Hoare Type Theory (HTT) which combines effectful higher-order functions, dependent types and Hoare Logic specifications into a unified framework. H...
POPL
2005
ACM
15 years 2 months ago
2005
ACM
105
click to vote
POPL
2007
ACM
15 years 2 months ago
2007
ACM
We present a formal model of memory that both captures the lowlevel features of C's pointers and memory, and that forms the basis for an expressive implementation of separati...