Name: Carl Seger
Title: Formal Verification of Complex Data-Paths: An Industrial Perspective
Abstract: After caches, most transistors in a modern chip are devoted to wide data-paths. Due to performance and power requirements, these data-paths are often implementing sophisticated algorithms and use complex implementations. As Intel experienced in 1994, a bug in a data-path can be extremely expensive and thus needs to be avoided at almost any cost. At the same time, simulation based verification is extremely poor at verifying data-paths due to the vast data space and thus formal verification is appealing. In this talk we will give a retrospective on the formal verification of complex data-paths that took place at Intel from the mid-1990s until recently. We will discuss the technology that made the effort possible, the tools developed that made it feasible, and the methodology created that made it practical.
Bio: Dr. Carl-Johan (Carl) Seger received his M.Sc. in Engineering Physics from Chalmers University of Technology, Sweden in 1985 and his M. Math and Ph.D. degrees in Computer Science from University of Waterloo, Canada, in 1986 and 1988 respectively.  After seven years in academia, ending as associate professor at the University of British Columbia, Canada, he joined Intel Corporation's Strategic CAD Labs in 1995 where he stayed for more than 21 years.  At Intel, Dr. Seger drove the development and successful wide deployment of formal verification of Intel's microprocessors.  In 2006-2007 has was granted a full year sabbatical from Intel and became an Oliver Smithies lecturer and visiting fellow at Balliol College, Oxford.  In 2016, he took early retirement from Intel and joined the Computer Science and Engineering department at Chalmers University of Technology as a WASP Professor. In addition to formal verification of hardware, Dr. Seger's research interests focuses on how to design and verify correct, robust, and secure software/hardware systems for autonomous vehicles and other Internet-of-Things.
Name: Grant Passmore
Title: Some Lessons Learned in the Industrialization of Formal Methods for Financial Algorithms
Abstract: At Imandra Inc. we have pioneered the application of formal methods to financial algorithms. After nearly a decade of R&D and business development, our Imandra automated reasoning system is now in mainstream use at major financial firms such as Goldman Sachs, Itiviti and OneChronos. In these settings, Imandra is relied upon for the design, verification, ongoing auditing and calibration of global financial infrastructure such as trading venues (exchanges and dark pools), smart order routers and FIX connectivity between trading systems. Getting to this point, however, was not an easy road. When we began, we faced a collection of simultaneous challenges. In this talk, we shall discuss these challenges and our solutions, with an eye towards open problems and the future.
Bio: Grant Passmore is co-founder and co-CEO of Imandra. Grant is a widely published researcher in formal verification and symbolic AI, and has more than fifteen years’ industrial formal verification experience. He has been a key contributor to safety verification of algorithms at Cambridge, Carnegie Mellon, Edinburgh, Microsoft Research and SRI. He earned his PhD from the University of Edinburgh, is a graduate of UT Austin (BA in Mathematics) and the Mathematical Research Institute in the Netherlands (Master Class in Mathematical Logic), and is a Life Member of Clare Hall, University of Cambridge.