\documentclass[a4]{report} %%%% SETTINGS \oddsidemargin 0pt \evensidemargin 0pt \marginparwidth 0pt \marginparsep 0pt \textwidth 6.2in \topmargin 0pt \textheight 9in \headsep 0in %%%% END SETTINGS \begin{document} %\noindent {\bf\Large Dr. J. Byron Cook} \\ \begin{center} {\bf\Huge Curriculum Vitae} \end{center} \ \\ \ \\ %\noindent {\bf\Large Prof. Dr. Byron Cook, Ph.D., B.Sci.} \\ \noindent {\bf\Large Byron Cook} \\ \noindent{\bf Affiliations}: University College London, and Amazon Web Services\\ %\noindent{\bf Address}: Microsoft Research, 21 Station Road, Cambridge CB1 2FB, United Kingdom \\ \noindent{\bf Email}: {\tt byroncook@gmail.com} \\ %\noindent{\bf Email}: {\tt bycook@microsoft.com} \\ %\noindent{\bf Telephone}: +44 (0)1223 479795 \\ \noindent{\bf URL}: {\tt http://www0.cs.ucl.ac.uk/staff/b.cook/} \\ %\noindent{\bf Date of birth}: March 15, 1971 \\ \noindent{\bf Citizenship}: US and UK (EU) dual national\\ \hrule \ \\ \ \\ %\section*{Research interests} %\begin{itemize} %\item Methods and algorithms for proving program correctness (termination proving, rely/guarantee, resource invariants, shape analysis, symbolic model checking, abstraction refinement, %abstract interpretation, etc.) %\item Theorem provers and decision procedures (interpolation, %decision procedure combinations, fast predicate abstraction, etc.) %\item SAT-solvers, propositional proof methods, and their applications (St\aa lmarck's saturation procedure, QBF, etc.) %\item Programming language theory (parametricity, semantics, %type systems, lazy evaluation, etc.) %\item Systems and runtime tools (new methods of concurrent %programming, runtime termination assurance, security, etc.) % %\end{itemize} % % \ \\ \section*{Short biography} Byron Cook is Professor of Computer Science at University College London. Byron is also a Senior Principal at Amazon Web Services. Byron's research interests include topics in formal methods, logic and and programming languages. Byron also has interest and expertise in the areas of hardware and systems, based on previous work experience in Intel's microprocessor design division and Microsoft's Windows kernel team. To date Byron has 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 ({\em 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 \textsc{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 \textsc{SLAM}, which is often credited for the recent revival of automatic program verification research, and \textsc{SLAyer} which is the best-of-class program verification tool supporting programs that make non-trivial use of the heap. At Amazon Byron leads a research group focused on formal/constraint-based tools for reasoning about cloud-computing security. %As well as traditional industrial research activities (publishing research papers, working with product groups, supervising interns, internal Microsoft lectures, etc), Byron has been active in academic outreach. For example, he has taught several semester-long courses at top universities (CMU, Berkeley, Cambridge) on termination and was invited to give a set of lectures at the prestigious Marktoberdorf summer school. % I am a principal researcher at Microsoft's laboratory at Cambridge University, and % full professor of computer science at Queen Mary, University of London. % My research interests include topics in formal methods, logic and % and programming languages. % I also have an interest and % expertise in the areas of hardware and systems, based on previous % work experience in Intel's microprocessor design division and % Microsoft's Windows kernel team. To date % I have worked actively in the areas of functional programming, % hardware modeling and design, % SAT-solving, symbolic model checking for finite-state systems, % decision procedures, and automatic program verification. % % My recent research in automatic program verification % has gained significant attention ({\em e.g.} % a substantial publication record, numerous keynote speaker invitations, and press hits in Scientific American, Vogue, Financial Times, Economist, and Wired). I am particularly well known for my work on automatic methods for proving program termination---this work represents a breakthrough, challenging the prevailing opinion in computer science that automatic termination proving is impossible. I am also well known for my contributions to \textsc{SLAM}, which % is often credited for the recent revival of automatic program verification research. My new work on hardware synthesis for C programs % promises to lead to further high impact in the area of computer design and % verification. % % As well as traditional industrial research activities (publishing research papers, working with product groups, supervising interns, internal Microsoft lectures, etc), I have been active in academic outreach. For example, I have taught several courses at top universities (CMU, Berkeley, Cambridge) on termination and was invited to give a set of lectures at the prestigious Marktoberdorf summer school. % I also supervise Ph.D. students % and postdoctoral researchers at Cambridge University % as well as Microsoft researchers and developers. %\section*{Featured publications} % %\begin{itemize} %\item {\em Termination proving is not impossible after all}\\ % Byron Cook\\ % Communications of the ACM ({\em forthcoming}) \\ % {Summary:} {\em This review paper synthesizes the 15+ %published research papers related to the development of the % \textsc{Terminator} termination prover into a single coherent form. } % %\item %{\em Termination proofs for systems code} \\ %Byron Cook, Andreas Podelski, and Andrey Rybalchenko \\ %PLDI [International Conference on Programming Language Design and Implementation], Ottawa, 2006\\ % {Summary:} {\em Breakthrough paper describing a new method of proving %program termination which lead to the % \textsc{Terminator} termination prover. } % %\item {\em Shape analysis for composite data structures} \\ %Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter O'Hearn, Thomas Wies, and Hongseok Yang \\ %CAV [International Conference on Computer-Aided Verification], %Berlin, 2007 %{Summary:} {\em This paper describes the technology behind the %\textsc{SLAyer} shape analysis engine.} %\item %{\em 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 [European Systems Conference], Leuven, 2006 \\ %{Summary:} {\em This paper describes the technology and experimental %evidence which lead to the Windows %\textsc{SDV} product.} %\end{itemize} \section*{Publications} \begin{center} {\bf Conference articles} \end{center} \begin{enumerate} \item {\em T2: temporal property verification}\\ Marc Brockschmidt, Byron Cook, Samin Ishtiaq, Heidy Khlaaf, and Nir Piterman\\ TACAS [International Conference on Tools and Algorithms for the Construction and Analysis of Systems], Eindhoven, 2016 \item {\em On automation of CTL$^*$ verification for infinite-state systems}\\ Byron Cook, Heidy Khlaaf and Nir Piterman\\ CAV [International Conference on Computer-Aided Verification], San Francisco, 2015 \item {\em Spatial interpolants} \\ Aws Albarghouthi, Josh Berdine, Byron Cook and Zachary Kincaid \\ ESOP [European Symposium on Programming], London, 2015 \item {\em Fairness for infinite-state systems}\\ Byron Cook, Heidy Khlaaf and Nir Piterman\\ TACAS [International Conference on Tools and Algorithms for the Construction and Analysis of Systems], London, 2015 \item {\em Proving nontermination via safety} \\ Hong Yi Chen, Byron Cook, Carsten Fuhs, Kaustubh Nimkar, Peter W. O'Hearn\\ TACAS [International Conference on Tools and Algorithms for the Construction and Analysis of Systems], Grenoble, 2014 \item {\em Faster temporal reasoning for infinite-state programs}\\ Byron Cook, Heidy Khlaaf, Nir Piterman \\ FMCAD [International Conference on Formal Methods in Computer Aided Design], Lausanne, 2014 \item {\em Disproving termination with overapproximation}\\ Byron Cook, Carsten Fuhs, Kaustubh Nimkar, Peter O'Hearn \\ FMCAD [International Conference on Formal Methods in Computer Aided Design], Lausanne, 2014 \item {\em Finding instability in biological models}\\ Byron Cook, Jasmin Fisher, Benjamin A. Hall, Samin Ishtiaq, Garvit Juniwal, Nir Piterman\\ CAV [International Conference on Computer-Aided Verification], Vienna, 2014 \item {\em Better termination proving through cooperation} \\ Marc Brockschmidt, Byron Cook and Carsten Fuhs \\ CAV [International Conference on Computer-Aided Verification], St. Petersburg, 2013 \item {\em Reasoning about nondeterminism in programs} \\ Byron Cook and Eric Koskinen \\ PLDI [International Conference on Programming Language Design and Implementation], Seattle, 2013 \item {\em Ramsey vs. lexicographic termination proving} \\ Byron Cook, Abigail See, and Florian Zuleger \\ TACAS [International Conference on Tools and Algorithms for the Construction and Analysis of Systems], Rome, 2013 \item {\em At the interface of biology and computation} \\ Alex S. Taylor, Nir Piterman, Samin Ishtiaq, Jasmin Fisher, Byron Cook, Caitlin Cockerton, Sam Bourton, and David Benque \\ CHI [ACM SIGCHI Conference on Human Factors in Computing Systems], Paris, 2013 \item {\em 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 [International Conference on Computer-Aided Verification], Berkeley, 2012 \item {\em Temporal property verification as a program analysis task} \\ Byron Cook, Eric Koskinen, Moshe Vardi \\ CAV [International Conference on Computer-Aided Verification], Snowbird, 2011 \item {\em SLAyer: Memory safety for systems-level code} \\ Josh Berdine, Byron Cook, Samin Ishtiaq \\ CAV [International Conference on Computer-Aided Verification], Snowbird, 2011 \item {\em Making prophecies with decision predicates} \\ Byron Cook and Eric Koskinen\\ POPL [International Symposium on Principles of Programming Languages], Austin, 2011 \item {\em Proving stabilization of biological systems} \\ Byron Cook, Jasmin Fisher, Elzbieta Krepska, Nir Piterman \\ VMCAI [International Conference on Verification, Model Checking, and Abstract Interpretation], Savannah, 2011 \item {\em Tractable Reasoning in a Fragment of Separation Logic} \\ Byron Cook, Christoph Haase, Joel Ouaknine, Matthew Parkinson and James Worrell\\ CONCUR [International Conference on Concurrency Theory], Aachen, 2011 \item {\em Ranking function synthesis for bit-vector relations}\\ Byron Cook, Daniel Kroening, Philipp Ruemmer, and Christoph Wintersteiger\\ TACAS [International Conference on Tools and Algorithms for the Construction and Analysis of Systems], Paphos, 2010 \item {\em Finding heap-bounds for hardware synthesis}\\ Byron Cook, Ashutosh Gupta, Stephen Magill, Andrey Rybalchenko, Jiri Simsa, Satnam Singh, and Viktor Vafeiadis\\ FMCAD [International Conference on Formal Methods in Computer Aided Design], Austin, 2010 \item {\em Proving that non-blocking algorithms don't block} \\ Alexey Gotsman, Byron Cook, Matthew Parkinson, and Viktor Vafeiadis\\ POPL [International Symposium on Principles of Programming Languages], Savannah, 2009 \item {\em Proving conditional termination} \\ Byron Cook, Sumit Gulwani, Tal Lev-Ami, Andrey Rybalchenko, and Mooly Sagiv\\ CAV [International Conference on Computer-Aided Verification], Princeton, 2008 \item {\em Scalable shape analysis for systems code}\\ Hongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, and Peter O'Hearn\\ CAV [International Conference on Computer-Aided Verification], Princeton, 2008 \item {\em Ranking abstractions} \\ Aziem Chawdhary, Byron Cook, Sumit Gulwani, Mooly Sagiv, and Hongseok Yang \\ ESOP [European Symposium on Programming], Budapest, 2008 \item {\em Proving thread termination} \\ Byron Cook, Andreas Podelski, and Andrey Rybalchenko, \\ PLDI [International Conference on Programming Language Design and Implementation], San Diego, 2007 \item {\em Thread-modular shape analysis} \\ Alexey Gotsman, Josh Berdine, Byron Cook, and Mooly Sagiv, \\ PLDI [International Conference on Programming Language Design and Implementation], San Diego, 2007 \item {\em Local reasoning for storable locks and threads} \\ Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky, and Mooly Sagiv \\ APLAS [Asian Symposium on Programming Languages and Systems], Singapore, 2007 \item {\em Proving that programs eventually do something good } \\ Byron Cook, Alexey Gotsman, Andreas Podelski, Andrey Rybalchenko, and Moshe Vardi \\ POPL [International Symposium on Principles of Programming Languages], Nice 2007 \item {\em Variance analyses from invariance analyses } \\ Josh Berdine, Aziem Chawdhary, Byron Cook, Dino Distefano, and Peter O'Hearn \\ POPL [International Symposium on Principles of Programming Languages], Nice 2007 \item {\em Shape analysis for composite data structures} \\ Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter O'Hearn, Thomas Wies, and Hongseok Yang \\ CAV [International Conference on Computer-Aided Verification], Berlin, 2007 \item {\em Arithmetic strengthening for shape analysis}\\ Stephen Magill, Josh Berdine, Edmund Clarke, and Byron Cook, \\ SAS [International Static Analysis Symposium], Denmark, 2007 \item {\em Proving termination by divergence} \\ Domagoj Babic, Byron Cook, Alan Hu, and Zvonimir Rakamaric \\ SEFM [International Conference on Software Engineering and Formal Methods], London, 2007 \item {\em Shape analysis by graph decomposition} \\ Roman Manevich, Josh Berdine, Byron Cook, Ganesan Ramalingam, and Mooly Sagiv \\ TACAS [International Conference on Tools and Algorithms for the Construction and Analysis of Systems], Braga, 2007 \item {\em Over-approximating Boolean programs with unbounded thread creation}\\ Byron Cook, Daniel Kroening, Natasha Sharygina \\ FMCAD [International Conference on Formal Methods in Computer Aided Design], San Jose, 2007 \item {\em Interprocedural shape analysis with separated heap abstractions} \\ Alexey Gotsman, Josh Berdine, and Byron Cook \\ SAS [International Symposium on Static Analysis], Seoul, 2007 \item {\em Automatic termination proofs for programs with shape-shifting heaps} \\ Josh Berdine, Byron Cook, Dino Distefano, and Peter O'Hearn \\ CAV [International Conference on Computer-Aided Verification], Seattle, 2006 \item {\em Terminator: Beyond safety} \\ Byron Cook, Andreas Podelski, and Andrey Rybalchenko \\ CAV [International Conference on Computer-Aided Verification], Seattle, 2006 \item {\em Repair of Boolean programs with an application to C} \\ Andreas Griesmayer, Roderick Bloem, and Byron Cook \\ CAV [International Conference on Computer-Aided Verification], Seattle, 2006 \item {\em Termination proofs for systems code} \\ Byron Cook, Andreas Podelski, and Andrey Rybalchenko \\ PLDI [International Conference on Programming Language Design and Implementation], Ottawa, 2006 \item {\em 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 [European Systems Conference], Leuven, 2006 \item {\em Abstraction-refinement for termination} \\ Byron Cook, Andreas Podelski, Andrey Rybalchenko \\ SAS [International Symposium on Static Analysis], London, 2005 \item {\em Using St\aa lmarck's algorithm to prove inequalities} \\ Byron Cook and George Gonthier\\ ICFEM [International Conference on Formal Engineering Methods], Manchester, 2005 \item {\em Predicate abstraction via symbolic decision procedures} \\ Shuvendu Lahiri, Thomas Ball, and Byron Cook\\ CAV [International Conference on Computer-Aided Verification], Edinburgh, 2005 \item {\em Cogent: Accurate theorem proving for program verification} \\ Byron Cook, Daniel Kroening, and Natasha Sharygina\\ CAV [International Conference on Computer-Aided Verification], Edinburgh, 2005 \item {\em Zapato: Automatic theorem proving for predicate abstraction refinement} \\ Thomas Ball, Byron Cook, Shuvendu K. Lahiri, and Lintao Zhang \\ CAV [International Conference on Computer-Aided Verification], Boston, 2004 \item {\em Refining approximations in software predicate abstraction} \\ Thomas Ball, Byron Cook, Satyaki Das, and Sriram K. Rajamani \\ TACAS [International Conference on Tools and Algorithms for the Construction and Analysis of Systems], Barcelona, 2004 \item {\em SLAM and Static Driver Verifier: technology transfer of formal methods inside Microsoft},\\ Thomas Ball, Byron Cook, Vladimir Levin and Sriram K. Rajamani. \\ IFM [International Conference on Integrated Formal Methods], Kent, 2004 \item {\em Accurate theorem proving for program verification}, \\ Byron Cook, Daniel Kroening, Natasha Sharygina, \\ ISoLA [Leveraging Applications of Formal Methods], Paphos, 2004 \item {\em A symbolic approach to predicate abstraction} \\ Shuvendu K. Lahiri, Randall E. Bryant, and Byron Cook \\ CAV [International Conference on Computer-Aided Verification], Boulder, 2003 \item {\em A proof engine approach to solving combinational design automation problems} \\ Gunnar Andersson, Per Bjesse, Byron Cook, and Ziyad Hanna \\ DAC [Design Automation Conference], Las Vegas, 2002 \item {\em A framework for microprocessor correctness statements} \\ Mark Aagaard, Byron Cook, Nancy Day, and Robert Jones \\ CHARME [Advanced Research Working Conference on Correct Hardware Design and Verification Methods], Edinburgh, 2001 \item {\em Combining stream-based and state-based verification techniques for microarchitectures} \\ Mark Aagaard, Byron Cook, and Nancy Day \\ FMCAD [International Conference on Formal Methods in Computer Aided Design], Austin, 2000 \item {\em Formal verification of explicitly parallel microprocessors} \\ Byron Cook, John Launchbury, John Matthews, and Dick Kieburtz \\ CHARME [Advanced Research Working Conference on Correct Hardware Design and Verification Methods], Bad Herrenalb, 1999 \item {\em On embedding a microarchitectural design language within Haskell} \\ John Launchbury, Jeff Lewis and Byron Cook \\ ICFP [International Conference on Functional Programming], Paris, 1999 \item {\em Microprocessor specification in Hawk} \\ John Matthews, John Launchbury, and Byron Cook \\ ICCL [International Conference on Computer Languages], Chicago, 1998 \begin{center} {\bf Journal articles} \end{center} \item {\em Drug target optimization in chronic myeloid leukemia using innovative computational platform} \\ R. Chuang, B. Hall, D. Benque, B. Cook, S. Ishtiaq, N. Piterman, A. Taylor, M. Vardi, S. Koschmieder, B. Gottgens, and J. Fisher \\ Scientific Reports, 5:8190, Nature Publishing Group, February 2015 \item {\em Relations} \\ Tauba Auerbach, Byron Cook, David Reinfurt \\ Bulletins of the Serving Library, 2014 \item {\em Mathematical artifacts} \\ Byron Cook\\ Parkett 94, 2014 \item {\em Ranking function synthsis for bit-vector relations}\\ Byron Cook, Daniel Kroening, Philipp R\"ummer, Christoph Winterstieger \\ International Journal on Formal Methods in System Design, March, 2013 \item {\em Proving termination of nonlinear command sequences} \\ Domagoj Babic, Byron Cook, Alan J. Hu, Zvonimir Rakamaric \\ International Journal on Formal Aspects of Computing (special issue from SEFM), 2013 \item {\em Temporal property verification as a program analysis task (extended version)}\\ Byron Cook, Eric Koskinen, Moshe Vardi \\ International Journal on Formal Methods in System Design (special issue from CAV), 2012 \item {\em Proving program termination}\\ Byron Cook, Andreas Podelski, Andrey Rybalchenko\\ Communications of the ACM, Volume 54 Issue 5, May 2011 \item {\em Summarization for termination}\\ Byron Cook, Andreas Podelski, and Andrey Rybalchenko\\ International Journal on Formal Methods in System Design, Vol 35, pp. 369--387 \item {\em Software engineering and formal methods}\\ Mike Hinchey, Michael Jackson, Patrick Cousot, Byron Cook, Jonathon P. Bowen\\ Communications of the ACM, Vol. 51, 2008, pp. 54-59 \item {\em 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 \item {\em Predicate abstraction via symbolic decision procedures} \\ Shuvendu Lahiri, Tom Ball, and Byron Cook \\ Journal of Logic Methods in Computer Science, Vol. 3(1:2), 2007, pp. 1-20 %\item {\em Iteratively proving program termination} \\ %Byron Cook, Andreas Podelski, and Andrey Rybalchenko \\ %Submitted for review, 2007 \item {\em Design automation with mixtures of proof strategies for propositional logic} \\ Gunnar Andersson, Per Bjesse, Byron Cook, and Ziyad Hanna \\ IEEE Transactions on CAD, Vol. 22(8), 2003, pp. 1042-1048 \item {\em 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), 2002, pp. 298-312 \begin{center} {\bf Books} \end{center} \item {\em Program termination} \\ Byron Cook\\ Cambridge University Press (forthcoming) \item {\em Computer Aided Verification} \\ Byron Cook, Tayssir Touili, Paul Jackson (Eds.) \\ Springer, 2010 \item {\em Formal Methods for Industrial Critical Systems} \\ Maria Alpuente, Byron Cook, Christophe Joubert (Eds.) \\ Springer, 2009 \item {\em Proceedings of the 8th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)} \\ Byron Cook and Andreas Podelski (Eds.) \\ Springer, 2007 \begin{center} {\bf Journal special issues} \end{center} \item {\em Special Issue on Satisfiability Modulo Theories} \\ Byron Cook and Roberto Sebastiani (Eds.) \\ Journal on Satisifiability, Boolean Modeling and Computation \begin{center} {\bf Workshop articles} \end{center} \item {\em Learning to decipher the heap for program verification}\\ Mark Brockschmidt, Yuxin CHen, Byron Cook, Pushmeet Kohli, and Daniel Tarlow\\ Workshop on Constructivee Machine Learning at ICML, 2015 \item {\em Symbolic model checking for asynchronous Boolean programs}\\ Byron Cook, Daniel Kroening, and Natasha Sharygina\\ SPIN [SPIN Workshop on Model Checking of Software], San Francisco, 2005 \item {\em Specifying superscalar microprocessors in Hawk} \\ Byron Cook, John Launchbury, and John Matthews \\ FTH [International Workshop on Formal Techniques for Hardware], Marstrand, 1998 \item {\em Disposable memo functions} \\ Byron Cook and John Launchbury \\ Haskell Workshop, Amsterdam, 1997 \begin{center} {\bf Invited articles} \end{center} \item {\em Principles of program termination} \\ Byron Cook \\ Lecture notes from 2008 Marktoberdorf summer school (Marktoberdorf) \item {\em Advances in Program Termination and Liveness} \\ Byron Cook \\ VMCAI [International Conference on Verification, Model Checking, and Abstract Interpretation], Savannah, 2009 \item {\em Computing bounds on space and time for hardware compilation} \\ Byron Cook \\ FMCAD [Formal Methods in Computer Aided Design], Portland, 2008 \item {\em Automatically proving program termination} \\ Byron Cook \\ CAV [International Conference on Computer-Aided Verification], Berlin, 2007 \item {\em Bringing hardware and software closer together with termination analysis} \\ Byron Cook \\ MEMOCODE [International Conference on Formal Methods and Models for Codesign], Nice, 2007 \item {\em Automatically Proving Concurrent Programs Correct} \\ Byron Cook \\ SEFM [IEEE International Conference on Software Engineering and Formal Methods], London, 2007 \item {\em Finding bugs in device drivers with Static Driver Verifier} \\ Byron Cook\\ ASM [International Conference on Abstract State Machines], Paris, 2005 \item {\em Finding API usage rule violations in Windows device drivers using Static Driver Verifier}\\ Byron Cook\\ ISoLA [Leveraging Applications of Formal Methods], Paphos, 2004 \end{enumerate} \ \\ \section*{Grants} \begin{itemize} \item ``Compositional Security Analysis for Binaries'' (EPSRC), 290k GBP \item ``Boosting Automated Verification Using Cyclic Proof'' (EPSRC), 550k GBP \item ``Program Verification Techniques for Understanding Security Properties of Software'' (EPSRC), 877k GBP \end{itemize} \section*{Awards} \begin{itemize} \item Roger Needham Award, 2009. The Roger Needham Award 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. The award includes a 5,000 GBP cash prize, and a public lecture at the UK's Royal Society in London. \end{itemize} \ \\ \section*{Press coverage} \begin{itemize} \item {\em Why the blue screen of death no longer plagues Windows users }, Nick Heath, ZDNet, September, 2013 \item {\em Modelling: Computing Cancer}, Neil Savage, Nature, November 2012 \item {\em Dr. Byron Cook: Geek of the week}, Richard Morris, Simple-Talk, September, 2010 \item {\em Sign Of The Times}, Cameron Bird, Wired, December 2009 \item {\em A Good Sign}, Angela Saini, Science, July 2009 \item {\em Optic Nerve}, Dodie Kazanjain, Vogue, January 2009 \item {\em All Shook Down}, Hiya Swanhuyser, San Francisco Weekly, December 2008 \item {\em Byron Cook: Terminator - Proving good things will eventually happen } (Video interview), Charles Torre, MSDN, July 2007 \item {\em Byron Cook: Inside Terminator} (Video interview), Charles Torre, MSDN, September 2007 \item {\em Send in the Terminator}, Gary Stix, Scientific American, December 2006 \item {\em Testers aim to kill off dreaded blue screens}, Mary Branscombe, Financial Times, November 22nd, 2006 \item {\em Microsoft creates an application terminator}, Andy Patrizio, Internet News, August, 2006 \item {\em Microsoft researcher aims to make software more predictable}, Tony Baer, Computer Wire, August, 2006, \item {\em Microsoft bug-checking tools promise fewer crashes}, Joris Evens, CNET, May 26, 2006 \item {\em Microsoft's secret bug squasher}, Simson Garfinkel, Wired, November, 2005 \item {\em Researching a path to fewer bugs}, Patrick Meader, Visual Studio Magazine, February 2003 \item {\em Building a better bug-trap }, Economist, June 19th, 2003 \end{itemize} \ \\ \section*{Graduate students} \begin{itemize} \item Alexey Gotsman. Completed PhD: 2009. Assistant Research Professor at IMDEA (Madrid Institute for Advanced Studies) \item Eric Koskinen. Completed Phd: 2012. Research Scientist at Yale. \item Kaustubh Nimkar. Completed PhD: 2015. Developer at Bloomberg \item Paul Subotic. Completion expected: 2019 \end{itemize} \ \\ \section*{Teaching} \begin{itemize} \item {\em Program termination}, 4 graduate-level lecture hours at University of California, Berkeley, 2009 \item {\em Program termination}, 6 graduate-level lecture hours at the International Summer School on Trends in Concurrency (Prague), 2008 \item {\em Program termination}, 5 graduate-level lecture hours at the Marktoberdorf Summer School, 2008 \item {\em Program termination}, 6 graduate-level lecture hours at the International Summer School on Trends in Concurrency (Prague), 2008 \item {\em Program termination}, 24 graduate-level lecture hours at Carnegie Mellon University, 2008 \item {\em Program termination}, 6 graduate-level lecture hours at Imperial College, 2008 \item {\em Program termination}, 6 graduate-level lecture hours at Cambridge University, 2007 \item {\em Introduction to C++}, 20 undergraduate-level lecture hours at The Evergreen State College, 1998 \item {\em Constructing Applets in Java}, 10 undergraduate-level lecture hours at The Evergreen State College, 1998 \item {\em C++ and Java, Object Oriented Programming}, 20 undergraduate-level lecture hours at The Evergreen State College, 1997 \item {\em C programming language: Introduction}, 20 undergraduate-level lecture hours at The Evergreen State College, 1997 \item {\em Web programming in Perl}, 10 undergraduate-level lecture hours at The Evergreen State College, 1997 \item {\em Introduction to Computer Science II}, 20 undergraduate-level lecture hours at Portland Community College, 1997 \item {\em Introduction to Computer Programming}, 20 undergraduate-level lecture hours at Oregon Institute of Technology, 1997 \item {\em Introduction to Data Structures}, 20 undergraduate-level lecture hours at Oregon Institute of Technology, 1997 \item {\em Introduction to Programming for the World Wide Web}, 20 undergraduate-level lecture hours at The Evergreen State College, 1996 \item {\em Introduction to UNIX Operating System}, 20 undergraduate-level lecture hours at The Evergreen State College, 1996 \item {\em Introduction to Computer Science I}, 20 undergraduate-level lecture hours at Portland Community College, 1996 \end{itemize} \ \\ \section*{Tools developed} \begin{itemize} \item \textsc{BMA} : Biological model analysis tool \\ {\tt http://biomodelanalyzer.research.microsoft.com} \item \textsc{T2} : Program termination prover \\ {\tt http://research.microsoft.com/en-us/projects/t2/} \item \textsc{Terminator} : Program termination prover \\ {\tt http://research.microsoft.com/TERMINATOR} \item \textsc{SLAyer} : Shape analysis engine \\ {\tt http://research.microsoft.com/SLAyer} \item \textsc{SLAM} : Symbolic software model checker \\ {\tt http://research.microsoft.com/SLAM} \item Static Driver Verifier : Device driver correctness tool (Microsoft Windows product released through the Windows Device Driver Development Kit) \\ {\tt http://www.microsoft.com/whdc/devtools/tools/SDV.mspx} \item \textsc{Zapato} : Decision procedure framework \\ (Microsoft internal) \item \textsc{Poindexter} : Pointer analysis engine \\ (Microsoft internal) \item \textsc{Prover CL} : Propositional SAT solver \\ {\tt http://www.prover.com/products/ppi/cl.xml} \item \textsc{Prover SL} : Symbolic model checker for finite-state systems \\ {\tt http://www.prover.com/products/ppi/sl.xml} \item \textsc{HLSpec} : High-level microprocessor design language and tools \\ (Intel internal) \item \textsc{Hawk} : High-level microprocessor design language and tools \\ {\tt http://www.cse.ogi.edu/PacSoft/projects/Hawk/} \end{itemize} \ \\ \section*{Invited talks, keynotes and tutorials} \begin{itemize} \item WST [International Workshop on Termination], Bertinoro (Italy), 2013 \item Workshop on Software Correctness and Reliability, Zurich, 2013 \item POPL (tutorial) [Symposium on Principles of Programming Languages], Philadelphia, 2012 \item Dutch Model Checking Day, Amsterdam, 2012 \item SIGPLAN Programming Languages Mentoring Workshop, Philadelphia, 2012 \item Manycore workshop, Birmingham, 2012 \item CAV workshop on Applications of Formal Methods in Systems Biology, Berkeley, 2012 \item Bright Club, London, April 2012 \item HCSS [International Conference on High Confidence Software and Systems], Annapolis, 2012 \item CADE [International Conference on Automated Deduction], Wroclaw, 2011 \item ECOOP Summer School [European Conference on Object-Oriented Programming ], Lancaster, 2011 \item Dutch Model Checking Day, Delft, 2011 \item IFIP Working Group 2.3, Santa Barbara, 2011 \item Workshop on Theory Engineering, Cambridge, 2010 \item IFIP Working Group 2.3, Zurich, 2010 \item Royal Society, London, 2009 \item Midlands Graduate School Christmas Seminar, 2009 \item HCSS [International Conference on High Confidence Software and Systems], Baltimore, 2009 \item NFM [NASA Formal Methods Symposium], Moffett Field, 2009 \item VMCAI [International Conference on Verification, Model Checking, and Abstract Interpretation], Savannah, 2009 \item IFM [Integrated Formal Methods], Dusseldorf, 2009 \item Infinity [International Workshop on Verification of Infinite-State Systems], Bologna, 2009 \item Workshop on Applied Logic: Inductive and Deductive Reasoning, 2009 \item IFIP Working Group 2.3, Cambridge, 2008 \item Marktoberdorf Summer School, 2008 \item FMCAD [Formal Methods in Computer Aided Design], Portland, 2008 \item HCSS [International Conference on High Confidence Software and Systems], Baltimore, 2008 \item International Summer School on Trends in Concurrency (Prague), 2008 \item CAV Workshop on Numerical Abstractions for Software Verification, 2008 \item Science of Security Workshop, Berkeley, 2008 \item QCon Enterprise Software Development Conference, San Francisco, 2007 \item CAV [International Conference on Computer-Aided Verification] Berlin, 2007 \item HCSS [International Conference on High Confidence Software and Systems], Baltimore, 2007 \item MEMOCODE [International Conference on Formal Methods and Models for Codesign] (Nice), 2007 \item SEFM [IEEE International Conference on Software Engineering and Formal Methods] London, 2007 \item Seminar on the Challenge of Software Verification, Dagstuhl, 2006 \item WST [International Workshop on Termination], Seattle, 2006 \item SVV [International Workshop on Software Verification and Validation], Seattle, 2006 \item AVoCS [International Workshop on Automated Verification of Critical Systems], Nancy, 2006 \item ARW [Automated Reasoning Workshop], Bristol, 2006 \item ICSSR [International Computer Science Symposium in Russia], St. Petersburg, 2006 \item ESCAR [CADE Workshop on Empirically Successful Classical Automated Reasoning], 2005 \item DISPROVING [Workshop on Disproving - Non-Theorems, Non-Validity, Non-Provability] Tallinn, 2005 \item ASM [International Workshop on Abstract State Machines], Paris, 2005 \item Combination of Decision Procedures Summer School, Stanford, 2004 \item HCSS [Conference on High Confidence Software and Systems], Baltimore, 2004 \item ISoLA [Leveraging Applications of Formal Methods] (Paphos) \item Colloquium L'ingnierie du logiciel, Paris, 2004 \item DAC [Design Automation Conference], Las Vegas 2001 \item University colloquium lectures at Stanford, Berkeley, Carnegie Mellon, Harvard, MIT, ETH, INRIA, University of Toronto, University of Birmingham, University of Manchester, University of British Columbia, University of Utah, University of Colorado, Oxford, Cambridge, Chalmers, and New York University. \item Internal symposiums at Compaq, Intel, the US National Security Agency, and Siemens. \item Microsoft Techfest\footnote{Techfest is a Microsoft event in which researchers give lectures and make demos available to Microsoft employees and the press. The event is high-profile ($>$30,000 attendees) and the lectures are selected using a competitive process.} in 2011, 2009, 2007, 2006, and 2005 %\item Bill Gates review (2006 %\item Bill Gates demo 2010 \end{itemize} \ \\ \section*{Panel discussions} \begin{itemize} \item NASA Formal Methods Symposium, Moffett Field, 2009 \item Science of Security Workshop, Berkeley, 2008 \item SMT [International Workshop on Satisfiability Modulo Theories], Princeton, 2008 \item HCSS [International Conference on High Confidence Software and Systems], Baltimore, 2008 \item University of Illinois Affiliates Conference, 2006 \item MEMOCODE [International Conference on Formal Methods and Models for Codesign] Verona, 2005 %\item DAC [Design Automation Conference], Los Angeles, 2000 \end{itemize} \ \\ \section*{Professional activities} \begin{itemize} \item Advisory board \begin{itemize} \item DeepSpec/NSF \end{itemize} \item Program committee appointments: \begin{itemize} \item VMCAI [International Conference on Verification, Model Checking, and Abstract Interpretation], 2017 \item CAV [International Conference on Computer-Aided Verification], 2015 \item CAV [International Conference on Computer-Aided Verification], 2014 \item CAV [International Conference on Computer-Aided Verification], 2013 \item RTA [Rewriting Techniques and Applications], 2013 \item PLDI [International Conference on Programming Language Design and Implementation], 2012 \item FMCAD [Formal Methods in Computer-Aided Design], 2012 \item SAS [International Static Analysis Symposium], 2011 \item FM [International Symposium on Formal Methods], 2011 \item PADL [International Symposium on Practical Aspects of Declarative Languages], 2011 \item SAS [International Static Analysis Symposium], 2010 \item CAV [International Conference on Computer-Aided Verification], 2010 \item CAV [International Conference on Computer-Aided Verification], 2009 \item FMICS [Formal Methods for Industrial Critical Systems], 2009 \item WST [International Workshop on Termination], 2009 \item POPL [Symposium on Principles of Programming Languages], 2008 \item TACAS [International Conference on Tools and Algorithms for the Construction and Analysis of Systems], 2008 \item SSV [International Workshop on Systems Software Verification], 2008 \item LPAR [International Conference on Logic for Programming Artificial Intelligence and Reasoning], 2007 \item VMCAI [International Conference on Verification, Model Checking, and Abstract Interpretation], 2007 \item TACAS [International Conference on Tools and Algorithms for the Construction and Analysis of Systems], 2007 \item SMT [International Workshop on Satisfiability Modulo Theories], 2007 \item SV [International Workshop on System Verification], 2007 \item TV [Thread Verification Workshop], 2006 \item PDPAR [Pragmatics of Decision Procedures in Automated Reasoning], 2006 \item SoftMC [Software Model Checking Workshop], 2005 \item CUFP [ICFP Workshop on Commercial Users of Functional Programming], 2004 \item SoftMC [Software Model Checking Workshop], 2003 \item CHARME [Advanced Research Working Conference on Correct Hardware Design and Verification Methods], 2003 \end{itemize} \item Co-organizer, HCSS [International Conference on High Confidence Software and Systems], Annapolis, 2013 \item External review committee, PLDI [International Conference on Programming Language Design and Implementation], 2013 \item External review committee, PLDI [International Conference on Programming Language Design and Implementation], 2010 \item Steering committee, International Workshop on Satisfiability Modulo Theories \item Co-chair, CAV [International Conference on Computer-Aided Verification], Edinburgh, 2010 \item Co-chair, FMICS [Formal Methods for Industrial Critical Systems], Eindhoven, 2009 \item Workshops chair, CAV [International Conference on Computer-Aided Verification], Princeton, 2008 \item Associate Editor, ACM Transactions on Programming Languages and Systems, 2009-2012 \item Guest co-editor, Journal on Satisfiability, Boolean Modeling, and Computation (Special Issue on Satisfiability Modulo Theories), \item Program chair for tools papers, TACAS [International Conference on Tools and Algorithms for the Construction and Analysis of Systems], 2008 \item Co-organizer, {\em Seminar on Deduction and Decision Procedures}, Schloss Dagstuhl, 2007 \item Co-chair, AHA [International Symposium on Automatic Heap Analysis], 2007 \item Co-chair, VMCAI [International Conference on Verification, Model Checking, and Abstract Interpretation], 2007 \item Co-organizer, SSPV [Symposium on SAT-solvers and Program Verification], 2006 \item Co-chair, PDPAR [Pragmatics of Decision Procedures in Automated Reasoning], 2006 \item Program chair for tools papers, TACAS [International Conference on Tools and Algorithms for the Construction and Analysis of Systems], 2007 \item Co-organizer of SoftMC'05 and SoftMC'03 [CAV Workshop on Software Model Checking] \item Co-organizer of CFDP'05 [Cambridge Forum on Decision Procedures] \item External Ph.D. reviewer: Albert Oliveras (Barcelona), Stephen Magill (CMU), Daron Vroon (Georgia Tech), Jonathan Heusser (Queen Mary), Jules Villard (Cachan), Elzbieta Krepska (VU Amsterdam) \item Grant reviewing: UK Engineering and Physical Sciences Research Council (EPSRC), European Research Council (ERC) \item Committee EAPLS Best PhD Dissertation Award 2011 \item MSR Internship supervision: Aws Albarghouthi, Mary Boeker, Marc Brockschmidt, Hongyi Chen, Ashutosh Gupta, Mihaela Gheorghiu, Alexey Gotsman, Christoph Haase, Zachary Kincaid, Heidy Khlaaf, Matt Lewis, Shuvendu Lahiri, Stephen Magill, Andrei Popescu, Patrick Rondon, Andrey Rybalchenko, Abigail See, Vlad Shcherbina, Jiri Simsa, Thomas Stroeder, Viktor Vafeiadis, Georg Weissenbacher, Thomas Wies, and Greta Yorsh. %\item %Reviewed papers for CAV %[International Conference on Computer-Aided Verification], % TACAS [International Conference on Tools % and Algorithms for the Construction and Analysis of Systems], % POPL [Principles of Programming Languages], % ICFP [International Conference on Functional Programming], % among others. \end{itemize} \ \\ \section*{Work history} \begin{center} {\bf Academic positions} \end{center} \begin{itemize} \item University College London, Professor, 2012-Current \item Queen Mary, University of London, Professor (joint with Microsoft), 2008-2012 % Contact: Edmund Robinson, {\tt edmundr@dcs.qmul.ac.uk} \item Carnegie Mellon University, Visiting Professor, 2008 % Contact: Randy Bryant, {\tt Randy.Bryant@cs.cmu.edu} \item Queen Mary, University of London, Visiting Professor, 2006-2008 %Contact: Edmund Robinson, {\tt edmundr@dcs.qmul.ac.uk} \item Chalmers University, Visiting Lecturer, 2005-2006 %Contact: Mary Sheeran, {\tt ms@cs.chalmers.se} \item The Evergreen State College, Adjunct Lecturer, 1996-1998 % Contact: John Cushing, {\tt cushja@elwha.evergreen.edu} \item Portland Community College, Adjunct Lecturer, 1996-1997 % Contact: Marty Murray, {\tt mmurray@pcc.edu} \item Oregon Institute of Technology, Adjunct Lecturer, 1997 % Contact: Ira Smith, {\tt ira.smith@adapx.com} \end{itemize} \ \\ \begin{center} {\bf Industrial positions} \end{center} \begin{itemize} \item Amazon Web Services, Senior Principal, 2014-Current \end{itemize} \begin{itemize} \item Microsoft Research 2004-2014 \begin{itemize} \item Principal Researcher, group manager (Programming, Principles, and Tools group), MSR-Cambridge senior leadership team member 2011-2014 \item Principal Researcher, 2009-2011, \item Senior Researcher, 2008-2009, \item Researcher, 2004-2008 \end{itemize} \item Microsoft, Software developer (Base OS kernel team), 2002-2004 %\item Microsoft Base OS group, Software developer, 2002-2004 %\item Monoidics Ltd, Corporate Board Member, 2008-Current \item Prover Technology AB, Software developer, 1999-2002 % Contact: Gunnar St\aa lmarck, {\tt gust@prover.com} \item Intel Strategic CAD Labs, Software developer, 1998-1999 % Contact: Robert Jones {\tt rjones@ichips.intel.com} \end{itemize} \ \\ \section*{Education} \begin{itemize} \item Ph.D. The Oregon Graduate Institute of Science and Technology, Defended 2002, Advisor: John Launchbury \item B.Sci. The Evergreen State College, Graduated 1995. %\item Secondary school -- The Jefferson County Open School (Colorado). Graduated 1990 \end{itemize} \ \\ \section*{References} \begin{itemize} %\item Mike Gordon -- Cambridge University % \\ {\tt Mike.Gordon@cl.cam.ac.uk} %\item Sir Prof. Dr. Tony Hoare -- Microsoft Research % \\ {\tt thoare@microsoft.com} %\item Brad Martin -- National Security Agency % \\ {\em Contact information available on request} \item Prof. Dr. Peter O'Hearn -- University College London \\ {\tt p.ohearn@ucl.ac.uk} \item Prof. Dr. Andreas Podelski -- Freiburg University \\ {\tt podelski@informatik.uni-freiburg.de} \item Prof. Dr. Mooly Sagiv -- Tel Aviv University \\ {\tt msagiv@post.ta.ac.il} %\item Mary Sheeran -- Chalmers University of Technology \\ {\tt ms@cs.chalmers.se} %\item John Launchbury -- Galois Connections / Oregon Graduate Institute \\ % {\tt jl@cse.ogi.edu} \item Dr. Don Syme -- Microsoft Research \\ {\tt dsyme@microsoft.com} \item Dr. Jasmin Fisher -- Microsoft Research \\ {\tt Jasmin.Fisher@microsoft.com} %\item Sriram Rajamani -- Microsoft Research \\ % {\tt sriram@microsoft.com} %\item Robert Jones -- Intel Strategic CAD Labs \\ % {\tt rjones@ichips.intel.com} \item Prof. Dr. Moshe Vardi -- Rice University \\ {\tt vardi@cs.rice.edu} \end{itemize} \end{document}