SPIN 2017 will feature the following invited speakers.
Google Inc., Mountain View, California, USAhttp://www.domagoj-babic.com
Title and abstract TBA
Domagoj Babic is a computer scientist at Google, Inc. His work focuses on research and development of automated software analysis systems for various security-related applications. Primarily, he wants his work to have a positive impact on people's lives. He enjoys building strong teams and working with them on solving large-scale real-world important problems, while learning and having fun on the way. He's particularly excited about big technical challenges and enjoy creating the vision, strategy, and technology for taming those challenges. Over his career, Domagoj has published in the areas of verification, testing, security of complex software systems, automated reasoning, grammar inference, and applied formal methods. Before joining Google, Domagoj was a research scientist at UC Berkeley and elsewhere in industry. He received his Dipl.Ing. in Electrical Engineering and M.Sc. in Computer Science from the Zagreb University (Faculty of Electrical Engineering and Computing) in 2001 and 2003. He received his Ph.D. in Computer Science in 2008 from the University of British Columbia. He was a recipient of the NSERC PDF Research Fellowship (2010-2012), Microsoft Graduate Research Fellowship (2005-2007), and several awards at international programming competitions (1st place at the 2007 Satisfiability Modulo Theories competition in the bit-vector arithmetic category and 3rd place at the 2005 Satisfiability Testing competition in the satisfiable-crafted instances category).
Amazon Web Services, New York, USA and University College London, UKhttp://www0.cs.ucl.ac.uk/staff/b.cook
Title: Automated Reasoning about Amazon Web Services
Byron Cook leads AWS Security’s Automated Reasoning Group which develops and applies constraint/logic based automated tools for proving the correctness of software, network configurations, and policies. Previous to joining AWS, Byron was for 10 years a researcher at Microsoft Research, where he investigated new approaches worked actively in the areas of functional programming, hardware modeling and design, SAT-solving, symbolic model checking for finite-state systems, decision procedures, automatic program verification and analysis, and the analysis of biological systems. Byron’s research in automatic program verification has gained significant attention (e.g. a substantial publication record, numerous keynote speaker invitations, and press hits in Scientific American, Science, Vogue, Financial Times, Economist, and Wired). Byron is particularly well known for his work on automatic methods for proving program termination and the Terminator termination prover. This work represents a breakthrough, challenging the prevailing opinion in computer science that automatic termination proving is impossible. Byron is also well known for his contributions to SLAM, which is often credited for the recent revival of automatic program verification research.
Nimble Research, Arcadia, California, USAhttp://spinroot.com/gerard
Title: Fast Structural Software Analysis
Gerard Holzmann got his PhD from Delft University of Technology in The Netherlands in the deep dark days before there were PCs, iphones, or even an internet. He joined Bell Labs in Murray Hill,New Jersey, to help fix some of these things, but others beat him to it. At Bell Labs he did develop one of the first digital darkroom programs, and early versions of software analysis tools like Spin. After twenty-some years at Bell Labs he moved to the sunnier side of the US and joined NASA/JPL to start a lab for reliable software (LaRS). For unclear reasons he was later made a JPL fellow, an ACM fellow, and a member of the auspicious National Academy of Engineering. He retired from JPL in January 2017 to start a new company called Nimble Research, where he is currently employed as prime nimbler.