This site uses cookies to deliver our services and to ensure you get the best experience. By continuing to use this site, you consent to our use of cookies and acknowledge that you have read and understand our Privacy Policy, Cookie Policy, and Terms
We present a framework for defining abstract interpreters for liveness properties, in particular program termination. The framework makes use of the theory of metric spaces to defi...
Live heap space analyses have so far been concerned with the standard sequential programming model. However, that model is not very well suited for embedded real-time systems, wher...
We consider programming language aspects of algorithms that operate on data too large to fit into memory. In previous work we have introduced IntML, a functional programming langu...
Abstract. We propose a flexible method for verifying the security of ML programs that use cryptography and recursive data structures. Our main applications are X.509 certificate ch...
We extract techniques developed in the Concurrent C minor project to build a framework for constructing logics that contain approximation and/or separation. Approximation occurs wh...
We consider the problem of specifying data structures with complex sharing in a manner that is both declarative and results in provably correct code. In our approach, abstract data...
Peter Hawkins, Alex Aiken, Kathleen Fisher, Martin...