POPL
2012
ACM
11 years 12 months ago
2012
ACM
We present an analysis which takes as its input a sequential program, augmented with annotations indicating potential parallelization opportunities, and a sequential proof, writte...
AOSD
2012
ACM
12 years 22 hour ago
2012
ACM
In this work we consider specification and compositional verification for interference detection when several aspects are woven together under joint-weaving semantics without re...
POPL
2011
ACM
12 years 7 months ago
2011
ACM
The technique of trace-based just-in-time compilation was introduced by Bala et al. and was further developed by Gal et al. It currently enjoys success in Mozilla Firefox’s Java...
PLDI
2010
ACM
13 years 8 months ago
2010
ACM
Verified compilers, such as Leroy's CompCert, are accompanied by a fully checked correctness proof. Both the compiler and proof are often constructed with an interactive proo...
ASM
1998
ASM
13 years 8 months ago
1998
ASM
This paper is devoted to the speci cation of the Stanford FLASHcache coherence protocol within the ASM formalism. Correctness proofs related to data consistency are presented. Corn...
FM
2003
Springer
13 years 9 months ago
2003
Springer
We present the formal framework for a novel approach for specifying and automatically implementing systems such as digital circuits and network protocols. The goal is to reduce the...
POPL
2010
ACM
14 years 1 months ago
2010
ACM
We present a verified compiler to an idealized assembly language from a small, untyped functional language with mutable references and exceptions. The compiler is programmed in th...