Sciweavers

Share
POPL
2007
ACM
10 years 12 months ago
Assessing security threats of looping constructs
There is a clear intuitive connection between the notion of leakage of information in a program and concepts from information theory. This intuition has not been satisfactorily pi...
Pasquale Malacaria
POPL
2007
ACM
10 years 12 months ago
Towards a mechanized metatheory of standard ML
We present an internal language with equivalent expressive power to Standard ML, and discuss its formalization in LF and the machine-checked verification of its type safety in Twe...
Daniel K. Lee, Karl Crary, Robert Harper
POPL
2007
ACM
10 years 12 months ago
Scrap your boilerplate with XPath-like combinators
XML programming involves idioms for expressing `structure shyness' such as the descendant axis of XPath or the default templates of XSLT. We initiate a discussion of the rela...
Ralf Lämmel
POPL
2007
ACM
10 years 12 months ago
On the analysis of interacting pushdown systems
Pushdown Systems (PDSs) has become an important paradigm for program analysis. Indeed, recent work has shown a deep connection between inter-procedural dataflow analysis for seque...
Vineet Kahlon, Aarti Gupta
POPL
2007
ACM
10 years 12 months ago
Cork: dynamic memory leak detection for garbage-collected languages
A memory leak in a garbage-collected program occurs when the program inadvertently maintains references to objects that it no longer needs. Memory leaks cause systematic heap grow...
Maria Jump, Kathryn S. McKinley
POPL
2007
ACM
10 years 12 months ago
Interprocedural analysis of asynchronous programs
An asynchronous program is one that contains procedure calls which are not immediately executed from the callsite, but stored and "dispatched" in a non-deterministic ord...
Ranjit Jhala, Rupak Majumdar
POPL
2007
ACM
10 years 12 months ago
Program verification as probabilistic inference
In this paper, we propose a new algorithm for proving the validity or invalidity of a pre/postcondition pair for a program. The algorithm is motivated by the success of the algori...
Sumit Gulwani, Nebojsa Jojic
POPL
2007
ACM
10 years 12 months ago
Geometry of synthesis: a structured approach to VLSI design
We propose a new technique for hardware synthesis from higherorder functional languages with imperative features based on Reynolds's Syntactic Control of Interference. The re...
Dan R. Ghica
POPL
2007
ACM
10 years 12 months ago
Lock allocation
We introduce lock allocation, an automatic technique that takes a multi-threaded program annotated with atomic sections (that must be executed atomically), and infers a lock assig...
Michael Emmi, Jeffrey S. Fischer, Ranjit Jhala, Ru...
books