Dr. Byron Cook is a Principal Researcher at Microsoft's laboratory at Cambridge University where he manages the Programming Principles and Tools (PPT) group together with Luca Cardelli.  Byron is also full professor of computer science at University College London (UCL) . 

Research

Byron's research interests include program analysis/verification, programming languages, theorem proving, logic, hardware design, operating systems, and biological systems.  Byron's recent work has been focused on the development of automatic tools for proving program termination/liveness (see the TERMINATOR project), memory safety (see the SLAyer project), as well as properties about models of biological systems (see the BMA project). 

Students

Former PhD students: Alexey Gotsman and Eric Koskinen. Current PhD student: Kaustubh Nimkar.

Interns

Byron's current and past MSR interns include: Hongyi Chen, Ashutosh Gupta, Mihaela Gheorghiu, Alexey Gotsman, Heidy Khlaaf, Matt Lewis, Shuvendu Lahiri, Stephen Magill, Andrei Popescu, Patrick Rondon, Andrey Rybalchenko, Abigail See, Vlad Shcherbina, Jiri Simsa, Viktor Vafeiadis, Georg Weissenbacher, Thomas Wies, and Greta Yorsh.

Visitors

Byron sometimes hosts visits by professors.  Current and past visiting professors include Koen Claessen, Peter O'Hearn, Andreas Podelski, John Reynolds, Mooly Sagiv, Moshe Vardi, and Helmut Veith.

History

• Byron was one of the developers of the SLAM software model checker. SLAM is now used in a Windows product called Static Driver Verifier, which automatically finds bugs in Windows OS device drivers.
• Byron, together with Shuvendu Lahiri started Microsoft's first SMT decision procedure project, called Zapato. Zapato is the decision procedure currently used within SLAM. Zapato eventually led to Madan Musuvathi's Zap decision procedure, which has since been replaced by Nikolaj Bjorner and Leonardo de Moura's Z3.
• Before joining Microsoft, Byron worked at Prover Technology, where he investigated new algorithms for use in SAT solvers and symbolic model checking tools. These tools (Prover SL, for example) are used in a variety of applications, including the verification of microprocessors, aircraft software, and embedded systems.
• Byron's PhD is from OGI, where he developed a programming language for describing microprocessors and invented a technique based on parametricity to decompose proofs of microprocessor correctness. The theory behind this work was motivated by tricks invented while working both on the Motorola Advanced INFOSEC Machine and prototypes of Intel microprocessors while at Intel's Strategic CAD Research Laboratories.

Still want more information?

You can find out all of the details about Byron in his CV. 

Publications

• BMA: Visual Tool for Modeling and Analysis of Biological Networks (tool paper)
  David Benque, Sam Bourton, Caitlan Cockerton, Byron Cook, Jasmin Fisher, Samin Ishtiaq, Nir Piterman, Alex Taylor, Moshe Vardi 
  CAV 2012
• Proving program termination (Review article)
  Byron Cook, Andreas Podelski, Andrey Rybalchenko 
  Communications of the ACM, Volume 54 Issue 5, May 2011
• Temporal property verification as a program analysis task
  Byron Cook, Eric Koskinen, Moshe Vardi  
  CAV'11 [International Conference on Computer-Aided Verification] (Snowbird)
• SLAyer: Memory safety for systems-level code
  Josh Berdine, Byron Cook, Samin Ishtiaq 
  CAV'11 [International Conference on Computer-Aided Verification] (Snowbird)
• Making prophecies with decision predicates
  Byron Cook and Eric Koskinen
  POPL'11 [Symposium on Principles of Programming Languages] (Austin)
• Tractable reasoning in a fragment of separation logic
  Byron Cook, Christoph Hasse, Joel Ouaknine, Matthew Parkinson, James Worrell
  CONCUR'11 [International conference on concurrency theory] (Aachen)
• Proving stabilization of biological systems
  Byron Cook, Jasmin Fisher, Elzbieta Krepska, Nir Piterman
  VMCAI'11 [Verification, model checking, and abstract interpretation] (Austin)

• Precision and the conjunction rule in concurrent separation logic
  Alexey Gotsman, Josh Berdine, Byron Cook
  MFPS'11 [Conference on the Mathematical Foundations of Programming Semantics] (Pittsburgh)

• Ranking function synthesis for bit-vector relations
  Byron Cook, Daniel Kroening, Philipp Rummer, and Christoph Wintersteiger
  TACAS'10 [Tenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems]

• Finding heap-bounds for hardware synthesis
  Byron Cook, Ashutosh Gupta, Stephen Magill, Andrey Rybalchenko, Jiri Simsa, Satnam Singh, Viktor Vafeiadis
  FMCAD'09 [Formal Methods in Computer Aided Design] (Austin)
• Summarization for termination: No return!
  Byron Cook, Andreas Podelski, Andrey Rybalchenko
  FMSD (2009) 35:369-387
• Proving that non-blocking algorithms don't block
  Alexey Gotsman, Byron Cook, Matthew Parkinson, and Viktor Vafeiadis
  POPL'09 [Symposium on Principles of Programming Languages] (Savannah)
• Principles of program termination (DRAFT)
  Byron Cook
  Notes from the 2008 Marktoberdorf summer school
• Proving conditional termination
  Byron Cook, Sumit Gulwani, Tal Lev-Ami, Andrey Rybalchenko, and Mooly Sagiv
  CAV'08 [International Conference on Computer-Aided Verification] (Princeton)
• Scalable shape analysis for systems code
  Hongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, and Peter O'Hearn
  CAV'08 [International Conference on Computer-Aided Verification] (Princeton)
• Ranking abstractions
  Aziem Chawdhary, Byron Cook, Sumit Gulwani, Mooly Sagiv, and Hongseok Yang
  ESOP'08 [European Symposium on Programming] (Budapest)
• Verification of Boolean programs with unbounded thread creation
  Byron Cook, Daniel Kroening, and Natasha Sharygina
  Journal of Theoretical Computer Science, Vol. 388, 2007, pp. 227-242
• Predicate abstraction via symbolic decision procedures
  Shuvendu Lahiri, Thomas Ball and Byron Cook
  Journal of Logical Methods in Computer Science, Vol. 3, 2007, pp. 1-20
• Proving thread termination 
  Byron Cook, Andreas Podelski, and Andrey Rybalchenko
  PLDI'07 [Conference on Programming Language Design and Implementation] (San Diego)
• Thread-modular shape analysis 
  Alexey Gotsman, Josh Berdine, Byron Cook, and Mooly Sagiv
  PLDI'07 [Conference on Programming Language Design and Implementation] (San Diego)
• Local reasoning for storable locks and threads
  Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky, and Mooly Sagiv
  APLAS'07 [Asian Symposium on Programming Languages and Systems] (Singapore)
• Shape analysis for composite data structures
  Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter O'Hearn, Thomas Wies, and Hongseok Yang
  CAV'07 [International Conference on Computer-Aided Verification] (Berlin)
• Proving termination by divergence
  Domagoj Babic, Byron Cook, Alan Hu, Zvonimir Rakamaric
  SEFM'07 [ International Conference on Software Engineering and Formal Methods] (London)
• Arithmetic strengthening for shape analysis
  Stephen Magill, Josh Berdine, Edmund Clarke, and Byron Cook.
  SAS'07 [International Static Analysis Symposium] (Denmark)
• Proving that programs eventually do something good 
  Byron Cook, Alexey Gotsman, Andreas Podelski, Andrey Rybalchenko, and Moshe Vardi
  POPL'07 [Symposium on Principles of Programming Languages] (Nice)
• Variance analyses from invariance analyses 
  Josh Berdine, Aziem Chawdhary, Byron Cook, Dino Distefano, and Peter O'Hearn
  POPL'07 [Symposium on Principles of Programming Languages] (Nice)
•  Shape analysis by graph decomposition
  Roman Manevich, Josh Berdine, Byron Cook, Ganesan Ramalingam, and Mooly Sagiv
  TACAS'07 [International Conference on Tools and Algorithms for the Construction and Analysis of Systems] (Braga)
• Automatic termination proofs for programs with shape-shifting heaps
  Josh Berdine, Byron Cook, Dino Distefano, and Peter O'Hearn
  CAV'06 [International Conference on Computer-Aided Verification] (Seattle)
• Terminator: Beyond safety(short tool description paper)
  Byron Cook, Andreas Podelski, and Andrey Rybalchenko
  CAV'06 [International Conference on Computer-Aided Verification] (Seattle)
• Repair of Boolean programs with an application to C
  Andreas Griesmayer, Roderick Bloem, and Byron Cook
  CAV'06 [International Conference on Computer-Aided Verification] (Seattle)
• Termination proofs for systems code
  Byron Cook, Andreas Podelski, and Andrey Rybalchenko
  PLDI'06 [Conference on Programming Language Design and Implementation] (Ottawa)
• Thorough static analysis of device drivers
  Thomas Ball, Ella Bounimova, Byron Cook, Vladimir Levin, Jakob Lichtenberg, Con McGarvey, Bohus Ondrusek, Sriram K. Rajamani, Abdullah Ustuner
  EuroSys'06 [European Systems Conference] (Leuven)
• Over-approximating Boolean programs with unbounded thread creation 
  Byron Cook, Daniel Kroening, Natasha Sharygina
  FMCAD'06 [Formal Methods in Computer Aided Design] (San Jose)
• Interprocedural shape analysis with separated heap abstractions 
  Alexey Gotsman, Josh Berdine, and Byron Cook
  SAS'06 [International Static Analysis Symposium] (Seoul)
• Abstraction refinement for termination 
  Byron Cook, Andreas Podelski, Andrey Rybalchenko
  SAS'05 [International Static Analysis Symposium] (London)
• Using Stalmarck's algorithm to prove inequalities 
  Byron Cook, Georges Gonthier
  ICFEM'05 [International Conference on Formal Engineering Methods] (Manchester)
• Symbolic model checking for asynchronous Boolean programs 
  Byron Cook, Daniel Kroening, Natasha Sharygina
  SPIN'05 (San Francisco)
• Predicate abstraction via symbolic decision procedures
  Shuvendu Lahiri, Thomas Ball and Byron Cook
  CAV'05 [International Conference on Computer-Aided Verification] (Edinburgh)
• Cogent: Accurate theorem proving for program verification(short tool description paper)
  Byron Cook, Daniel Kroening, Natasha Sharygina
  CAV'05 [International Conference on Computer-Aided Verification] (Edinburgh)
• Zapato: Automatic theorem proving for predicate abstraction refinement (short tool description paper)
  Thomas Ball, Byron Cook, Shuvendu K. Lahriri, and Lintao Zhang
  CAV'04 [International Conference on Computer-Aided Verification] (Boston)
• Refining approximations in software predicate abstraction 
  Thomas Ball, Byron Cook, Satyaki Das, and Sriram K. Rajamani
  TACAS'04 [Tenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems]
• A symbolic approach to predicate abstraction 
  Shuvendu K. Lahiri, Randal E. Bryant, and Byron Cook
  CAV'03 [International Conference on Computer-Aided Verification] (Boulder)
• Design automation with mixtures of proof strategies for propositional logic
  Gunnar Andersson, Per Bjesse, Byron Cook and Ziyad Hanna
  IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol. 22(8) 2003
• A proof engine approach to solving combinational design automation problems
  Gunnar Andersson, Per Bjesse, Byron Cook, and Ziyad Hanna
  DAC'02 [Design Automation Conference] (Las Vegas)
• A framework for microprocessor correctness statements
  Mark Aagaard, Byron Cook, Nancy Day, and Robert Jones
  International Journal on Software Tools for Technology Transfer, Vol. 4(3), 2003
• A framework for microprocessor correctness statements
  Mark Aagaard, Byron Cook, Nancy Day, and Robert Jones
  CHARME'01 [Correct Hardware Design and Verification Methods] (Edinburgh)
• Combining stream-based and state-based verification techniques for microarchitectures
  Mark Aagaard, Byron Cook, and Nancy Day
  FMCAD'00 [International Conference on Formal Methods in Computer Aided Design] (Austin)
• Formal verification of explicitly parallel microprocessors
  Byron Cook, John Launchbury, John Matthews, and Dick Kieburtz CHARME'99 [Conference on Correct Hardware Design and Verification Methods] (Bad Herrenalb)
• On embedding a microarchitectural design language within Haskell
  John Launchbury, Jeff Lewis and Byron Cook
  ICFP'99 [International Conference on Functional Programming] (Paris)
• Specifying superscalar microprocessors in Hawk
  Byron Cook, John Launchbury, and John Matthews
  1998 Workshop on Formal Techniques for Hardware (Marstrand)
• Microprocessor specification in Hawk
  John Matthews, John Launchbury, and Byron Cook
  ICL'98 [International Conference on Computer Languages] (Chicago)
• Disposable memo functions
  Byron Cook and John Launchbury
  1997 Haskell Workshop Proceedings (Amsterdam)

Projects

• TERMINATOR
• BMA
• SLAyer
• Static Driver Verifier
• SLAM

Upcoming events

• FMCAD'12 (PC)
• HCSS'12 (Invited speaker)
• Formal methods in systems biology (Invited speaker)
• PLDI'12 (PC)

Press

• Geek of the week
  Simple Talk
  By Richard Morris
  September, 2010
• A Sign of the Times
  Wired
  By Cameron Bird
  December, 2009
• A Good Sign
  Science
  By Angela Saini
  July, 2009
• Optic Nerve 
  Vogue
  By Dodie Kazanjain 
  January, 2009
• All Shook Down
  San Francisco Weekly
  By Hiya Swanhuyser
  December 28, 2008
• Inside Terminator
  channel9.msdn.com
  By Charles Torre
  September, 2007
• Using Proofs to Catch System Hangs Before They're Born
  channel9.msdn.com
  By Charles Torre
  July, 2007
• Send in the Terminator
  By Gary Stix
  Scientific American
  December, 2006
• Testers aim to kill off dreaded blue screens
  By Mary Branscombe
  Financial Times
  November, 2006
• Terminator tackles an impossible task
  By Rob Knies
  Microsoft Research News
  September, 2006
• Microsoft bug-checking tools promise fewer crashes
  By Joris Evers
  CNET
  May, 2006
• Microsoft's secret bug squasher
  By Simson Garfinkel
  Wired
  November, 2005
• Building a better bug-trap
  The Economist
  June, 2003
• Researching a path to fewer bugs
  By Patrick Meader
  Visual Studio Magazine
  February, 2003

Recorded presentations

• Proving that programs eventually do something good
  Place: Royal Society, Roger Needham Lecture 
  Date: November 4th, 2009
  Materials: Video
• Automatically Proving Concurrent Programs Correct
  Place: Microsoft TechFest'07
  Date: March 8th 2007
  Materials: Video
• Variance Analyses from Invariance Analyses
  Speaker: Byron Cook
  Place: Microsoft Research, Redmond
  Date: August 8th 2006
  Materials: Video
• Automatically proving the termination of C programs
  Speaker: Byron Cook
  Place: Isaac Newton Institute for Mathematical Sciences
  Date: February 3rd 2006
  Materials: slides and audio 
• Termination and shape-shifting heaps 
  Place: Isaac Newton Institute for Mathematical Sciences Date: May 8th 2006
  Materials: slides and audio

Contact

• Admin: Lynn Hammans
• Email: a-lynnh@microsoft.com 
• Telephone: +44 1223 479 943
• Fax: +44 1223 479 999
• Regular mail:
  Byron Cook
  Roger Needham Building
  J J Thomson Avenue
  Cambridge, CB3 0FB
  United Kingdom