Sciweavers

POPL
2007
ACM
14 years 4 months ago
First-class nonstandard interpretations by opening closures
Jeffrey Mark Siskind, Barak A. Pearlmutter
POPL
2007
ACM
14 years 4 months ago
A semantics-based approach to malware detection
Mila Dalla Preda, Mihai Christodorescu, Somesh Jha...
POPL
2007
ACM
14 years 4 months ago
Dynamic heap type inference for program understanding and debugging
C programs can be difficult to debug due to lax type enforcement and low-level access to memory. We present a dynamic analysis for C that checks heap snapshots for consistency wit...
Ben Liblit, Chloë W. Schulze, Marina Polishch...
POPL
2007
ACM
14 years 4 months ago
Generative unbinding of names
This paper is concerned with a programming language construct for typed name binding that enforces -equivalence. It proves a new result about what operations on names can co-exist...
Andrew M. Pitts, Mark R. Shinwell
POPL
2007
ACM
14 years 4 months ago
Lazy multivariate higher-order forward-mode AD
A method is presented for computing all higher-order partial derivatives of a multivariate function Rn R. This method works by evaluating the function under a nonstandard interpre...
Barak A. Pearlmutter, Jeffrey Mark Siskind
POPL
2007
ACM
14 years 4 months ago
Modular verification of a non-blocking stack
This paper contributes to the development of techniques for the modular proof of programs that include concurrent algorithms. We present a proof of a non-blocking concurrent algor...
Matthew J. Parkinson, Richard Bornat, Peter W. O'H...
POPL
2007
ACM
14 years 4 months ago
Lightweight fusion by fixed point promotion
This paper proposes a lightweight fusion method for general recursive function definitions. Compared with existing proposals, our method has several significant practical features...
Atsushi Ohori, Isao Sasano
POPL
2007
ACM
14 years 4 months ago
Conditional must not aliasing for static race detection
Race detection algorithms for multi-threaded programs using the common lock-based synchronization idiom must correlate locks with the memory locations they guard. The heart of a p...
Mayur Naik, Alex Aiken
POPL
2007
ACM
14 years 4 months ago
Logic-flow analysis of higher-order programs
This work presents a framework for fusing flow analysis and theorem proving called logic-flow analysis (LFA). The framework itthe reduced product of two abstract interpretations: ...
Matthew Might