Sciweavers

ESOP
2010
Springer
14 years 8 months ago
Verifying a Compiler for Java Threads
Abstract. A verified compiler is an integral part of every security infrastructure. Previous work has come up with formal semantics for sequential and concurrent variants of Java a...
Andreas Lochbihler
ESOP
2010
Springer
14 years 8 months ago
Faulty Logic: Reasoning about Fault Tolerant Programs
Transient faults are single-shot hardware errors caused by high energy particles from space, manufacturing defects, overheating, and other sources. Such faults can be devastating f...
Matthew L. Meola and David Walker
ESOP
2010
Springer
14 years 8 months ago
Formal Verification of Coalescing Graph-Coloring Register Allocation
Iterated Register Coalescing (IRC) is a widely used heuristic for performing register allocation via graph coloring. Many implementations in existing compilers follow (more or less...
Andrew W. Appel, Benoît Robillard, Sandrine ...
ESOP
2010
Springer
14 years 8 months ago
A Grammar-based Approach to Invertible Programs
Abstract. Program inversion has many applications such as in the implementation of serialization/deserialization and in providing support for redo/undo, and has been studied by man...
Kazutaka Matsuda, Shin-Cheng Mu, Zhenjiang Hu and ...
ESOP
2010
Springer
14 years 8 months ago
A theory of speculative computation
Gérard Boudol, Gustavo Petri
ESOP
2010
Springer
14 years 8 months ago
Logical Concurrency Control From Sequential Proofs
G. Ramalingam, Jyotirmoy V. Deshmukh, Kapil Vaswan...
ESOP
2010
Springer
14 years 8 months ago
Explicit Stabilisation for Modular Rely-Guarantee Reasoning
Abstract. We propose a new formalisation of stability for Rely-Guarantee, in which an assertion's stability is encoded into its syntactic form. This allows two advances in mod...
John Wickerson, Matthew J. Parkinson, Mike Dodds
ESOP
2010
Springer
14 years 8 months ago
Fluid Updates: Beyond Strong vs. Weak Updates
Abstract. We describe a symbolic heap abstraction that unifies reasoning about arrays, pointers, and scalars, and we define a fluid update operation on this symbolic heap that rela...
Isil Dillig, Thomas Dillig and Alex Aiken
ESOP
2010
Springer
14 years 8 months ago
Weighted Dynamic Pushdown Networks
We develop a generic framework for the analysis of programs with recursive procedures and dynamic process creation. To this end we combine the approach of weighted pushdown systems...
Alexander Wenner
ESOP
2010
Springer
14 years 8 months ago
Amortized Resource Analysis with Polynomial Potential - A Static Inference of Polynomial Bounds for Functional Programs
In 2003, Hofmann and Jost introduced a type system that uses a potential-based amortized analysis to infer bounds on the resource consumption of (first-order) functional programs. ...
Jan Hoffmann and Martin Hofmann