Journal of the ACM (JACM)


Search Issue
enter search term and/or author name


Journal of the ACM (JACM), Volume 52 Issue 3, May 2005

An improved exponential-time algorithm for k-SAT
Ramamohan Paturi, Pavel Pudlák, Michael E. Saks, Francis Zane
Pages: 337-364
DOI: 10.1145/1066100.1066101
We propose and analyze a simple new randomized algorithm, called ResolveSat, for finding satisfying assignments of Boolean formulas in conjunctive normal form. The algorithm consists of two stages: a preprocessing stage in which resolution is applied...

Simplify: a theorem prover for program checking
David Detlefs, Greg Nelson, James B. Saxe
Pages: 365-473
DOI: 10.1145/1066100.1066102
This article provides a detailed description of the automatic theorem prover Simplify, which is the proof engine of the Extended Static Checkers ESC/Java and ESC/Modula-3. Simplify uses the Nelson--Oppen method to combine decision procedures for...

Beyond proof-of-compliance: security analysis in trust management
Ninghui Li, John C. Mitchell, William H. Winsborough
Pages: 474-514
DOI: 10.1145/1066100.1066103
Trust management is a form of distributed access control that allows one principal to delegate some access decisions to other principals. While the use of delegation greatly enhances flexibility and scalability, it may also reduce the control that a...