Byron Cook
Publication record assembled from the DBLP archive of ranked conferences.
Papers indexed
72
Venues
21
Active years
1997–2026
Best venue rank
A*
Where they publish
Papers
72 indexed papers, newest first.
| Year | Venue | Title | Authors |
|---|---|---|---|
| 2026 | CAV | A Neurosymbolic Approach to Natural Language Formalization and Verification. | Chenyang An, Sam Bayless, Stefano Buliani, Darion Cassel, Byron Cook, Duncan Clough, Rmi Delmas, Nafi Diallo, Ferhat Erata, Nick Feng, Dimitra Giannakopoulou, Aman Goel, Aditya Gokhale, Joe Hendrix, Victor Heorhiadi, Marc Hudak, Dejan Jovanovic, Andrew M. Kent, Benjamin Kiesl-Reiter, Jeffrey J. Kuna, Nadia Labai, Joseph Lilien, Divya Raghunathan, Zvonimir Rakamaric, Niloofar Razavi, Michael Tautschnig, Ali Torkamani, Nathaniel Weir, Michael W. Whalen, Jianan Yao |
| 2024 | FMCAD | 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, Kunal Sheth, Christopher Stephens, Michael W. Whalen |
| 2023 | FMCAD | Partitioning Strategies for Distributed SMT Solving. | Amalee Wilson, Andres Ntzli, Andrew Reynolds, Byron Cook, Cesare Tinelli, Clark W. Barrett |
| 2020 | CAV | Stratified Abstraction of Access Control Policies. | John Backes, Ulises Berrueco, Tyler Bray, Daniel Brim, Byron Cook, Andrew Gacek, Ranjit Jhala, Kasper Se Luckow, Sean McLaughlin, Madhav Menon, Daniel Peebles, Ujjwal Pugalia, Neha Rungta, Cole Schlesinger, Adam Schodde, Anvesh Tanuku, Carsten Varming, Deepa Viswanathan |
| 2020 | FMCAD | Using model checking tools to triage the severity of security bugs in the Xen hypervisor. | Byron Cook, Bjrn Dbel, Daniel Kroening, Norbert Manthey, Martin Pohlack, Elizabeth Polgreen, Michael Tautschnig, Pawel Wieczorkiewicz |
| 2020 | ICSE | 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 |
| 2019 | CAV | 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 |
| 2018 | CAV | Continuous Formal Verification of Amazon s2n. | Andrey Chudnov, Nathan Collins, Byron Cook, Joey Dodds, Brian Huffman, Colm MacCrthaigh, Stephen Magill, Eric Mertens, Eric Mullen, Serdar Tasiran, Aaron Tomb, Eddy Westbrook |
| 2018 | CAV | Formal Reasoning About the Security of Amazon Web Services. | Byron Cook |
| 2018 | CAV | Model Checking Boot Code from AWS Data Centers. | Byron Cook, Kareem Khazem, Daniel Kroening, Serdar Tasiran, Michael Tautschnig, Mark R. Tuttle |
| 2018 | FMCAD | Semantic-based Automated Reasoning for AWS Access Policies using SMT. | John Backes, Pauline Bolignano, Byron Cook, Catherine Dodge, Andrew Gacek, Kasper Se Luckow, Neha Rungta, Oksana Tkachuk, Carsten Varming |
| 2017 | FMCAD | Automated formal reasoning about AWS systems. | Byron Cook |
| 2016 | TACAS | T2: Temporal Property Verification. | Marc Brockschmidt, Byron Cook, Samin Ishtiaq, Heidy Khlaaf, Nir Piterman |
| 2015 | CAV | On Automation of CTL* Verification for Infinite-State Systems. | Byron Cook, Heidy Khlaaf, Nir Piterman |
| 2015 | ESOP | Spatial Interpolants. | Aws Albarghouthi, Josh Berdine, Byron Cook, Zachary Kincaid |
| 2015 | TACAS | Fairness for Infinite-State Systems. | Byron Cook, Heidy Khlaaf, Nir Piterman |
| 2014 | CAV | Finding Instability in Biological Models. | Byron Cook, Jasmin Fisher, Benjamin A. Hall, Samin Ishtiaq, Garvit Juniwal, Nir Piterman |
| 2014 | FMCAD | Disproving termination with overapproximation. | Byron Cook, Carsten Fuhs, Kaustubh Nimkar, Peter W. O'Hearn |
| 2014 | FMCAD | Faster temporal reasoning for infinite-state programs. | Byron Cook, Heidy Khlaaf, Nir Piterman |
| 2014 | TACAS | Proving Nontermination via Safety. | Hong Yi Chen, Byron Cook, Carsten Fuhs, Kaustubh Nimkar, Peter W. O'Hearn |
| 2013 | CAV | Better Termination Proving through Cooperation. | Marc Brockschmidt, Byron Cook, Carsten Fuhs |
| 2013 | CHI | At the interface of biology and computation. | Alex S. Taylor, Nir Piterman, Samin Ishtiaq, Jasmin Fisher, Byron Cook, Caitlin Cockerton, Sam Bourton, David Benqu |
| 2013 | PLDI | Reasoning about nondeterminism in programs. | Byron Cook, Eric Koskinen |
| 2013 | TACAS | Ramsey vs. Lexicographic Termination Proving. | Byron Cook, Abigail See, Florian Zuleger |
| 2012 | CAV | 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 |
| 2011 | CADE | Advances in Proving Program Termination and Liveness. | Byron Cook |
| 2011 | CAV | SLAyer: Memory Safety for Systems-Level Code. | Josh Berdine, Byron Cook, Samin Ishtiaq |
| 2011 | CAV | Temporal Property Verification as a Program Analysis Task. | Byron Cook, Eric Koskinen, Moshe Y. Vardi |
| 2011 | CONCUR | Tractable Reasoning in a Fragment of Separation Logic. | Byron Cook, Christoph Haase, Jol Ouaknine, Matthew J. Parkinson, James Worrell |
| 2011 | POPL | Making prophecies with decision predicates. | Byron Cook, Eric Koskinen |
| 2011 | VMCAI | Proving Stabilization of Biological Systems. | Byron Cook, Jasmin Fisher, Elzbieta Krepska, Nir Piterman |
| 2010 | TACAS | Ranking Function Synthesis for Bit-Vector Relations. | Byron Cook, Daniel Kroening, Philipp Rmmer, Christoph M. Wintersteiger |
| 2009 | FMCAD | Finding heap-bounds for hardware synthesis. | Byron Cook, Ashutosh Gupta, Stephen Magill, Andrey Rybalchenko, Jir Simsa, Satnam Singh, Viktor Vafeiadis |
| 2009 | IFM | Taming the Unbounded for Hardware Synthesis. | Byron Cook |
| 2009 | POPL | Proving that non-blocking algorithms don't block. | Alexey Gotsman, Byron Cook, Matthew J. Parkinson, Viktor Vafeiadis |
| 2009 | VMCAI | Advances in Program Termination and Liveness. | Byron Cook |
| 2008 | CAV | Proving Conditional Termination. | Byron Cook, Sumit Gulwani, Tal Lev-Ami, Andrey Rybalchenko, Mooly Sagiv |
| 2008 | CAV | Scalable Shape Analysis for Systems Code. | Hongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn |
| 2008 | ESOP | Ranking Abstractions. | Aziem Chawdhary, Byron Cook, Sumit Gulwani, Mooly Sagiv, Hongseok Yang |
| 2007 | APLAS | Local Reasoning for Storable Locks and Threads. | Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky, Mooly Sagiv |
| 2007 | CAV | Shape Analysis for Composite Data Structures. | Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn, Thomas Wies, Hongseok Yang |
| 2007 | CAV | Automatically Proving Program Termination. | Byron Cook |
| 2007 | MEMOCODE | Bringing Hardware and Software Closer Together with Termination Analysis. | Byron Cook |
| 2007 | PLDI | Proving thread termination. | Byron Cook, Andreas Podelski, Andrey Rybalchenko |
| 2007 | PLDI | Thread-modular shape analysis. | Alexey Gotsman, Josh Berdine, Byron Cook, Mooly Sagiv |
| 2007 | POPL | Variance analyses from invariance analyses. | Josh Berdine, Aziem Chawdhary, Byron Cook, Dino Distefano, Peter W. O'Hearn |
| 2007 | POPL | Proving that programs eventually do something good. | Byron Cook, Alexey Gotsman, Andreas Podelski, Andrey Rybalchenko, Moshe Y. Vardi |
| 2007 | SAS | Arithmetic Strengthening for Shape Analysis. | Stephen Magill, Josh Berdine, Edmund M. Clarke, Byron Cook |
| 2007 | SEFM | Proving Termination by Divergence. | Domagoj Babic, Alan J. Hu, Zvonimir Rakamaric, Byron Cook |
| 2007 | SEFM | Automatically Proving Concurrent Programs Correct. | Byron Cook |
| 2007 | TACAS | Shape Analysis by Graph Decomposition. | Roman Manevich, Josh Berdine, Byron Cook, G. Ramalingam, Mooly Sagiv |
| 2006 | CAV | Automatic Termination Proofs for Programs with Shape-Shifting Heaps. | Josh Berdine, Byron Cook, Dino Distefano, Peter W. O'Hearn |
| 2006 | CAV | Terminator: Beyond Safety. | Byron Cook, Andreas Podelski, Andrey Rybalchenko |
| 2006 | CAV | Repair of Boolean Programs with an Application to C. | Andreas Griesmayer, Roderick Bloem, Byron Cook |
| 2006 | EuroSys | 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 |
| 2006 | FMCAD | Over-Approximating Boolean Programs with Unbounded Thread Creation. | Byron Cook, Daniel Kroening, Natasha Sharygina |
| 2006 | PLDI | Termination proofs for systems code. | Byron Cook, Andreas Podelski, Andrey Rybalchenko |
| 2006 | SAS | Interprocedural Shape Analysis with Separated Heap Abstractions. | Alexey Gotsman, Josh Berdine, Byron Cook |
| 2005 | CAV | Cogent: Accurate Theorem Proving for Program Verification. | Byron Cook, Daniel Kroening, Natasha Sharygina |
| 2005 | CAV | Predicate Abstraction via Symbolic Decision Procedures. | Shuvendu K. Lahiri, Thomas Ball, Byron Cook |
| 2005 | ICFEM | Using Stlmarck's Algorithm to Prove Inequalities. | Byron Cook, Georges Gonthier |
| 2005 | SAS | Abstraction Refinement for Termination. | Byron Cook, Andreas Podelski, Andrey Rybalchenko |
| 2004 | CAV | Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement. | Thomas Ball, Byron Cook, Shuvendu K. Lahiri, Lintao Zhang |
| 2004 | IFM | SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft. | Thomas Ball, Byron Cook, Vladimir Levin, Sriram K. Rajamani |
| 2004 | ISoLA | Finding API usage rule violations in Windows device drivers using Static Driver Verifier. | Byron Cook |
| 2004 | ISoLA | Accurate Theorem Proving for Program Verification. | Byron Cook, Daniel Kroening, Natasha Sharygina |
| 2004 | TACAS | Refining Approximations in Software Predicate Abstraction. | Thomas Ball, Byron Cook, Satyaki Das, Sriram K. Rajamani |
| 2003 | CAV | A Symbolic Approach to Predicate Abstraction. | Shuvendu K. Lahiri, Randal E. Bryant, Byron Cook |
| 2002 | DAC | A proof engine approach to solving combinational design automation problems. | Gunnar Andersson, Per Bjesse, Byron Cook, Ziyad Hanna |
| 2000 | FMCAD | Combining Stream-Based and State-Based Verification Techniques. | Nancy A. Day, Mark D. Aagaard, Byron Cook |
| 1999 | ICFP | On Embedding a Microarchitectural Design Language within Haskell. | John Launchbury, Jeffrey R. Lewis, Byron Cook |
| 1997 | ICFP | Disposable Memo Functions (Extended Abstract). | Byron Cook, John Launchbury |