This talk is based on the paper "Formal Verification of LabVIEW
Programs Using the ACL2 Theorem Prover" by Matt Kaufmann, Jacob
Kornerup, and Mark Reitblatt (speaker), to be presented at the 2009
ACL2 Workshop.

Abstract (quoting from that paper):

The LabVIEW* system is based on a graphical dataflow language, and is widely
used for data acquisition, instrument control and industrial automation.  This
paper presents a methodology for annotating LabVIEW programs with their
specifications, translating those annotated programs into ACL2, and proving
the translated specifications with ACL2.  Our system supports verification of
inductive invariants of bounded loops as well as assertions about
straight-line code.  Our verification methodology supports the user by
generating a highly structured set of proof obligations, many or all of which
are discharged automatically.  This methodology makes extensive use of hints
to support scalability, including careful theory control as well as functional
instantiation that avoids explicit use of induction.  We describe the design,
applicability and limitations of the framework. We also present several
examples demonstrating our approach.

* LabVIEW is a trademark of National Instruments, Inc.