VMCAI
2009
Springer
14 years 9 months ago
2009
Springer
We present a lightweight type-and-effect system for Java programs that features two major innovations over extant object-oriented effects systems: initialization effects, which ...
VMCAI
2009
Springer
14 years 9 months ago
2009
Springer
We present the first shape analysis for multithreaded programs that avoids the explicit enumeration of execution-interleavings. Our approach is to automatically infer a resource ...
VMCAI
2009
Springer
14 years 9 months ago
2009
Springer
There has been a lot of recent research on transaction-based concurrent programming, aimed at offering an easier concurrent programming paradigm that enables programmers to better...
VMCAI
2009
Springer
14 years 9 months ago
2009
Springer
We study price-per-reward games on hybrid automata with strong resets. They generalise priced games previously studied and have applications in scheduling. We obtain decidability r...
VMCAI
2009
Springer
14 years 9 months ago
2009
Springer
This paper presents a case study in modelling and verifying the Linux Virtual File System (VFS). Our work is set in the context of Hoare’s verification grand challenge and, in p...
VMCAI
2009
Springer
14 years 9 months ago
2009
Springer
Abstract. Because of its critical importance underlying all other software, lowlevel system software is among the most important targets for formal verification. Low-level systems...
VMCAI
2009
Springer
14 years 9 months ago
2009
Springer
Abstract There is an intimate link between program structure and behaviour. Exploiting this link to phrase program correctness problems in terms of the structural properties of a p...
VMCAI
2009
Springer
14 years 9 months ago
2009
Springer
—A variety of partial modeling formalisms, aimed re and reason about abstractions, have been proposed. Some, e.g., Kripke Modal Transition Systems (KMTSs) put strong restrictions...
VMCAI
2009
Springer
14 years 9 months ago
2009
Springer
This paper describes the methods used in Empire, a tool to detect concurrency-related bugs, namely atomic-set serializability violations in Java programs. The correctness criterion...