1 citations · 1 across the 5 of their papers we have counts for
7 papers
Encapsulation for Practical Simplification Procedures
Olga Shumsky Matlin, William McCune
ACL2 was used to prove properties of two simplification procedures. The procedures differ in complexity but solve the same programming problem that arises in the context of a resol…
Methods to Model-Check Parallel Systems Software
Olga Shumsky Matlin, William McCune, Ewing Lusk
We report on an effort to develop methodologies for formal verification of parts of the Multi-Purpose Daemon (MPD) parallel process management system. MPD is a distributed collecti…
OTTER 3.3 Reference Manual
William McCune
OTTER is a resolution-style theorem-proving program for first-order logic with equality. OTTER includes the inference rules binary resolution, hyperresolution, UR-resolution, and b…
Mace4 Reference Manual and Guide
William McCune
Mace4 is a program that searches for finite models of first-order formulas. For a given domain size, all instances of the formulas over the domain are constructed. The result is a…
Yet Another Single Law for Lattices
William McCune, Ranganathan Padmanabhan, Robert Veroff
In this note we show that the equational theory of all lattices is defined by a single absorption law. The identity of length 29 with 8 variables is shorter than previously known s…
SPINning Parallel Systems Software
O. S. Matlin, E. Lusk, W. McCune
We describe our experiences in using SPIN to verify parts of the Multi Purpose Daemon (MPD) parallel process management system. MPD is a distributed collection of processes connect…