
Dr. Byron Cook is a senior researcher at Microsoft's laboratory at Cambridge University and full professor of computer science at Queen Mary, University of London.
Byron has recently been named the winner of the 2009 Roger Needham Award, which is made annually by the British Computer Society for a distinguished research contribution in computer science by a UK based researcher within ten years of their PhD.
Research
Byron's research interests include program analysis/verification, programming languages, theorem proving, logic, hardware design, and operating systems. Byron's recent work has been focused on the development of automatic tools for
- C-to-gates hardware synthesis (See a recent paper)
- Termination and liveness proving (See TERMINATOR and a recent Scientfic American article),
- Discovering invariants regarding mutable data structures (See the SLAyer project).
Teaching
Byron has recently taught graduate-level courses on methods of proving program termination at Cambridge University, Carnegie Mellon, Imperial College, the Marktoberdorf summer school, and the Trends in Concurrency summer school. Annotated copies of the slides from the Marktoberdorf lectures will be made available soon. The lecture notes from these courses will form the basis of Byron's forthcoming book, entitled Proving Program Termination (Cambridge University Press). Byron will be teaching 4 graduate-level lectures at Berkeley University in April 2009
Students
Byron supervises several PhD students at Cambridge University, including Alexey Gotsman and Eric Koskinen. Byron sometimes also supervises Cambridge undergraduate final-year projects.
Interns
Byron's current and past research interns include: Ashutosh Gupta, Mihaela Gheorghiu, Alexey Gotsman, Shuvendu Lahiri, Jacopo Mantovani, Stephen Magill, Andrei Popescu, Patrick Rondon, Andrey Rybalchenko, Jiri Simsa, Viktor Vafeiadis, Georg Weissenbacher, Thomas Wies, and Greta Yorsh.
Visitors
Byron sometimes hosts visits by professors. Current and past visiting professors include 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.
You can find out more information about Byron on his blog or in his CV.
- Finding heap-bounds for hardware synthesis (DRAFT)
Byron Cook, Ashutosh Gupta, Stephen Magill, Andrey Rybalchenko, Jiri Simsa, Satnam Singh, Viktor Vafeiadis
Submitted for review - Summarization for termination
Byron Cook, Andreas Podelski, Andrey Rybalchenko
To appear: Journal of Formal Methods in System Design - Proving that non-blocking algorithms don't block
Alexey Gotsman, Byron Cook, Matthew Parkinson, and Viktor Vafeiadis
To appear: 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
Upcoming events
- WST'09 (PC)
- Infinity'09 (Invited speaker)
- CAV'09 (PC)
- FMICS'09 (Co-chair)
- Needham lecture
- CAV'10 (Co-chair)
Press
- 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
- 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 information
- Email: bycook at microsoft.com
- Telephone: +44(0)1223479795
- Fax: +44 (0)1223 479 999 (Put "Attn: Byron Cook" on the cover sheet)
- Regular mail:
Byron Cook
Roger Needham Building
J J Thomson Avenue
Cambridge, CB3 0FB
United Kingdom



