Disposable Memo Functions (Extended Abstract). - Byron Cook; John Launchbury (ICFP, 1997)

Microprocessor Specification in Hawk. - John Matthews; Byron Cook; John Launchbury (ICCL, 1998)

Formal Verification of Explicitly Parallel Microprocessors. - Byron Cook; John Launchbury; John Matthews; Richard B. Kieburtz (CHARME, 1999)

Symbolic Simulation of Microprocessor Models using Type Classes in Haskell. - Nancy A. Day; Jeffrey R. Lewis; Byron Cook (CHARME, 1999)

On Embedding a Microarchitectural Design Language within Haskell. - John Launchbury; Jeffrey R. Lewis; Byron Cook (ICFP, 1999)

Combining Stream-Based and State-Based Verification Techniques. - Nancy A. Day; Mark D. Aagaard; Byron Cook (FMCAD, 2000)

A Framework for Microprocessor Correctness Statements. - Mark D. Aagaard; Byron Cook; Nancy A. Day; Robert B. Jones (CHARME, 2001)

A proof engine approach to solving combinational design automation problems. - Gunnar Andersson; Per Bjesse; Byron Cook; Ziyad Hanna (DAC, 2002)

A Symbolic Approach to Predicate Abstraction. - Shuvendu K. Lahiri; Randal E. Bryant; Byron Cook (CAV, 2003)

SoftMC 2003: Workshop on Software Model Checking. - Byron Cook; Scott D. Stoller; Willem Visser (SoftMC@CAV, 2003)

A framework for superscalar microprocessor correctness statements. - Mark D. Aagaard; Byron Cook; Nancy A. Day; Robert B. Jones (Int. J. Softw. Tools Technol. Transf., 2003)

Design automation with mixtures of proof strategies for propositional logic. - Gunnar Andersson; Per Bjesse; Byron Cook; Ziyad Hanna (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2003)

Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement. - Thomas Ball 001; Byron Cook; Shuvendu K. Lahiri; Lintao Zhang (CAV, 2004)

SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft. - Thomas Ball 001; Byron Cook; Vladimir Levin; Sriram K. Rajamani (IFM, 2004)

Finding API usage rule violations in Windows device drivers using Static Driver Verifier. - Byron Cook (ISoLA (Preliminary proceedings), 2004)

Accurate Theorem Proving for Program Verification. - Byron Cook; Daniel Kroening; Natasha Sharygina (ISoLA, 2004)

Refining Approximations in Software Predicate Abstraction. - Thomas Ball 001; Byron Cook; Satyaki Das; Sriram K. Rajamani (TACAS, 2004)

Finding Bugs in Device Drivers with Static Driver Verifier. - Byron Cook (Abstract State Machines, 2005)

Cogent: Accurate Theorem Proving for Program Verification. - Byron Cook; Daniel Kroening; Natasha Sharygina (CAV, 2005)

Using Stålmarck's Algorithm to Prove Inequalities. - Byron Cook; Georges Gonthier (ICFEM, 2005)

Abstraction Refinement for Termination. - Byron Cook; Andreas Podelski; Andrey Rybalchenko (SAS, 2005)

Symbolic Model Checking for Asynchronous Boolean Programs. - Byron Cook; Daniel Kroening; Natasha Sharygina (SPIN, 2005)

Preface. - Byron Cook; Scott D. Stoller; Willem Visser (SoftMC@CAV, 2005)

Automatic Termination Proofs for Programs with Shape-Shifting Heaps. - Josh Berdine; Byron Cook; Dino Distefano; Peter W. O'Hearn (CAV, 2006)

Terminator: Beyond Safety. - Byron Cook; Andreas Podelski; Andrey Rybalchenko (CAV, 2006)

Repair of Boolean Programs with an Application to C. - Andreas Griesmayer; Roderick Bloem; Byron Cook (CAV, 2006)

Thorough static analysis of device drivers. - Thomas Ball 001; Ella Bounimova; Byron Cook; Vladimir Levin; Jakob Lichtenberg; Con McGarvey; Bohus Ondrusek; Sriram K. Rajamani; Abdullah Ustuner (EuroSys, 2006)

Over-Approximating Boolean Programs with Unbounded Thread Creation. - Byron Cook; Daniel Kroening; Natasha Sharygina (FMCAD, 2006)

Termination proofs for systems code. - Byron Cook; Andreas Podelski; Andrey Rybalchenko (PLDI, 2006)

Interprocedural Shape Analysis with Separated Heap Abstractions. - Alexey Gotsman; Josh Berdine; Byron Cook (SAS, 2006)

Preface and Foreword. - Byron Cook; Roberto Sebastiani (PDPAR/PaUL@FLoC, 2006)

Local Reasoning for Storable Locks and Threads. - Alexey Gotsman; Josh Berdine; Byron Cook; Noam Rinetzky; Mooly Sagiv (APLAS, 2007)

Shape Analysis for Composite Data Structures. - Josh Berdine; Cristiano Calcagno; Byron Cook; Dino Distefano; Peter W. O'Hearn; Thomas Wies; Hongseok Yang (CAV, 2007)

Automatically Proving Program Termination. - Byron Cook (CAV, 2007)

07401 Executive Summary – Deduction and Decision Procedures. - Franz Baader; Byron Cook; Jürgen Giesl; Robert Nieuwenhuis (Deduction and Decision Procedures, 2007)

07401 Abstracts Collection – Deduction and Decision Procedures. - Franz Baader; Byron Cook; Jürgen Giesl; Robert Nieuwenhuis (Deduction and Decision Procedures, 2007)

Bringing Hardware and Software Closer Together with Termination Analysis. - Byron Cook (MEMOCODE, 2007)

Proving thread termination. - Byron Cook; Andreas Podelski; Andrey Rybalchenko (PLDI, 2007)

Thread-modular shape analysis. - Alexey Gotsman; Josh Berdine; Byron Cook; Mooly Sagiv (PLDI, 2007)

Variance analyses from invariance analyses. - Josh Berdine; Aziem Chawdhary; Byron Cook; Dino Distefano; Peter W. O'Hearn (POPL, 2007)

Proving that programs eventually do something good. - Byron Cook; Alexey Gotsman; Andreas Podelski; Andrey Rybalchenko; Moshe Y. Vardi (POPL, 2007)

Arithmetic Strengthening for Shape Analysis. - Stephen Magill; Josh Berdine; Edmund M. Clarke; Byron Cook (SAS, 2007)

Proving Termination by Divergence. - Domagoj Babic; Alan J. Hu; Zvonimir Rakamaric; Byron Cook (SEFM, 2007)

Automatically Proving Concurrent Programs Correct. - Byron Cook (SEFM, 2007)

Shape Analysis by Graph Decomposition. - Roman Manevich; Josh Berdine; Byron Cook; G. Ramalingam; Mooly Sagiv (TACAS, 2007)

Preface to Special Issue on Satisfiability Modulo Theories. - Byron Cook; Roberto Sebastiani (J. Satisf. Boolean Model. Comput., 2007)

Predicate Abstraction via Symbolic Decision Procedures. - Shuvendu K. Lahiri; Thomas Ball 001; Byron Cook (Log. Methods Comput. Sci., 2007)

Verification of Boolean programs with unbounded thread creation. - Byron Cook; Daniel Kroening; Natasha Sharygina (Theor. Comput. Sci., 2007)

Proving Conditional Termination. - Byron Cook; Sumit Gulwani; Tal Lev-Ami; Andrey Rybalchenko; Mooly Sagiv (CAV, 2008)

Scalable Shape Analysis for Systems Code. - Hongseok Yang; Oukseh Lee; Josh Berdine; Cristiano Calcagno; Byron Cook; Dino Distefano; Peter W. O'Hearn (CAV, 2008)

Ranking Abstractions. - Aziem Chawdhary; Byron Cook; Sumit Gulwani; Mooly Sagiv; Hongseok Yang (ESOP, 2008)

Software engineering and formal methods. - Mike Hinchey; Michael Jackson 001; Patrick Cousot; Byron Cook; Jonathan P. Bowen; Tiziana Margaria (Commun. ACM, 2008)

Finding heap-bounds for hardware synthesis. - Byron Cook; Ashutosh Gupta 001; Stephen Magill; Andrey Rybalchenko; Jirí Simsa; Satnam Singh; Viktor Vafeiadis (FMCAD, 2009)

Taming the Unbounded for Hardware Synthesis. - Byron Cook (IFM, 2009)

Proving that non-blocking algorithms don't block. - Alexey Gotsman; Byron Cook; Matthew J. Parkinson; Viktor Vafeiadis (POPL, 2009)

Advances in Program Termination and Liveness. - Byron Cook (VMCAI, 2009)

Summarization for termination: no return! - Byron Cook; Andreas Podelski; Andrey Rybalchenko (Formal Methods Syst. Des., 2009)

Advances in Proving Program Termination and Liveness. - Byron Cook (CADE, 2011)

SLAyer: Memory Safety for Systems-Level Code. - Josh Berdine; Byron Cook; Samin Ishtiaq (CAV, 2011)

Temporal Property Verification as a Program Analysis Task. - Byron Cook; Eric Koskinen; Moshe Y. Vardi (CAV, 2011)

Tractable Reasoning in a Fragment of Separation Logic. - Byron Cook; Christoph Haase; Joël Ouaknine; Matthew J. Parkinson; James Worrell 001 (CONCUR, 2011)

Making prophecies with decision predicates. - Byron Cook; Eric Koskinen (POPL, 2011)

Proving Stabilization of Biological Systems. - Byron Cook; Jasmin Fisher; Elzbieta Krepska; Nir Piterman (VMCAI, 2011)

Proving program termination. - Byron Cook; Andreas Podelski; Andrey Rybalchenko (Commun. ACM, 2011)

Precision and the Conjunction Rule in Concurrent Separation Logic. - Alexey Gotsman; Josh Berdine; Byron Cook (MFPS, 2011)

Bma: Visual Tool for Modeling and Analyzing Biological Networks. - David Benqué; Sam Bourton; Caitlin Cockerton; Byron Cook; Jasmin Fisher; Samin Ishtiaq; Nir Piterman; Alex S. Taylor; Moshe Y. Vardi (CAV, 2012)

Temporal property verification as a program analysis task - Extended Version. - Byron Cook; Eric Koskinen; Moshe Y. Vardi (Formal Methods Syst. Des., 2012)

Better Termination Proving through Cooperation. - Marc Brockschmidt; Byron Cook; Carsten Fuhs (CAV, 2013)

At the interface of biology and computation. - Alex S. Taylor; Nir Piterman; Samin Ishtiaq; Jasmin Fisher; Byron Cook; Caitlin Cockerton; Sam Bourton; David Benqué (CHI, 2013)

Reasoning about nondeterminism in programs. - Byron Cook; Eric Koskinen (PLDI, 2013)

Ramsey vs. Lexicographic Termination Proving. - Byron Cook; Abigail See; Florian Zuleger (TACAS, 2013)

Proving termination of nonlinear command sequences. - Domagoj Babic; Byron Cook; Alan J. Hu; Zvonimir Rakamaric (Formal Aspects Comput., 2013)

Ranking function synthesis for bit-vector relations. - Byron Cook; Daniel Kroening; Philipp Rümmer; Christoph M. Wintersteiger (Formal Methods Syst. Des., 2013)

Finding Instability in Biological Models. - Byron Cook; Jasmin Fisher; Benjamin A. Hall; Samin Ishtiaq; Garvit Juniwal; Nir Piterman (CAV, 2014)

Disproving termination with overapproximation. - Byron Cook; Carsten Fuhs; Kaustubh Nimkar; Peter W. O'Hearn (FMCAD, 2014)

Faster temporal reasoning for infinite-state programs. - Byron Cook; Heidy Khlaaf; Nir Piterman (FMCAD, 2014)

Proving Nontermination via Safety. - Hong Yi Chen; Byron Cook; Carsten Fuhs; Kaustubh Nimkar; Peter W. O'Hearn (TACAS, 2014)

On Automation of CTL* Verification for Infinite-State Systems. - Byron Cook; Heidy Khlaaf; Nir Piterman (CAV (1), 2015)

Spatial Interpolants. - Aws Albarghouthi; Josh Berdine; Byron Cook; Zachary Kincaid (ESOP, 2015)

Fairness for Infinite-State Systems. - Byron Cook; Heidy Khlaaf; Nir Piterman (TACAS, 2015)

Embracing Overapproximation for Proving Nontermination. - Byron Cook; Carsten Fuhs; Kaustubh Nimkar; Peter W. O'Hearn (Adv. Math. Commun., 2015)

T2: Temporal Property Verification. - Marc Brockschmidt; Byron Cook; Samin Ishtiaq; Heidy Khlaaf; Nir Piterman (TACAS, 2016)

Automated formal reasoning about AWS systems. - Byron Cook (FMCAD, 2017)

Automated formal reasoning about amazon web services (keynote). - Byron Cook (SPIN, 2017)

Verifying Increasingly Expressive Temporal Logics for Infinite-State Systems. - Byron Cook; Heidy Khlaaf; Nir Piterman (J. ACM, 2017)

Continuous Formal Verification of Amazon s2n. - Andrey Chudnov; Nathan Collins; Byron Cook; Joey Dodds; Brian Huffman; Colm MacCárthaigh; Stephen Magill; Eric Mertens; Eric Mullen; Serdar Tasiran; Aaron Tomb; Eddy Westbrook (CAV (2), 2018)

Formal Reasoning About the Security of Amazon Web Services. - Byron Cook (CAV (1), 2018)

Semantic-based Automated Reasoning for AWS Access Policies using SMT. - John Backes; Pauline Bolignano; Byron Cook; Catherine Dodge; Andrew Gacek; Kasper Søe Luckow; Neha Rungta; Oksana Tkachuk; Carsten Varming (FMCAD, 2018)

SideTrail: Verifying Time-Balancing of Cryptosystems. - Konstantinos Athanasiou; Byron Cook; Michael Emmi; Colm MacCárthaigh; Daniel Schwartz-Narbonne; Serdar Tasiran (VSTTE, 2018)

Reachability Analysis for AWS-Based Networks. - John Backes; Sam Bayless; Byron Cook; Catherine Dodge; Andrew Gacek; Alan J. Hu; Temesghen Kahsai; Bill Kocik; Evgenii Kotelnikov; Jure Kukovec; Sean McLaughlin; Jason Reed 004; et al. (CAV (2), 2019)

One-Click Formal Methods. - John Backes; Pauline Bolignano; Byron Cook; Andrew Gacek; Kasper Søe Luckow; Neha Rungta; Martin Schäf; Cole Schlesinger; Rima Tanash; Carsten Varming; Michael W. Whalen (IEEE Softw., 2019)

Stratified Abstraction of Access Control Policies. - John Backes; Ulises Berrueco; Tyler Bray; Daniel Brim; Byron Cook; Andrew Gacek; Ranjit Jhala; Kasper Søe Luckow; Sean McLaughlin; Madhav Menon; Daniel Peebles; Ujjwal Pugalia; et al. (CAV (1), 2020)

Using model checking tools to triage the severity of security bugs in the Xen hypervisor. - Byron Cook; Björn Döbel; Daniel Kroening; Norbert Manthey; Martin Pohlack; Elizabeth Polgreen; Michael Tautschnig; Pawel Wieczorkiewicz (FMCAD, 2020)

Code-level model checking in the software development workflow. - Nathan Chong; Byron Cook; Konstantinos Kallas; Kareem Khazem; Felipe R. Monteiro; Daniel Schwartz-Narbonne; Serdar Tasiran; Michael Tautschnig; Mark R. Tuttle (ICSE (SEIP), 2020)

Block public access: trust safety verification of access control policies. - Malik Bouchet; Byron Cook; Bryant Cutler; Anna Druzkina; Andrew Gacek; Liana Hadarean; Ranjit Jhala; Brad Marshall; Daniel Peebles; Neha Rungta; Cole Schlesinger; Chriss Stephens; et al. (ESEC/SIGSOFT FSE, 2020)

Model checking boot code from AWS data centers. - Byron Cook; Kareem Khazem; Daniel Kroening; Serdar Tasiran; Michael Tautschnig; Mark R. Tuttle (Formal Methods Syst. Des., 2021)

Code-level model checking in the software development workflow at Amazon Web Services. - Nathan Chong; Byron Cook; Jonathan Eidelman; Konstantinos Kallas; Kareem Khazem; Felipe R. Monteiro; Daniel Schwartz-Narbonne; Serdar Tasiran; Michael Tautschnig; Mark R. Tuttle (Softw. Pract. Exp., 2021)

Partitioning Strategies for Distributed SMT Solving. - Amalee Wilson; Andres Nötzli; Andrew Reynolds 001; Byron Cook; Cesare Tinelli; Clark W. Barrett (FMCAD, 2023)

Generating and Exploiting Automated Reasoning Proof Certificates. - Haniel Barbosa; Clark W. Barrett; Byron Cook; Bruno Dutertre; Gereon Kremer; Hanna Lachnitt; Aina Niemetz; Andres Nötzli; Alex Ozdemir; Mathias Preiner; Andrew Reynolds 001; Cesare Tinelli; et al. (Commun. ACM, 2023)

SMT-D: New Strategies for Portfolio-Based SMT Solving. - Clark W. Barrett; Pei-Wei Chen; Byron Cook; Bruno Dutertre; Robert B. Jones; Nham Le; Andrew Reynolds 001; Kunal Sheth; Christopher Stephens; Michael W. Whalen (FMCAD, 2024)