CVC3 and Applications

The first part of this talk covers the history and progression of SMT solvers I have worked on, starting with SVC, and then continuing with CVC, CVC Lite, CVC3, and finally CVC4, describing innovations, applications, limitations, and lessons learned along the way. The second part of the talk describes a specific application of CVC3 to verify low-level packet processing code in C. This application makes use of a large number of features including uninterpreted functions, data types, bit-vectors, arrays, and quantifiers.

Clark Barrett, New York University, New York, USA

Clark Barrett received his bachelor's degree in Mathematics, Computer Science, and Electrical Engineering from Brigham Young University in 1995. He received his PhD from Stanford University and joined the faculty of New York University in the Fall of 2002.

His industry experience includes work on formal hardware verification at Intel's Strategic CAD Labs, as well as work on formal and semi-formal hardware verification tools at 0-in Design Automation (now part of Mentor Graphics).

Professor Barrett's research agenda includes the theory, implementation, and application of advanced automated deduction and theorem proving. His SMT tools have been widely used. He received an IBM Software Quality Innovation Award for CVC3 in November 2008 and the 2010 HVC award (with Leonardo de Moura, Silvio Ranise, Aaron Stump, and Cesare Tinelli) for his work helping to establish and support the SMT community.