Sciweavers

APLAS
2007
ACM
13 years 7 months ago
The Nuggetizer: Abstracting Away Higher-Orderness for Program Verification
Paritosh Shroff, Christian Skalka, Scott F. Smith
APLAS
2007
ACM
13 years 7 months ago
Complete Lattices and Up-To Techniques
Abstract. We propose a theory of up-to techniques for proofs by coinduction, in the setting of complete lattices. This theory improves over existing results by providing a way to c...
Damien Pous
APLAS
2007
ACM
13 years 7 months ago
A Systematic Approach to Probabilistic Pointer Analysis
Abstract. We present a formal framework for syntax directed probabilistic program analysis. Our focus is on probabilistic pointer analysis. We show how to obtain probabilistic poin...
Alessandra Di Pierro, Chris Hankin, Herbert Wiklic...
APLAS
2007
ACM
13 years 7 months ago
Type-Based Verification of Correspondence Assertions for Communication Protocols
Gordon and Jeffrey developed a type system for checking correspondence assertions. The correspondence assertions, proposed by Woo and Lam, state that when a certain event (called a...
Daisuke Kikuchi, Naoki Kobayashi
APLAS
2007
ACM
13 years 7 months ago
Call-by-Name and Call-by-Value in Normal Modal Logic
Abstract. This paper provides a call-by-name and a call-by-value calculus, both of which have a Curry-Howard correspondence to the minimal normal logic K. The calculi are extension...
Yoshihiko Kakutani
APLAS
2007
ACM
13 years 7 months ago
The Semantics of "Semantic Patches" in Coccinelle: Program Transformation for the Working Programmer
We rationally reconstruct the core of the Coccinelle system, used for automating and documenting collateral evolutions in Linux device drivers. A denotational semantics of the syst...
Neil D. Jones, René Rydhof Hansen
APLAS
2007
ACM
13 years 7 months ago
Deriving Compilers and Virtual Machines for a Multi-level Language
We develop virtual machines and compilers for a multi-level language, which supports multi-stage specialization by composing program fragments with quotation mechanisms. We conside...
Atsushi Igarashi, Masashi Iwaki
APLAS
2007
ACM
13 years 7 months ago
A Probabilistic Applied Pi-Calculus
Abstract. We propose an extension of the Applied Pi
Jean Goubault-Larrecq, Catuscia Palamidessi, Angel...
APLAS
2007
ACM
13 years 7 months ago
Local Reasoning for Storable Locks and Threads
We present a resource oriented program logic that is able to reason about concurrent heap-manipulating programs with unbounded numbers of dynamically-allocated locks and threads. T...
Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rin...
APLAS
2007
ACM
13 years 7 months ago
Scalable Simulation of Cellular Signaling Networks
Abstract. Given the combinatorial nature of cellular signalling pathways, where biological agents can bind and modify each other in a large number of ways, concurrent or agent-base...
Vincent Danos, Jérôme Feret, Walter F...