Introduction to the Special Section.

This article provides information about extended versions of four of the best papers presented at the Eleventh Annual Conference on Computer Assurance, with the theme of "Industrial Strength Research," held at the National Institute of Standards and Technology in Gaithersburg, Maryland, in June 1996. These papers address the issue of how to apply the theory of high assurance computing to system and software development. The first paper, "An Industrial-Strength Theorem Prover for a Logic Based on Common Lisp" describes a computational logic for Applicative Common Lisp (ACL2), a reimplemented, extended version of the Boyer-Moore theorem prover. In the second paper, titled, "Comparing Verification Systems: Interactive Consistency in ACL2," researchers have developed a multitude of formal techniques for specifying and verifying computer systems. The benchmark problem exists in this type of specification is the Oral Messages algorithm, a generalization of the Byzantine Generals problem. The third paper, "Using a Protean Language to Enhance Expressiveness in Specification," introduces a Protean specification language, a generalization of process algebras that allows the user to invent his own domain-specific operators to improve abstraction and readability.