Three conferences and a workshop, all in the field of formal verification and system design, were held from the end of September through the beginning of October.
The first, MEMOCODE ‘15, in its thirteenth year, is dedicated to bringing principles of formal methods to hardware development, which enables hardware designers to prove rigorously that their chips will function as intended. Indeed, as hardware has grown exponentially more complex, traditional methods of testing have become unreliable, and instead formal proofs of correctness are preferred.
The second, SAT ‘15, is focused on the propositional satisfiability problem, which asks if a given logical statement, which is a mix of Boolean operators and variables, admits a set of assignments to those variables which make the logical statement true. SAT ‘15 also focuses on finding new applications of solutions to this problem.
The third, FMCAD ‘15 (Formal Methods in Computer-Aided Design), is dedicated to presenting novel approaches in the theory of formal methods in hardware and system verification. FMCAD focuses heavily on using formal methods to automate system design.
In addition, the 13th annual workshop on the ACL2 theorem prover, a Lisp-based computer modeling software package, was held immediately after FMCAD ‘15. The ACL2 theorem prover was heavily developed by Dr. J Strother Moore, Professor Emeritus at UT Austin, and his work on the class of theorem provers of which ACL2 is a member (known as Boyer-Moore theorem provers), won him the prestigious ACM Software System Award in 2005.
Dr. Warren Hunt, Jr., a professor of computer science at UT whose research focus includes writing formal specifications for computer hardware and proving their correctness, served on the steering committee of FMCAD and the program committee for the ACL2 workshop, and helped organize MEMOCODE and SAT as well. According to Dr. Hunt, the results presented at these conferences, which represent the cutting edge of research in their respective areas, are significant, but their utility may not be immediately apparent.
Said Dr. Hunt, “It's often hard to say what is significant when it first appears. Why? Well, it's not yet [known] how much of an effect some newly-reported result will have until some time has passed.” As is often the case with theoretical results, like the ones presented at these conferences, while their utility is not immediately known, they end up having a tremendous impact after further research. One famous example is PageRank, an algorithm that ranks results of a web search; this algorithm, created by Sergey Brin and Larry Page at Stanford, now powers Google’s ranking engine.
All three conferences will be held again in one year and the ACL2 workshop will be held again in 18 months.