SPIN 2017 will feature the following invited speakers.
Google Inc., Mountain View, California, USAhttp://www.domagoj-babic.com
Title and abstract TBA
BioDomagoj 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 Formal Reasoning About Amazon Web Services
Automatic and semiautomatic formal verification and model checking tools are now being used within AWS to find proofs that prove or disprove desired properties of key AWS components. In this session, we outline these efforts and discuss how tools are used to play and then replay found proofs of desired properties when software artifacts or networks are modified, thus helping provide security throughout the lifetime of the AWS system.
Byron’s interests include program analysis/verification, security, programming languages, theorem proving, logic, hardware design, operating systems, and biological systems. At Amazon Byron leads a research group focused on formal/constraint-based tools for reasoning about cloud-computing security. Byron is previously known for his work on the termination prover Terminator/T2, and the SLAM model checker.
Nimble Research, Arcadia, California, USAhttp://spinroot.com/gerard
Title: Cobra: Fast Structural Code Checking
In software analysis we are usually interested in formally proving some key correctness properties of a software design. Design errors can be hard to catch without the right tools. Actually, even with the right tools they can be hard to catch, because now developers do not only have to understand their own design but also the details of the tools that they are trying to use to analyze it.
There’s another thing that most software developers know well: the number of coding errors is typically far larger than the number of design errors. If something is wrong, the problem can almost always be traced back to a coding mistake, and less often to an algorithmic error. Tools for chasing down bugs are popular because they are usually simple to use. Yet, they rarely rise beyond the level of sophisticated forms of trial and error. That is: they are not very effective.
The first commercial static source code analyzers hit the market a little over a decade ago to fill this gap. Today these tools are mature, and their use is rightly widespread in commercial software development. The currently available analyzers share some undesirable features though. They tend to be big, slow, and hard to customize even for fairly basic types of checks. In this talk I’ll describe a different type of multi-core static analysis tool, Cobra, that is designed to be small, simple to customize, and fast enough that it can be used interactively. The tool does this by targeting a more limited, but interesting, set of properties.