default search action
Byron Cook
Person information
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2023
- [j16]Haniel Barbosa, Clark W. Barrett
, Byron Cook, Bruno Dutertre, Gereon Kremer, Hanna Lachnitt, Aina Niemetz
Generating and Exploiting Automated Reasoning Proof Certificates. Commun. ACM 66(10): 86-95 (2023) - [c83]Amalee Wilson, Andres Nötzli, Andrew Reynolds, Byron Cook, Cesare Tinelli, Clark W. Barrett:
Partitioning Strategies for Distributed SMT Solving. FMCAD 2023: 199-208 - [i7]Amalee Wilson, Andres Nötzli, Andrew Reynolds, Byron Cook, Cesare Tinelli, Clark W. Barrett:
Partitioning Strategies for Distributed SMT Solving. CoRR abs/2306.05854 (2023) - 2021
- [j15]Byron Cook, Kareem Khazem, Daniel Kroening, Serdar Tasiran, Michael Tautschnig, Mark R. Tuttle:
Model checking boot code from AWS data centers. Formal Methods Syst. Des. 57(1): 34-52 (2021) - [j14]Nathan Chong
Code-level model checking in the software development workflow at Amazon Web Services. Softw. Pract. Exp. 51(4): 772-797 (2021) - 2020
- [c82]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:
Stratified Abstraction of Access Control Policies. CAV (1) 2020: 165-176 - [c81]Byron Cook, Björn Döbel, Daniel Kroening, Norbert Manthey, Martin Pohlack, Elizabeth Polgreen, Michael Tautschnig, Pawel Wieczorkiewicz:
Using model checking tools to triage the severity of security bugs in the Xen hypervisor. FMCAD 2020: 185-193 - [c80]Nathan Chong, Byron Cook, Konstantinos Kallas, Kareem Khazem, Felipe R. Monteiro, Daniel Schwartz-Narbonne, Serdar Tasiran, Michael Tautschnig, Mark R. Tuttle:
Code-level model checking in the software development workflow. ICSE (SEIP) 2020: 11-20 - [c79]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:
Block public access: trust safety verification of access control policies. ESEC/SIGSOFT FSE 2020: 281-291
2010 – 2019
- 2019
- [j13]John Backes, Pauline Bolignano, Byron Cook, Andrew Gacek, Kasper Søe Luckow, Neha Rungta, Martin Schäf
One-Click Formal Methods. IEEE Softw. 36(6): 61-65 (2019) - [c78]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:
Reachability Analysis for AWS-Based Networks. CAV (2) 2019: 231-241 - 2018
- [c77]Byron Cook:
Formal Reasoning About the Security of Amazon Web Services. CAV (1) 2018: 38-47 - [c76]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:
Continuous Formal Verification of Amazon s2n. CAV (2) 2018: 430-446 - [c75]Byron Cook, Kareem Khazem, Daniel Kroening
Model Checking Boot Code from AWS Data Centers. CAV (2) 2018: 467-486 - [c74]John Backes, Pauline Bolignano, Byron Cook, Catherine Dodge, Andrew Gacek, Kasper Søe Luckow, Neha Rungta, Oksana Tkachuk, Carsten Varming:
Semantic-based Automated Reasoning for AWS Access Policies using SMT. FMCAD 2018: 1-9 - [c73]Konstantinos Athanasiou, Byron Cook, Michael Emmi, Colm MacCárthaigh, Daniel Schwartz-Narbonne, Serdar Tasiran:
SideTrail: Verifying Time-Balancing of Cryptosystems. VSTTE 2018: 215-228 - 2017
- [j12]Byron Cook, Heidy Khlaaf, Nir Piterman
Verifying Increasingly Expressive Temporal Logics for Infinite-State Systems. J. ACM 64(2): 15:1-15:39 (2017) - [c72]Byron Cook:
Automated formal reasoning about AWS systems. FMCAD 2017: 7 - [c71]Byron Cook:
Automated formal reasoning about amazon web services (keynote). SPIN 2017: 9 - 2016
- [c70]Marc Brockschmidt, Byron Cook, Samin Ishtiaq, Heidy Khlaaf, Nir Piterman
T2: Temporal Property Verification. TACAS 2016: 387-393 - 2015
- [c69]Byron Cook, Heidy Khlaaf, Nir Piterman
On Automation of CTL* Verification for Infinite-State Systems. CAV (1) 2015: 13-29 - [c68]Aws Albarghouthi, Josh Berdine, Byron Cook, Zachary Kincaid:
Spatial Interpolants. ESOP 2015: 634-660 - [c67]Byron Cook, Heidy Khlaaf, Nir Piterman
Fairness for Infinite-State Systems. TACAS 2015: 384-398 - [i6]Aws Albarghouthi, Josh Berdine, Byron Cook, Zachary Kincaid:
Spatial Interpolants. CoRR abs/1501.04100 (2015) - [i5]Marc Brockschmidt, Byron Cook, Samin Ishtiaq, Heidy Khlaaf, Nir Piterman:
T2: Temporal Property Verification. CoRR abs/1512.08689 (2015) - [i4]Byron Cook, Carsten Fuhs, Kaustubh Nimkar, Peter W. O'Hearn:
Embracing Overapproximation for Proving Nontermination. Tiny Trans. Comput. Sci. 3 (2015) - 2014
- [c66]Byron Cook, Jasmin Fisher
Finding Instability in Biological Models. CAV 2014: 358-372 - [c65]Byron Cook, Carsten Fuhs, Kaustubh Nimkar, Peter W. O'Hearn:
Disproving termination with overapproximation. FMCAD 2014: 67-74 - [c64]Byron Cook, Heidy Khlaaf, Nir Piterman
Faster temporal reasoning for infinite-state programs. FMCAD 2014: 75-82 - [c63]Hong Yi Chen, Byron Cook, Carsten Fuhs, Kaustubh Nimkar, Peter W. O'Hearn:
Proving Nontermination via Safety. TACAS 2014: 156-171 - 2013
- [j11]Domagoj Babic, Byron Cook, Alan J. Hu, Zvonimir Rakamaric:
Proving termination of nonlinear command sequences. Formal Aspects Comput. 25(3): 389-403 (2013) - [j10]Byron Cook, Daniel Kroening
Ranking function synthesis for bit-vector relations. Formal Methods Syst. Des. 43(1): 93-120 (2013) - [c62]Marc Brockschmidt, Byron Cook, Carsten Fuhs:
Better Termination Proving through Cooperation. CAV 2013: 413-429 - [c61]Alex S. Taylor
At the interface of biology and computation. CHI 2013: 493-502 - [c60]Byron Cook, Eric Koskinen:
Reasoning about nondeterminism in programs. PLDI 2013: 219-230 - [c59]Byron Cook, Abigail See, Florian Zuleger:
Ramsey vs. Lexicographic Termination Proving. TACAS 2013: 47-61 - 2012
- [j9]Byron Cook, Eric Koskinen, Moshe Y. Vardi:
Temporal property verification as a program analysis task - Extended Version. Formal Methods Syst. Des. 41(1): 66-82 (2012) - [c58]David Benqué, Sam Bourton, Caitlin Cockerton, Byron Cook, Jasmin Fisher
Bma: Visual Tool for Modeling and Analyzing Biological Networks. CAV 2012: 686-692 - 2011
- [j8]Byron Cook, Andreas Podelski, Andrey Rybalchenko:
Proving program termination. Commun. ACM 54(5): 88-98 (2011) - [c57]Byron Cook:
Advances in Proving Program Termination and Liveness. CADE 2011: 4 - [c56]Josh Berdine, Byron Cook, Samin Ishtiaq:
SLAyer: Memory Safety for Systems-Level Code. CAV 2011: 178-183 - [c55]Byron Cook, Eric Koskinen, Moshe Y. Vardi:
Temporal Property Verification as a Program Analysis Task. CAV 2011: 333-348 - [c54]Byron Cook, Christoph Haase
Tractable Reasoning in a Fragment of Separation Logic. CONCUR 2011: 235-249 - [c53]Byron Cook, Eric Koskinen:
Making prophecies with decision predicates. POPL 2011: 399-410 - [c52]Byron Cook, Jasmin Fisher
Proving Stabilization of Biological Systems. VMCAI 2011: 134-149 - [c51]Alexey Gotsman, Josh Berdine, Byron Cook:
Precision and the Conjunction Rule in Concurrent Separation Logic. MFPS 2011: 171-190 - 2010
- [c50]Byron Cook, Daniel Kroening
Ranking Function Synthesis for Bit-Vector Relations. TACAS 2010: 236-250 - [e6]Tayssir Touili, Byron Cook, Paul B. Jackson
Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings. Lecture Notes in Computer Science 6174, Springer 2010, ISBN 978-3-642-14294-9 [contents]
2000 – 2009
- 2009
- [j7]Byron Cook, Andreas Podelski, Andrey Rybalchenko:
Summarization for termination: no return! Formal Methods Syst. Des. 35(3): 369-387 (2009) - [c49]Byron Cook, Ashutosh Gupta, Stephen Magill, Andrey Rybalchenko, Jirí Simsa, Satnam Singh, Viktor Vafeiadis
Finding heap-bounds for hardware synthesis. FMCAD 2009: 205-212 - [c48]Byron Cook:
Taming the Unbounded for Hardware Synthesis. IFM 2009: 39 - [c47]Alexey Gotsman, Byron Cook, Matthew J. Parkinson, Viktor Vafeiadis
Proving that non-blocking algorithms don't block. POPL 2009: 16-28 - [c46]Byron Cook:
Advances in Program Termination and Liveness. VMCAI 2009: 4 - [e5]María Alpuente
Formal Methods for Industrial Critical Systems, 14th International Workshop, FMICS 2009, Eindhoven, The Netherlands, November 2-3, 2009. Proceedings. Lecture Notes in Computer Science 5825, Springer 2009, ISBN 978-3-642-04569-1 [contents] - 2008
- [j6]Mike Hinchey
Software engineering and formal methods. Commun. ACM 51(9): 54-59 (2008) - [c45]Byron Cook, Sumit Gulwani, Tal Lev-Ami, Andrey Rybalchenko, Mooly Sagiv:
Proving Conditional Termination. CAV 2008: 328-340 - [c44]Hongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn:
Scalable Shape Analysis for Systems Code. CAV 2008: 385-398 - [c43]Aziem Chawdhary, Byron Cook, Sumit Gulwani, Mooly Sagiv, Hongseok Yang:
Ranking Abstractions. ESOP 2008: 148-162 - 2007
- [j5]Byron Cook, Roberto Sebastiani:
Preface to Special Issue on Satisfiability Modulo Theories. J. Satisf. Boolean Model. Comput. 3(1-2) (2007) - [j4]Shuvendu K. Lahiri, Thomas Ball, Byron Cook:
Predicate Abstraction via Symbolic Decision Procedures. Log. Methods Comput. Sci. 3(2) (2007) - [j3]Byron Cook, Daniel Kroening
Verification of Boolean programs with unbounded thread creation. Theor. Comput. Sci. 388(1-3): 227-242 (2007) - [c42]Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky, Mooly Sagiv:
Local Reasoning for Storable Locks and Threads. APLAS 2007: 19-37 - [c41]Byron Cook:
Automatically Proving Program Termination. CAV 2007: 1 - [c40]Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn, Thomas Wies, Hongseok Yang:
Shape Analysis for Composite Data Structures. CAV 2007: 178-192 - [c39]Byron Cook:
Bringing Hardware and Software Closer Together with Termination Analysis. MEMOCODE 2007: 201 - [c38]Alexey Gotsman, Josh Berdine, Byron Cook, Mooly Sagiv:
Thread-modular shape analysis. PLDI 2007: 266-277 - [c37]Byron Cook, Andreas Podelski, Andrey Rybalchenko:
Proving thread termination. PLDI 2007: 320-330 - [c36]Josh Berdine, Aziem Chawdhary, Byron Cook, Dino Distefano, Peter W. O'Hearn:
Variance analyses from invariance analyses. POPL 2007: 211-224 - [c35]Byron Cook, Alexey Gotsman, Andreas Podelski, Andrey Rybalchenko, Moshe Y. Vardi:
Proving that programs eventually do something good. POPL 2007: 265-276 - [c34]Stephen Magill, Josh Berdine, Edmund M. Clarke, Byron Cook:
Arithmetic Strengthening for Shape Analysis. SAS 2007: 419-436 - [c33]Domagoj Babic, Alan J. Hu, Zvonimir Rakamaric, Byron Cook:
Proving Termination by Divergence. SEFM 2007: 93-102 - [c32]Byron Cook:
Automatically Proving Concurrent Programs Correct. SEFM 2007: 269-272 - [c31]Roman Manevich, Josh Berdine, Byron Cook, G. Ramalingam, Mooly Sagiv:
Shape Analysis by Graph Decomposition. TACAS 2007: 3-18 - [e4]Franz Baader, Byron Cook, Jürgen Giesl, Robert Nieuwenhuis
Deduction and Decision Procedures, 30.09. - 05.10.2007. Dagstuhl Seminar Proceedings 07401, Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany 2007 [contents] - [e3]Byron Cook, Andreas Podelski:
Verification, Model Checking, and Abstract Interpretation, 8th International Conference, VMCAI 2007, Nice, France, January 14-16, 2007, Proceedings. Lecture Notes in Computer Science 4349, Springer 2007, ISBN 978-3-540-69735-0 [contents] - [i3]Franz Baader, Byron Cook, Jürgen Giesl, Robert Nieuwenhuis
07401 Executive Summary -- Deduction and Decision Procedures. Deduction and Decision Procedures 2007 - [i2]Franz Baader, Byron Cook, Jürgen Giesl, Robert Nieuwenhuis
07401 Abstracts Collection -- Deduction and Decision Procedures. Deduction and Decision Procedures 2007 - 2006
- [c30]Andreas Griesmayer, Roderick Bloem, Byron Cook:
Repair of Boolean Programs with an Application to C. CAV 2006: 358-371 - [c29]Josh Berdine, Byron Cook, Dino Distefano, Peter W. O'Hearn:
Automatic Termination Proofs for Programs with Shape-Shifting Heaps. CAV 2006: 386-400 - [c28]Byron Cook, Andreas Podelski, Andrey Rybalchenko:
Terminator: Beyond Safety. CAV 2006: 415-418 - [c27]Thomas Ball, Ella Bounimova, Byron Cook, Vladimir Levin, Jakob Lichtenberg, Con McGarvey, Bohus Ondrusek, Sriram K. Rajamani, Abdullah Ustuner:
Thorough static analysis of device drivers. EuroSys 2006: 73-85 - [c26]Byron Cook, Daniel Kroening
Over-Approximating Boolean Programs with Unbounded Thread Creation. FMCAD 2006: 53-59 - [c25]Byron Cook, Andreas Podelski, Andrey Rybalchenko:
Termination proofs for systems code. PLDI 2006: 415-426 - [c24]Alexey Gotsman, Josh Berdine, Byron Cook:
Interprocedural Shape Analysis with Separated Heap Abstractions. SAS 2006: 240-260 - [c23]Byron Cook, Roberto Sebastiani:
Preface and Foreword. PDPAR/PaUL@FLoC 2006: 3-6 - [e2]Byron Cook, Scott D. Stoller, Willem Visser:
Proceedings of the 3rd Workshop on Software Model Checking, SoftMC@CAV 2005, Edinburgh, UK, July 11, 2005. Electronic Notes in Theoretical Computer Science 144(3), Elsevier 2006 [contents] - [i1]Shuvendu K. Lahiri, Thomas Ball, Byron Cook:
Predicate Abstraction via Symbolic Decision Procedures. CoRR abs/cs/0612003 (2006) - 2005
- [c22]Byron Cook:
Finding Bugs in Device Drivers with Static Driver Verifier. Abstract State Machines 2005: 71 - [c21]Shuvendu K. Lahiri, Thomas Ball, Byron Cook:
Predicate Abstraction via Symbolic Decision Procedures. CAV 2005: 24-38 - [c20]Byron Cook, Daniel Kroening, Natasha Sharygina:
Cogent: Accurate Theorem Proving for Program Verification. CAV 2005: 296-300 - [c19]Byron Cook, Georges Gonthier:
Using Stålmarck's Algorithm to Prove Inequalities. ICFEM 2005: 330-344 - [c18]Byron Cook, Andreas Podelski, Andrey Rybalchenko:
Abstraction Refinement for Termination. SAS 2005: 87-101 - [c17]Byron Cook, Daniel Kroening, Natasha Sharygina:
Symbolic Model Checking for Asynchronous Boolean Programs. SPIN 2005: 75-90 - [c16]Byron Cook, Scott D. Stoller, Willem Visser:
Preface. SoftMC@CAV 2005: 1-2 - 2004
- [c15]Thomas Ball, Byron Cook, Shuvendu K. Lahiri, Lintao Zhang:
Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement. CAV 2004: 457-461 - [c14]Thomas Ball, Byron Cook, Vladimir Levin, Sriram K. Rajamani:
SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft. IFM 2004: 1-20 - [c13]Byron Cook:
Finding API usage rule violations in Windows device drivers using Static Driver Verifier. ISoLA (Preliminary proceedings) 2004: 18-18 - [c12]Byron Cook, Daniel Kroening, Natasha Sharygina:
Accurate Theorem Proving for Program Verification. ISoLA 2004: 96-114 - [c11]Thomas Ball, Byron Cook, Satyaki Das, Sriram K. Rajamani:
Refining Approximations in Software Predicate Abstraction. TACAS 2004: 388-403 - 2003
- [j2]Mark D. Aagaard, Byron Cook, Nancy A. Day, Robert B. Jones:
A framework for superscalar microprocessor correctness statements. Int. J. Softw. Tools Technol. Transf. 4(3): 298-312 (2003) - [j1]Gunnar Andersson, Per Bjesse, Byron Cook, Ziyad Hanna:
Design automation with mixtures of proof strategies for propositional logic. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 22(8): 1042-1048 (2003) - [c10]Shuvendu K. Lahiri, Randal E. Bryant, Byron Cook:
A Symbolic Approach to Predicate Abstraction. CAV 2003: 141-153 - [c9]Byron Cook, Scott D. Stoller, Willem Visser:
SoftMC 2003: Workshop on Software Model Checking. SoftMC@CAV 2003: 377 - [e1]Byron Cook, Scott D. Stoller, Willem Visser:
2003 Workshop on Software Model Checking, SoftMC 2003, Boulder, Colorado, USA, July 14, 2003. Electronic Notes in Theoretical Computer Science 89(3), Elsevier 2003 [contents] - 2002
- [c8]Gunnar Andersson, Per Bjesse, Byron Cook, Ziyad Hanna:
A proof engine approach to solving combinational design automation problems. DAC 2002: 725-730 - 2001
- [c7]Mark D. Aagaard, Byron Cook, Nancy A. Day, Robert B. Jones:
A Framework for Microprocessor Correctness Statements. CHARME 2001: 433-448 - 2000
- [c6]Nancy A. Day, Mark D. Aagaard, Byron Cook:
Combining Stream-Based and State-Based Verification Techniques. FMCAD 2000: 126-142
1990 – 1999
- 1999
- [c5]Byron Cook, John Launchbury, John Matthews, Richard B. Kieburtz:
Formal Verification of Explicitly Parallel Microprocessors. CHARME 1999: 23-36 - [c4]Nancy A. Day, Jeffrey R. Lewis, Byron Cook:
Symbolic Simulation of Microprocessor Models using Type Classes in Haskell. CHARME 1999: 346-349 - [c3]John Launchbury, Jeffrey R. Lewis, Byron Cook:
On Embedding a Microarchitectural Design Language within Haskell. ICFP 1999: 60-69 - 1998
- [c2]John Matthews, Byron Cook, John Launchbury:
Microprocessor Specification in Hawk. ICCL 1998: 90-101 - 1997
- [c1]Byron Cook, John Launchbury:
Disposable Memo Functions (Extended Abstract). ICFP 1997: 310
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-10-07 22:24 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: