Mechanical proofs about computer programs
D.I. Good, 2100 Main Building, Institute for Computing Science, The University of Texas at Austin, Austin, Texas 78712, U.S.A.
Publisher Summary
This chapter provides an overview of the mechanical proofs about computer programs. One of the major problems with the current practice of software engineering is an absence of predictability. Within current software engineering practice, the only sound way to make a precise, accurate prediction about how a software system will behave is to build it and run it. In contrast to software engineering, mathematical logic provides a sound, objective way to make accurate, precise predictions about the behaviour of mathematical operations. The Gypsy verification ...
Get Readings in Artificial Intelligence and Software Engineering now with the O’Reilly learning platform.
O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.
