Sciweavers

ESOP
2010
Springer
13 years 7 months ago
A Semantic Framework for Declassification and Endorsement
Language-based information flow methods offer a principled way to enforce strong security properties, but enforcing noninterference is too inflexible for realistic applications. Se...
Aslan Askarov, Andrew Myers
ESOP
2010
Springer
13 years 7 months ago
TRX: A Formally Verified Parser Interpreter
Parsing is an important problem in computer science and yet surprisingly little attention has been devoted to its formal verification. In this paper, we present TRX: a parser inter...
Adam Koprowski, Henri Binsztok
ESOP
2010
Springer
13 years 7 months ago
CFA2: A Context-Free Approach to Control-Flow Analysis
Abstract. In a functional language, the dominant control-flow mechanism is function call and return. Most higher-order flow analyses, including k-CFA, do not handle call and retu...
Dimitrios Vardoulakis, Olin Shivers
ESOP
2010
Springer
13 years 8 months ago
Dynamic Boundaries: Information Hiding by Second Order Framing with First Order Assertions
Abstract. The hiding of internal invariants creates a mismatch between procedure specifications in an interface and proof obligations on the implementations of those procedures. T...
David A. Naumann, Anindya Banerjee
ESOP
2010
Springer
13 years 8 months ago
On the Expressive Power of Primitives for Compensation Handling
Modern software systems have frequently to face unexpected events, reacting so to reach a consistent state. In the field of concurrent and mobile systems (e.g., for web services) ...
Ivan Lanese, Cátia Vaz, Carla Ferreira
ESOP
2010
Springer
13 years 10 months ago
Amortized Resource Analysis with Polynomial Potential
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 0002, Martin Hofmann
ESOP
2010
Springer
13 years 10 months ago
A Universal Calculus for Stream Processing Languages
Stream processing applications such as algorithmic trading, MPEG processing, and web content analysis are ubiquitous and essential to business and entertainment. Language designers...
Robert Soulé, Martin Hirzel, Robert Grimm, ...
ESOP
2010
Springer
14 years 29 days ago
Precise and Automated Contract-based Reasoning for Verification and Certification of Information Flow Properties of Programs wit
Abstract. Embedded information assurance applications that are critical to national and international infrastructures, must often adhere to certification regimes that require infor...
Torben Amtoft, John Hatcliff and Edwin Rodríguez
ESOP
2010
Springer
14 years 29 days ago
Deadlock-free Channels and Locks
The combination of message passing and locking to protect shared state is a useful concurrency pattern. However, programs that employ this pattern are susceptible to deadlock. That...
Jan Smans, K. Rustan M. Leino, Peter Müller