enter search term and/or author name
An improved exponential-time algorithm for k-SAT
Ramamohan Paturi, Pavel Pudlák, Michael E. Saks, Francis Zane
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
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
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...