APLAS
2009
ACM
14 years 6 months ago
2009
ACM
We define a higher-order process calculus with algebraic operations such as encryption and decryption, and develop a bisimulation proof method for behavioral equivalence in this c...
APLAS
2009
ACM
14 years 6 months ago
2009
ACM
We describe an algorithm for synthesizing resource invariants that are used in the verification of concurrent programs. This synthesis employs bi-abductive inference to identify t...
APLAS
2009
ACM
14 years 6 months ago
2009
ACM
Separation Algebras serve as models of Separation Logics; Share Accounting allows reasoning about concurrent-read/exclusive-write resources in Separation Logic. In designing a Conc...
APLAS
2009
ACM
14 years 6 months ago
2009
ACM
Abstract. Context-sensitive points-to analysis is critical for several program optimizations. However, as the number of contexts grows exponentially, storage requirements for the a...
APLAS
2009
ACM
14 years 6 months ago
2009
ACM
APLAS
2009
ACM
14 years 6 months ago
2009
ACM
We propose a type system for a programming language with memory allocation/deallocation primitives, which prevents memory-related errors such as double-frees and memory leaks. The ...
APLAS
2009
ACM
14 years 6 months ago
2009
ACM
We present a simple algorithmic extension of the classical call-strings approach to mitigate substantial performance degradation caused by spurious interprocedural cycles. Spuriou...