Byron Cook

According to our database, Byron Cook authored at least 99 papers between 1997 and 2023.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of three.

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, Cesare Tinelli, Yoni Zohar

Commun. ACM, October, 2023

Partitioning Strategies for Distributed SMT Solving.

Amalee Wilson, Andres Nötzli, Andrew Reynolds, Byron Cook, Cesare Tinelli, Clark W. Barrett

Proceedings of the Formal Methods in Computer-Aided Design, 2023

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

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

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, Carsten Varming, Andy Warfield

Proceedings of the ESEC/FSE '20: 28th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 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

Proceedings of the ICSE-SEIP 2020: 42nd International Conference on Software Engineering, Software Engineering in Practice, Seoul, South Korea, 27 June, 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

Proceedings of the 2020 Formal Methods in Computer Aided Design, 2020

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, Neha Rungta, Cole Schlesinger, Adam Schodde, Anvesh Tanuku, Carsten Varming, Deepa Viswanathan

Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

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

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, Neha Rungta, John Sizemore, Mark A. Stalzer, Preethi Srinivasan, Pavle Subotic, Carsten Varming, Blake Whaley

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

2018

SideTrail: Verifying Time-Balancing of Cryptosystems.

Konstantinos Athanasiou, Byron Cook, Michael Emmi, Colm MacCárthaigh, Daniel Schwartz-Narbonne, Serdar Tasiran

Proceedings of the Verified Software. Theories, Tools, and Experiments, 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

Proceedings of the 2018 Formal Methods in Computer Aided Design, 2018

Formal Reasoning About the Security of Amazon Web Services.

Byron Cook

Proceedings of the Computer Aided Verification - 30th International Conference, 2018

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

Proceedings of the Computer Aided Verification - 30th International Conference, 2018

2017

Verifying Increasingly Expressive Temporal Logics for Infinite-State Systems.

Byron Cook, Heidy Khlaaf, Nir Piterman

J. ACM, 2017

Automated formal reasoning about amazon web services (keynote).

Byron Cook

Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, 2017

Automated formal reasoning about AWS systems.

Byron Cook

Proceedings of the 2017 Formal Methods in Computer Aided Design, 2017

2016

T2: Temporal Property Verification.

Marc Brockschmidt, Byron Cook, Samin Ishtiaq, Heidy Khlaaf, Nir Piterman

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2016

2015

Embracing Overapproximation for Proving Nontermination.

Byron Cook, Carsten Fuhs, Kaustubh Nimkar, Peter W. O'Hearn

Tiny Trans. Comput. Sci., 2015

Fairness for Infinite-State Systems.

Byron Cook, Heidy Khlaaf, Nir Piterman

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2015

Spatial Interpolants.

Aws Albarghouthi, Josh Berdine, Byron Cook, Zachary Kincaid

Proceedings of the Programming Languages and Systems, 2015

On Automation of CTL* Verification for Infinite-State Systems.

Byron Cook, Heidy Khlaaf, Nir Piterman

Proceedings of the Computer Aided Verification - 27th International Conference, 2015

2014

Proving Nontermination via Safety.

Hong Yi Chen, Byron Cook, Carsten Fuhs, Kaustubh Nimkar, Peter W. O'Hearn

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2014

Faster temporal reasoning for infinite-state programs.

Byron Cook, Heidy Khlaaf, Nir Piterman

Proceedings of the Formal Methods in Computer-Aided Design, 2014

Disproving termination with overapproximation.

Byron Cook, Carsten Fuhs, Kaustubh Nimkar, Peter W. O'Hearn

Proceedings of the Formal Methods in Computer-Aided Design, 2014

Finding Instability in Biological Models.

Byron Cook, Jasmin Fisher, Benjamin A. Hall, Samin Ishtiaq, Garvit Juniwal, Nir Piterman

Proceedings of the Computer Aided Verification - 26th International Conference, 2014

2013

Ranking function synthesis for bit-vector relations.

Byron Cook, Daniel Kroening, Philipp Rümmer, Christoph M. Wintersteiger

Formal Methods Syst. Des., 2013

Proving termination of nonlinear command sequences.

Domagoj Babic, Byron Cook, Alan J. Hu, Zvonimir Rakamaric

Formal Aspects Comput., 2013

Ramsey vs. Lexicographic Termination Proving.

Byron Cook, Abigail See, Florian Zuleger

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2013

Reasoning about nondeterminism in programs.

Byron Cook, Eric Koskinen

Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 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é

Proceedings of the 2013 ACM SIGCHI Conference on Human Factors in Computing Systems, 2013

Better Termination Proving through Cooperation.

Marc Brockschmidt, Byron Cook, Carsten Fuhs

Proceedings of the Computer Aided Verification - 25th International Conference, 2013

2012

Temporal property verification as a program analysis task - Extended Version.

Byron Cook, Eric Koskinen, Moshe Y. Vardi

Formal Methods Syst. Des., 2012

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

Proceedings of the Computer Aided Verification - 24th International Conference, 2012

2011

Precision and the Conjunction Rule in Concurrent Separation Logic.

Alexey Gotsman, Josh Berdine, Byron Cook

Proceedings of the Twenty-seventh Conference on the Mathematical Foundations of Programming Semantics, 2011

Proving program termination.

Byron Cook, Andreas Podelski, Andrey Rybalchenko

Commun. ACM, 2011

Proving Stabilization of Biological Systems.

Byron Cook, Jasmin Fisher, Elzbieta Krepska, Nir Piterman

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2011

Making prophecies with decision predicates.

Byron Cook, Eric Koskinen

Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2011

Tractable Reasoning in a Fragment of Separation Logic.

Byron Cook, Christoph Haase, Joël Ouaknine, Matthew J. Parkinson, James Worrell

Proceedings of the CONCUR 2011 - Concurrency Theory - 22nd International Conference, 2011

Temporal Property Verification as a Program Analysis Task.

Byron Cook, Eric Koskinen, Moshe Y. Vardi

Proceedings of the Computer Aided Verification - 23rd International Conference, 2011

SLAyer: Memory Safety for Systems-Level Code.

Josh Berdine, Byron Cook, Samin Ishtiaq

Proceedings of the Computer Aided Verification - 23rd International Conference, 2011

Advances in Proving Program Termination and Liveness.

Byron Cook

Proceedings of the Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31, 2011

2009

Summarization for termination: no return!

Byron Cook, Andreas Podelski, Andrey Rybalchenko

Formal Methods Syst. Des., 2009

Advances in Program Termination and Liveness.

Byron Cook

Proceedings of the Verification, 2009

Proving that non-blocking algorithms don't block.

Alexey Gotsman, Byron Cook, Matthew J. Parkinson, Viktor Vafeiadis

Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2009

Taming the Unbounded for Hardware Synthesis.

Byron Cook

Proceedings of the Integrated Formal Methods, 7th International Conference, 2009

Finding heap-bounds for hardware synthesis.

Byron Cook, Ashutosh Gupta, Stephen Magill, Andrey Rybalchenko, Jirí Simsa, Satnam Singh, Viktor Vafeiadis

Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, 2009

2008

Software engineering and formal methods.

Mike Hinchey, Michael Jackson, Patrick Cousot, Byron Cook, Jonathan P. Bowen, Tiziana Margaria

Commun. ACM, 2008

Ranking Abstractions.

Aziem Chawdhary, Byron Cook, Sumit Gulwani, Mooly Sagiv, Hongseok Yang

Proceedings of the Programming Languages and Systems, 2008

Scalable Shape Analysis for Systems Code.

Hongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn

Proceedings of the Computer Aided Verification, 20th International Conference, 2008

Proving Conditional Termination.

Byron Cook, Sumit Gulwani, Tal Lev-Ami, Andrey Rybalchenko, Mooly Sagiv

Proceedings of the Computer Aided Verification, 20th International Conference, 2008

2007

Verification of Boolean programs with unbounded thread creation.

Byron Cook, Daniel Kroening, Natasha Sharygina

Theor. Comput. Sci., 2007

Predicate Abstraction via Symbolic Decision Procedures.

Shuvendu K. Lahiri, Thomas Ball, Byron Cook

Log. Methods Comput. Sci., 2007

Preface to Special Issue on Satisfiability Modulo Theories.

Byron Cook, Roberto Sebastiani

J. Satisf. Boolean Model. Comput., 2007

Shape Analysis by Graph Decomposition.

Roman Manevich, Josh Berdine, Byron Cook, G. Ramalingam, Mooly Sagiv

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

Automatically Proving Concurrent Programs Correct.

Byron Cook

Proceedings of the Fifth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007), 2007

Proving Termination by Divergence.

Domagoj Babic, Alan J. Hu, Zvonimir Rakamaric, Byron Cook

Proceedings of the Fifth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007), 2007

Arithmetic Strengthening for Shape Analysis.

Stephen Magill, Josh Berdine, Edmund M. Clarke, Byron Cook

Proceedings of the Static Analysis, 14th International Symposium, 2007

Proving that programs eventually do something good.

Byron Cook, Alexey Gotsman, Andreas Podelski, Andrey Rybalchenko, Moshe Y. Vardi

Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2007

Variance analyses from invariance analyses.

Josh Berdine, Aziem Chawdhary, Byron Cook, Dino Distefano, Peter W. O'Hearn

Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2007

Thread-modular shape analysis.

Alexey Gotsman, Josh Berdine, Byron Cook, Mooly Sagiv

Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, 2007

Proving thread termination.

Byron Cook, Andreas Podelski, Andrey Rybalchenko

Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, 2007

Bringing Hardware and Software Closer Together with Termination Analysis.

Byron Cook

Proceedings of the 5th ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2007), May 30, 2007

07401 Abstracts Collection -- Deduction and Decision Procedures.

Franz Baader, Byron Cook, Jürgen Giesl, Robert Nieuwenhuis

Proceedings of the Deduction and Decision Procedures, 30.09. - 05.10.2007, 2007

07401 Executive Summary -- Deduction and Decision Procedures.

Franz Baader, Byron Cook, Jürgen Giesl, Robert Nieuwenhuis

Proceedings of the Deduction and Decision Procedures, 30.09. - 05.10.2007, 2007

Automatically Proving Program Termination.

Byron Cook

Proceedings of the Computer Aided Verification, 19th International Conference, 2007

Shape Analysis for Composite Data Structures.

Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn, Thomas Wies, Hongseok Yang

Proceedings of the Computer Aided Verification, 19th International Conference, 2007

Local Reasoning for Storable Locks and Threads.

Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky, Mooly Sagiv

Proceedings of the Programming Languages and Systems, 5th Asian Symposium, 2007

2006

Preface and Foreword.

Byron Cook, Roberto Sebastiani

Proceedings of the Combined Proceedings of the Fourth Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR 2006) and the First International Workshop on Probabilistic Automata and Logics (PaUL 2006), 2006

Interprocedural Shape Analysis with Separated Heap Abstractions.

Alexey Gotsman, Josh Berdine, Byron Cook

Proceedings of the Static Analysis, 13th International Symposium, 2006

Termination proofs for systems code.

Byron Cook, Andreas Podelski, Andrey Rybalchenko

Proceedings of the ACM SIGPLAN 2006 Conference on Programming Language Design and Implementation, 2006

Over-Approximating Boolean Programs with Unbounded Thread Creation.

Byron Cook, Daniel Kroening, Natasha Sharygina

Proceedings of the Formal Methods in Computer-Aided Design, 6th International Conference, 2006

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

Proceedings of the 2006 EuroSys Conference, Leuven, Belgium, April 18-21, 2006, 2006

Repair of Boolean Programs with an Application to C.

Andreas Griesmayer, Roderick Bloem, Byron Cook

Proceedings of the Computer Aided Verification, 18th International Conference, 2006

Terminator: Beyond Safety.

Byron Cook, Andreas Podelski, Andrey Rybalchenko

Proceedings of the Computer Aided Verification, 18th International Conference, 2006

Automatic Termination Proofs for Programs with Shape-Shifting Heaps.

Josh Berdine, Byron Cook, Dino Distefano, Peter W. O'Hearn

Proceedings of the Computer Aided Verification, 18th International Conference, 2006

2005

Preface.

Byron Cook, Scott D. Stoller, Willem Visser

Proceedings of the 3rd Workshop on Software Model Checking, 2005

Symbolic Model Checking for Asynchronous Boolean Programs.

Byron Cook, Daniel Kroening, Natasha Sharygina

Proceedings of the Model Checking Software, 2005

Abstraction Refinement for Termination.

Byron Cook, Andreas Podelski, Andrey Rybalchenko

Proceedings of the Static Analysis, 12th International Symposium, 2005

Using Stålmarck's Algorithm to Prove Inequalities.

Byron Cook, Georges Gonthier

Proceedings of the Formal Methods and Software Engineering, 2005

Cogent: Accurate Theorem Proving for Program Verification.

Byron Cook, Daniel Kroening, Natasha Sharygina

Proceedings of the Computer Aided Verification, 17th International Conference, 2005

Finding Bugs in Device Drivers with Static Driver Verifier.

Byron Cook

Proceedings of the 12th International Workshop on Abstract State Machines, 2005

2004

Refining Approximations in Software Predicate Abstraction.

Thomas Ball, Byron Cook, Satyaki Das, Sriram K. Rajamani

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2004

Accurate Theorem Proving for Program Verification.

Byron Cook, Daniel Kroening, Natasha Sharygina

Proceedings of the Leveraging Applications of Formal Methods, 2004

Finding API usage rule violations in Windows device drivers using Static Driver Verifier.

Byron Cook

Proceedings of the International Symposium on Leveraging Applications of Formal Methods, 2004

SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft.

Thomas Ball, Byron Cook, Vladimir Levin, Sriram K. Rajamani

Proceedings of the Integrated Formal Methods, 4th International Conference, 2004

Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement.

Thomas Ball, Byron Cook, Shuvendu K. Lahiri, Lintao Zhang

Proceedings of the Computer Aided Verification, 16th International Conference, 2004

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

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

SoftMC 2003: Workshop on Software Model Checking.

Byron Cook, Scott D. Stoller, Willem Visser

Proceedings of the 2003 Workshop on Software Model Checking, 2003

A Symbolic Approach to Predicate Abstraction.

Shuvendu K. Lahiri, Randal E. Bryant, Byron Cook

Proceedings of the Computer Aided Verification, 15th International Conference, 2003

2002

A proof engine approach to solving combinational design automation problems.

Gunnar Andersson, Per Bjesse, Byron Cook, Ziyad Hanna

Proceedings of the 39th Design Automation Conference, 2002

2001

A Framework for Microprocessor Correctness Statements.

Mark D. Aagaard, Byron Cook, Nancy A. Day, Robert B. Jones

Proceedings of the Correct Hardware Design and Verification Methods, 2001

2000

Combining Stream-Based and State-Based Verification Techniques.

Nancy A. Day, Mark D. Aagaard, Byron Cook

Proceedings of the Formal Methods in Computer-Aided Design, Third International Conference, 2000

1999

On Embedding a Microarchitectural Design Language within Haskell.

John Launchbury, Jeffrey R. Lewis, Byron Cook

Proceedings of the fourth ACM SIGPLAN International Conference on Functional Programming (ICFP '99), 1999

Symbolic Simulation of Microprocessor Models using Type Classes in Haskell.

Nancy A. Day, Jeffrey R. Lewis, Byron Cook

Proceedings of the Correct Hardware Design and Verification Methods, 1999

Formal Verification of Explicitly Parallel Microprocessors.

Byron Cook, John Launchbury, John Matthews, Richard B. Kieburtz

Proceedings of the Correct Hardware Design and Verification Methods, 1999

1998

Microprocessor Specification in Hawk.

John Matthews, Byron Cook, John Launchbury

Proceedings of the 1998 International Conference on Computer Languages, 1998

1997

Disposable Memo Functions (Extended Abstract).

Byron Cook, John Launchbury

Proceedings of the 1997 ACM SIGPLAN International Conference on Functional Programming (ICFP '97), 1997