25 Dec 2015
Our task is to define formal systems that describe systems and reason about those systems to determine correctness. One application of this is verifying language properties, but that represents a tiny fraction of the kinds of verification we can do. In fact, we do this all the time: (i) circuits example of a parity checker; (ii) examples from physics.
24 Dec 2015
About 7 months ago I started exploring new theorem provers for use in my lab and teaching. I am a diehard PVS fan and that really hasn’t changed. The folks at SRI produced a tool that shaped my teaching and research for years. I just got a bit stir crazy and wanted to check out something completely different.