Paper Info
Title
Comparing Verification Systems: Interactive Consistency in ACL2
Abstract
Achieving interactive consistency among processors in the presence of faults is an important problem in fault tolerant computing, first cleanly formulated by Lamport, Pease, and Shostak and solved in selected cases with their Oral Messages (OM) algorithm. Several machine-supported verifications of this algorithm have been presented, including a particularly elegant formulation and proof by John Rushby using EHDM and PVS. Rushby proposes interactive consistency as a benchmark problem for specification and verification systems. We present a formalization of the OM algorithm in the ACL2 logic and compare our formalization and proof to his. We draw some conclusions concerning the range of desirable features for verification systems. In particular, while higher-order functions, strong typing, lambda abstraction, and full quantification have some value they come with a cost; moreover, many uses of such features can be easily translated into simpler logical constructs, which facilitate more automated proof discovery. We offer a cautionary note about comparing systems with respect to a small set of problems in a limited domain.
Year
DOI
Venue
1997
10.1109/32.588536
IEEE Trans. Software Eng.
Keywords
Field
DocType
lambda abstraction,algorithm design and analysis,formal specification,cost function,software fault tolerance,formal verification,computational logic,higher order functions,fault tolerance,fault tolerant,theorem proving,strong typing,formal logic
Algorithm design,Programming language,Computer science,Lisp,Formal specification,Theoretical computer science,Fault tolerance,ACL2,Formal verification
Journal
Volume
Issue
ISSN
23
4
0098-5589
Citations 
PageRank 
References 
5
1.21
9
Authors
1
Name
Order
Citations
PageRank
William D. Young133166.64