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 30 Issue 5, August 2008

A semantics-based approach to malware detection
Mila Dalla Preda, Mihai Christodorescu, Somesh Jha, Saumya Debray
Article No.: 25
DOI: 10.1145/1387673.1387674

Malware detection is a crucial aspect of software security. Current malware detectors work by checking for signatures, which attempt to capture the syntactic characteristics of the machine-level byte sequence of the malware. This reliance...

Nominal logic programming
James Cheney, Christian Urban
Article No.: 26
DOI: 10.1145/1387673.1387675

Nominal logic is an extension of first-order logic which provides a simple foundation for formalizing and reasoning about abstract syntax modulo consistent renaming of bound names (that is, α-equivalence). This article investigates logic...

A capability calculus for concurrency and determinism
Tachio Terauchi, Alex Aiken
Article No.: 27
DOI: 10.1145/1387673.1387676

This article presents a static system for checking determinism (technically, partial confluence) of communicating concurrent processes. Our approach automatically detects partial confluence in programs communicating via a mix of different kinds of...

Two-dimensional bidirectional object layout
Joseph (Yossi) Gil, William Pugh, Grant E. Weddell, Yoav Zibin
Article No.: 28
DOI: 10.1145/1387673.1387677

Object layout schemes used in C++ and other languages rely on (sometimes numerous) compiler generated fields. We describe a language-independent object layout scheme, which is space optimal, that is, objects are contiguous, and contain no...

A type system equivalent to a model checker
Mayur Naik, Jens Palsberg
Article No.: 29
DOI: 10.1145/1387673.1387678

Type systems and model checking are two prevalent approaches to program verification. A prominent difference between them is that type systems are typically defined in a syntactic and modular style whereas model checking is usually performed in a...