[CSUSB]>> [CNS]>> [CSE]>> [R J Botting]>> biba.php
The author used simple reasoning about weakest preconditions, postconditions, invariants and logic to find and fix errors in real C code for TCP/IP and other communications software. A nice example of a pragmatic use of formal methods for program derivation and verification.
Search for a specific bibliographic item by name.
To see the complete bibliography (1Mb+) select:[Bibliography]