a summary of progress toward proving program correctness
Interest in proving the correctness of programs has grown explosively within the last two or three years. There are now over a hundred people pursuing research on this general topic; most of them are relative newcomers to the field. At least three reasons can be cited for this rapid growth: (1) The inability to design and implement software systems which can be guaranteed correct is severely restricting computer applications in many important areas. (2) Debugging and maintaining large computer programs is now well recognized as one of the most serious and costly problems facing the computer industry. (3) A large number of mathematicians, especially logicians, are interested in applications where their talents can be used.
program correctness research general reasoning design software systems computation applications debugging industrial relation