Sciweavers

POPL
2007
ACM
14 years 11 months ago
First-class nonstandard interpretations by opening closures
Jeffrey Mark Siskind, Barak A. Pearlmutter
POPL
2007
ACM
14 years 11 months ago
A semantics-based approach to malware detection
Mila Dalla Preda, Mihai Christodorescu, Somesh Jha...
POPL
2007
ACM
14 years 11 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 11 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 11 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 11 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 11 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 11 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 11 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
POPL
2007
ACM
14 years 11 months ago
Operational semantics for multi-language programs
Jacob Matthews, Robert Bruce Findler