Share this page
Share this page E-mail this page Print this page RSS feeds
Home > People > Byron Cook
Byron Cook

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

 

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

Press

Recorded presentations

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