Formal Verification of LabVIEW/G

This project centered around constructing a formal verification system for LabVIEW/G diagrams using the ACL2 theorem prover.  Funded by National Instruments, it was a collaboration with the Dept. of Computer Sciences at UT Austin.

Participants: Jacob Kornerup (NI), Grant Passmore (Texas & NI), Matt Kaufmann (Texas)

Papers

Formal Verification of LabVIEW Programs Using the ACL2 Theorem Prover (ACL2 2009)

Undergraduate Thesis

Presentations

Oh Yeah? Then Prove It! (Turing Scholars Undergraduate Research Symposium, Summer 2008)

ACL2 Seminar (22 April 2009)

Thesis Presentation (27 April 2009)

Past

Distributed Murϕ Model Checking with PReach

When I joined Intel, one of my first projects was working on a distributed model checker being developed in collaboration with researchers at the University of British Columbia. Intel had very large models of various HW protocols written in Murϕ, but were unable to verify them due to their size. PReach is a fully distributed implementation of the Murϕ system written in Erlang. This project was a lot of fun, and really helped cement my belief that using the right tool (Erlang) for the job (distributed computation) makes all the difference in the world.

Participants: Flavio M. de Paula (UBC), Brad Bingham (UBC), Jesse Bingham (Intel), John Erickson (Intel), Gaurav Singh (Intel)

Papers

PReach: A Distributed Explicit State Model Checker (UBC TR-2010-05)

Future

My brain is open!