Title: Automated Reasoning in LabVIEW with the Method/ACL2 System

Speaker: Grant Passmore

Short Abstract:

Since June, I've been working at National Instruments with Jacob Kornerup
and Jeff Kodosky on the goal of extending their programming language,
LabVIEW/G, with meta-linguistic constructs and tools for proving theorems
about LabVIEW/G code.  The product thus far is what I call the Method/ACL2
System, and is comprised of methods for adding assertions to LabVIEW
diagrams (Theorem Blocks), tools for translating both the object-level
LabVIEW code and meta-level assertions into reasonably viable ACL2
counterparts, and new induction heuristics for generating inductive proof
obligations based upon LabVIEW's singular inductive structure (the Shift
Register).   

Working towards this goal has been a wonderful, fascinating journey.   
The purpose of this talk is to show some examples of my approaches and
little milestones thus far, gain insight from all of you, and hopefully
share some of the excitement and joy that I have gained (and continue to
gain) from this project.