ACM DL

Programming Languages and Systems (TOPLAS)

Menu

Search Issue
enter search term and/or author name

Archive


ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 33 Issue 5, November 2011

Software model checking using languages of nested trees
Rajeev Alur, Swarat Chaudhuri, P. Madhusudan
Article No.: 15
DOI: 10.1145/2039346.2039347

While model checking of pushdown systems is by now an established technique in software verification, temporal logics and automata traditionally used in this area are unattractive on two counts. First, logics and automata traditionally used in...

On contract satisfaction in a higher-order world
Christos Dimoulas, Matthias Felleisen
Article No.: 16
DOI: 10.1145/2039346.2039348

Behavioral software contracts have become a popular mechanism for specifying and ensuring logical claims about a program's flow of values. While contracts for first-order functions come with a natural interpretation and are well understood, the...

Bottom-up shape analysis using LISF
Bhargav S. Gulavani, Supratik Chakraborty, G. Ramalingam, Aditya V. Nori
Article No.: 17
DOI: 10.1145/2039346.2039349

In this article, we present a new shape analysis algorithm. The key distinguishing aspect of our algorithm is that it is completely compositional, bottom-up and noniterative. We present our algorithm as an inference system for computing Hoare...