Colloquium: Verification of Programs with Weakest Precondition

Mr. W. Mark Vanfleet, US National Security Agency

Host: Professor V.W. Marek

Venue: 453f FPAT (Engineering Tower)

(Refreshments at 3.30 p.m., 773 FPAT) 

Abstract:

Everyone has learned about Floyd-Hoare Program verification when they took basic computer science courses even as long ago as 30 years ago. Now, how to integrate Floyd-Hoare state processing, state verification, jump across loops, integrate with a theorem prover, generate test vectors, connect weakest pre-condition to strongest post-condition to various cut point verification conditions in the program thus verifying intermediate results will be presented. Instead of cutting a loop and creating a loop invariant, we will show how to jump across a loop, create a single verification condition that allows the entire loop state transform to be stepped across in one virtual clock cycle will be shown. The presentation will show some worked examples and demonstrate the technology and will refer the reader to technical papers. The presentation will show the technology in play. The presentation will reduce Floyd-Hoare and Weakest Precondition Analysis to simple LISP programs. The attendee may be tempted to jump out of his seat and say what about Haskell? The answer is we are generating Primitive Recursive Function Theory relationships with a touch of Lambda Calculus that just flows naturally as LISP. Thus, providing a natural extension to the University of Texas Theorem prover, ACL2.

Speaker's short bio:

Mr. W. Mark Vanfleet has worked for the National Security Agency (NSA) Information Assurance Directorate for over 23 years as an Information Systems Security Analyst, Crypto Mathematician, and Global network Analyst. He holds NSA certifications in crypto-mathematics, communication and information systems security, and software engineering process and practice. Mr. Vanfleet has been involved in high-assurance software architecture, design, and evaluation for 32 years. He has bachelor's degrees in mathematics and computer science, and a master's degree in mathematics and statistics from the University of Utah. Mr. Vanfleet leads Formal Methods evaluations for infrastructures requiring high robustness in the US Department of Defense.