Sciweavers

Share
warning: Creating default object from empty value in /var/www/modules/taxonomy/taxonomy.module on line 1416.
ESOP
2007
Springer
11 years 5 months ago
Type Reconstruction for General Refinement Types
Abstract. General refinement types allow types to be refined by predicates written in a general-purpose programming language, and can express function pre- and postconditions and d...
Kenneth W. Knowles, Cormac Flanagan
ESOP
2007
Springer
11 years 5 months ago
Controlling the What and Where of Declassification in Language-Based Security
Abstract. While a rigorous information flow analysis is a key step in obtaining meaningful end-to-end confidentiality guarantees, one must also permit possibilities for declassific...
Heiko Mantel, Alexander Reinhard
ESOP
2007
Springer
11 years 5 months ago
Scalar Outcomes Suffice for Finitary Probabilistic Testing
Abstract. The question of equivalence has long vexed research in concurrency, leading to many different denotational- and bisimulation-based approaches; a breakthrough occurred wit...
Yuxin Deng, Rob J. van Glabbeek, Carroll Morgan, C...
ESOP
2007
Springer
11 years 5 months ago
A Certified Lightweight Non-interference Java Bytecode Verifier
Non-interference is a semantical condition on programs that guarantees the absence of illicit information flow throughout their execution, and that can be enforced by appropriate i...
Gilles Barthe, David Pichardie, Tamara Rezk
ESOP
2007
Springer
11 years 7 months ago
On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning
We study the relationship between Concurrent Separation Logic (CSL) and the assume-guarantee (A-G) method (a.k.a. rely-guarantee method). We show in three steps that CSL can be tre...
Xinyu Feng, Rodrigo Ferreira, Zhong Shao
ESOP
2007
Springer
11 years 7 months ago
Using History Invariants to Verify Observers
Abstract. This paper contributes a technique that expands the set of object invariants that one can reason about in modular verification. The technique uses history invariants, tw...
K. Rustan M. Leino, Wolfram Schulte
ESOP
2007
Springer
11 years 7 months ago
Type-Based Analysis of Deadlock for a Concurrent Calculus with Interrupts
The goal of our research project is to establish a type-based method for verification of certain critical properties (such as deadlockand race-freedom) of operating system kernels...
Kohei Suenaga, Naoki Kobayashi
ESOP
2007
Springer
11 years 7 months ago
Interprocedurally Analysing Linear Inequality Relations
In this paper we present an alternative approach to interprocedurally g linear inequality relations. We propose an abstraction of the effects of procedures through convex sets of t...
Helmut Seidl, Andrea Flexeder, Michael Petter
books