Byron Cook - RankMe

115 papers A* 27A 13B 23C 4Journal 22Unranked 23

Year	Rank	Type	Title / Venue / Authors
2026	—	`conf`	Reasoning About Hilbert's Choice Operator in SMT. On the Pursuit of Insight and Elegance Byron Cook, Andres Nötzli
2025	J	`jnl`	A Neurosymbolic Approach to Natural Language Formalization and Verification. CoRR Sam Bayless, Stefano Buliani, Darion Cassel, Byron Cook, Duncan Clough, Rémi Delmas, Nafi Diallo, Ferhat Erata, Nick Feng, Dimitra Giannakopoulou, Aman Goel, Aditya Gokhale, Joe Hendrix, 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	B	`conf`	SMT-D: New Strategies for Portfolio-Based SMT Solving. FMCAD 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	J	`jnl`	Generating and Exploiting Automated Reasoning Proof Certificates. Commun. ACM 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
2023	B	`conf`	Partitioning Strategies for Distributed SMT Solving. FMCAD Amalee Wilson, Andres Nötzli, Andrew Reynolds, Byron Cook, Cesare Tinelli, Clark W. Barrett
2023	J	`jnl`	Partitioning Strategies for Distributed SMT Solving. CoRR Amalee Wilson, Andres Nötzli, Andrew Reynolds, Byron Cook, Cesare Tinelli, Clark W. Barrett
2021	J	`jnl`	Code-level model checking in the software development workflow at Amazon Web Services. Softw. Pract. Exp. Nathan Chong, Byron Cook, Jonathan Eidelman, Konstantinos Kallas, Kareem Khazem, Felipe R. Monteiro, Daniel Schwartz-Narbonne, Serdar Tasiran, Michael Tautschnig, Mark R. Tuttle
2021	J	`jnl`	Model checking boot code from AWS data centers. Formal Methods Syst. Des. Byron Cook, Kareem Khazem, Daniel Kroening, Serdar Tasiran, Michael Tautschnig, Mark R. Tuttle
2020	—	`conf`	Block public access: trust safety verification of access control policies. ESEC/SIGSOFT FSE 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
2020	—	`conf`	Code-level model checking in the software development workflow. ICSE (SEIP) Nathan Chong, Byron Cook, Konstantinos Kallas, Kareem Khazem, Felipe R. Monteiro, Daniel Schwartz-Narbonne, Serdar Tasiran, Michael Tautschnig, Mark R. Tuttle
2020	—	`conf`	Stratified Abstraction of Access Control Policies. CAV (1) 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
2020	B	`conf`	Using model checking tools to triage the severity of security bugs in the Xen hypervisor. FMCAD Byron Cook, Björn Döbel, Daniel Kroening, Norbert Manthey, Martin Pohlack, Elizabeth Polgreen, Michael Tautschnig, Pawel Wieczorkiewicz
2019	J	`jnl`	One-Click Formal Methods. IEEE Softw. John Backes, Pauline Bolignano, Byron Cook, Andrew Gacek, Kasper Søe Luckow, Neha Rungta, Martin Schäf, Cole Schlesinger, Rima S. Tanash, Carsten Varming, Michael W. Whalen
2019	—	`conf`	Reachability Analysis for AWS-Based Networks. CAV (2) 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	—	`conf`	Continuous Formal Verification of Amazon s2n. CAV (2) 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
2018	—	`conf`	Formal Reasoning About the Security of Amazon Web Services. CAV (1) Byron Cook
2018	—	`conf`	Model Checking Boot Code from AWS Data Centers. CAV (2) Byron Cook, Kareem Khazem, Daniel Kroening, Serdar Tasiran, Michael Tautschnig, Mark R. Tuttle
2018	B	`conf`	Semantic-based Automated Reasoning for AWS Access Policies using SMT. FMCAD John Backes, Pauline Bolignano, Byron Cook, Catherine Dodge, Andrew Gacek, Kasper Søe Luckow, Neha Rungta, Oksana Tkachuk, Carsten Varming
2018	—	`conf`	SideTrail: Verifying Time-Balancing of Cryptosystems. VSTTE Konstantinos Athanasiou, Byron Cook, Michael Emmi, Colm MacCárthaigh, Daniel Schwartz-Narbonne, Serdar Tasiran
2017	B	`conf`	Automated formal reasoning about AWS systems. FMCAD Byron Cook
2017	—	`conf`	Automated formal reasoning about amazon web services (keynote). SPIN Byron Cook
2017	J	`jnl`	Verifying Increasingly Expressive Temporal Logics for Infinite-State Systems. J. ACM Byron Cook, Heidy Khlaaf, Nir Piterman
2016	A	`conf`	T2: Temporal Property Verification. TACAS Marc Brockschmidt, Byron Cook, Samin Ishtiaq, Heidy Khlaaf, Nir Piterman
2015	J	`jnl`	Embracing Overapproximation for Proving Nontermination. Tiny Trans. Comput. Sci. Byron Cook, Carsten Fuhs, Kaustubh Nimkar, Peter W. O'Hearn
2015	A	`conf`	Fairness for Infinite-State Systems. TACAS Byron Cook, Heidy Khlaaf, Nir Piterman
2015	—	`conf`	On Automation of CTL* Verification for Infinite-State Systems. CAV (1) Byron Cook, Heidy Khlaaf, Nir Piterman
2015	A	`conf`	Spatial Interpolants. ESOP Aws Albarghouthi, Josh Berdine, Byron Cook, Zachary Kincaid
2015	J	`jnl`	Spatial Interpolants. CoRR Aws Albarghouthi, Josh Berdine, Byron Cook, Zachary Kincaid
2015	J	`jnl`	T2: Temporal Property Verification. CoRR Marc Brockschmidt, Byron Cook, Samin Ishtiaq, Heidy Khlaaf, Nir Piterman
2014	B	`conf`	Disproving termination with overapproximation. FMCAD Byron Cook, Carsten Fuhs, Kaustubh Nimkar, Peter W. O'Hearn
2014	B	`conf`	Faster temporal reasoning for infinite-state programs. FMCAD Byron Cook, Heidy Khlaaf, Nir Piterman
2014	A*	`conf`	Finding Instability in Biological Models. CAV Byron Cook, Jasmin Fisher, Benjamin A. Hall, Samin Ishtiaq, Garvit Juniwal, Nir Piterman
2014	A	`conf`	Proving Nontermination via Safety. TACAS Hong Yi Chen, Byron Cook, Carsten Fuhs, Kaustubh Nimkar, Peter W. O'Hearn
2013	A*	`conf`	At the interface of biology and computation. CHI Alex S. Taylor, Nir Piterman, Samin Ishtiaq, Jasmin Fisher, Byron Cook, Caitlin Cockerton, Sam Bourton, David Benqué
2013	A*	`conf`	Better Termination Proving through Cooperation. CAV Marc Brockschmidt, Byron Cook, Carsten Fuhs
2013	J	`jnl`	Proving termination of nonlinear command sequences. Formal Aspects Comput. Domagoj Babic, Byron Cook, Alan J. Hu, Zvonimir Rakamaric
2013	A	`conf`	Ramsey vs. Lexicographic Termination Proving. TACAS Byron Cook, Abigail See, Florian Zuleger
2013	J	`jnl`	Ranking function synthesis for bit-vector relations. Formal Methods Syst. Des. Byron Cook, Daniel Kroening, Philipp Rümmer, Christoph M. Wintersteiger
2013	A*	`conf`	Reasoning about nondeterminism in programs. PLDI Byron Cook, Eric Koskinen
2012	A*	`conf`	Bma: Visual Tool for Modeling and Analyzing Biological Networks. CAV David Benqué, Sam Bourton, Caitlin Cockerton, Byron Cook, Jasmin Fisher, Samin Ishtiaq, Nir Piterman, Alex S. Taylor, Moshe Y. Vardi
2012	J	`jnl`	Temporal property verification as a program analysis task - Extended Version. Formal Methods Syst. Des. Byron Cook, Eric Koskinen, Moshe Y. Vardi
2011	A	`conf`	Advances in Proving Program Termination and Liveness. CADE Byron Cook
2011	A*	`conf`	Making prophecies with decision predicates. POPL Byron Cook, Eric Koskinen
2011	B	`conf`	Precision and the Conjunction Rule in Concurrent Separation Logic. MFPS Alexey Gotsman, Josh Berdine, Byron Cook
2011	B	`conf`	Proving Stabilization of Biological Systems. VMCAI Byron Cook, Jasmin Fisher, Elzbieta Krepska, Nir Piterman
2011	J	`jnl`	Proving program termination. Commun. ACM Byron Cook, Andreas Podelski, Andrey Rybalchenko
2011	A*	`conf`	SLAyer: Memory Safety for Systems-Level Code. CAV Josh Berdine, Byron Cook, Samin Ishtiaq
2011	A*	`conf`	Temporal Property Verification as a Program Analysis Task. CAV Byron Cook, Eric Koskinen, Moshe Y. Vardi
2011	B	`conf`	Tractable Reasoning in a Fragment of Separation Logic. CONCUR Byron Cook, Christoph Haase, Joël Ouaknine, Matthew J. Parkinson, James Worrell
2010	A*	`ed.`	Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings CAV Tayssir Touili, Byron Cook, Paul B. Jackson
2010	A	`conf`	Ranking Function Synthesis for Bit-Vector Relations. TACAS Byron Cook, Daniel Kroening, Philipp Rümmer, Christoph M. Wintersteiger
2009	B	`conf`	Advances in Program Termination and Liveness. VMCAI Byron Cook
2009	B	`conf`	Finding heap-bounds for hardware synthesis. FMCAD Byron Cook, Ashutosh Gupta, Stephen Magill, Andrey Rybalchenko, Jirí Simsa, Satnam Singh, Viktor Vafeiadis
2009	C	`ed.`	Formal Methods for Industrial Critical Systems, 14th International Workshop, FMICS 2009, Eindhoven, The Netherlands, November 2-3, 2009. Proceedings FMICS María Alpuente, Byron Cook, Christophe Joubert
2009	A*	`conf`	Proving that non-blocking algorithms don't block. POPL Alexey Gotsman, Byron Cook, Matthew J. Parkinson, Viktor Vafeiadis
2009	J	`jnl`	Summarization for termination: no return! Formal Methods Syst. Des. Byron Cook, Andreas Podelski, Andrey Rybalchenko
2009	B	`conf`	Taming the Unbounded for Hardware Synthesis. IFM Byron Cook
2008	A*	`conf`	Proving Conditional Termination. CAV Byron Cook, Sumit Gulwani, Tal Lev-Ami, Andrey Rybalchenko, Mooly Sagiv
2008	A	`conf`	Ranking Abstractions. ESOP Aziem Chawdhary, Byron Cook, Sumit Gulwani, Mooly Sagiv, Hongseok Yang
2008	A*	`conf`	Scalable Shape Analysis for Systems Code. CAV Hongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn
2008	J	`jnl`	Software engineering and formal methods. Commun. ACM Mike Hinchey, Michael Jackson, Patrick Cousot, Byron Cook, Jonathan P. Bowen, Tiziana Margaria
2007	—	`conf`	07401 Abstracts Collection -- Deduction and Decision Procedures. Deduction and Decision Procedures Franz Baader, Byron Cook, Jürgen Giesl, Robert Nieuwenhuis
2007	—	`conf`	07401 Executive Summary -- Deduction and Decision Procedures. Deduction and Decision Procedures Franz Baader, Byron Cook, Jürgen Giesl, Robert Nieuwenhuis
2007	B	`conf`	Arithmetic Strengthening for Shape Analysis. SAS Stephen Magill, Josh Berdine, Edmund M. Clarke, Byron Cook
2007	B	`conf`	Automatically Proving Concurrent Programs Correct. SEFM Byron Cook
2007	A*	`conf`	Automatically Proving Program Termination. CAV Byron Cook
2007	C	`conf`	Bringing Hardware and Software Closer Together with Termination Analysis. MEMOCODE Byron Cook
2007	—	`ed.`	Deduction and Decision Procedures, 30.09. - 05.10.2007 Deduction and Decision Procedures Franz Baader, Byron Cook, Jürgen Giesl, Robert Nieuwenhuis
2007	B	`conf`	Local Reasoning for Storable Locks and Threads. APLAS Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky, Mooly Sagiv
2007	J	`jnl`	Predicate Abstraction via Symbolic Decision Procedures. Log. Methods Comput. Sci. Shuvendu K. Lahiri, Thomas Ball, Byron Cook
2007	J	`jnl`	Preface to Special Issue on Satisfiability Modulo Theories. J. Satisf. Boolean Model. Comput. Byron Cook, Roberto Sebastiani
2007	B	`conf`	Proving Termination by Divergence. SEFM Domagoj Babic, Alan J. Hu, Zvonimir Rakamaric, Byron Cook
2007	A*	`conf`	Proving that programs eventually do something good. POPL Byron Cook, Alexey Gotsman, Andreas Podelski, Andrey Rybalchenko, Moshe Y. Vardi
2007	A*	`conf`	Proving thread termination. PLDI Byron Cook, Andreas Podelski, Andrey Rybalchenko
2007	A	`conf`	Shape Analysis by Graph Decomposition. TACAS Roman Manevich, Josh Berdine, Byron Cook, G. Ramalingam, Mooly Sagiv
2007	A*	`conf`	Shape Analysis for Composite Data Structures. CAV Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn, Thomas Wies, Hongseok Yang
2007	A*	`conf`	Thread-modular shape analysis. PLDI Alexey Gotsman, Josh Berdine, Byron Cook, Mooly Sagiv
2007	A*	`conf`	Variance analyses from invariance analyses. POPL Josh Berdine, Aziem Chawdhary, Byron Cook, Dino Distefano, Peter W. O'Hearn
2007	J	`jnl`	Verification of Boolean programs with unbounded thread creation. Theor. Comput. Sci. Byron Cook, Daniel Kroening, Natasha Sharygina
2007	B	`ed.`	Verification, Model Checking, and Abstract Interpretation, 8th International Conference, VMCAI 2007, Nice, France, January 14-16, 2007, Proceedings VMCAI Byron Cook, Andreas Podelski
2006	A*	`conf`	Automatic Termination Proofs for Programs with Shape-Shifting Heaps. CAV Josh Berdine, Byron Cook, Dino Distefano, Peter W. O'Hearn
2006	B	`conf`	Interprocedural Shape Analysis with Separated Heap Abstractions. SAS Alexey Gotsman, Josh Berdine, Byron Cook
2006	B	`conf`	Over-Approximating Boolean Programs with Unbounded Thread Creation. FMCAD Byron Cook, Daniel Kroening, Natasha Sharygina
2006	J	`jnl`	Predicate Abstraction via Symbolic Decision Procedures CoRR Shuvendu K. Lahiri, Thomas Ball, Byron Cook
2006	—	`conf`	Preface and Foreword. PDPAR/PaUL@FLoC Byron Cook, Roberto Sebastiani
2006	—	`ed.`	Proceedings of the 3rd Workshop on Software Model Checking, SoftMC@CAV 2005, Edinburgh, UK, July 11, 2005 SoftMC@CAV Byron Cook, Scott D. Stoller, Willem Visser
2006	A*	`conf`	Repair of Boolean Programs with an Application to C. CAV Andreas Griesmayer, Roderick Bloem, Byron Cook
2006	A*	`conf`	Termination proofs for systems code. PLDI Byron Cook, Andreas Podelski, Andrey Rybalchenko
2006	A*	`conf`	Terminator: Beyond Safety. CAV Byron Cook, Andreas Podelski, Andrey Rybalchenko
2006	A	`conf`	Thorough static analysis of device drivers. EuroSys Thomas Ball, Ella Bounimova, Byron Cook, Vladimir Levin, Jakob Lichtenberg, Con McGarvey, Bohus Ondrusek, Sriram K. Rajamani, Abdullah Ustuner
2005	B	`conf`	Abstraction Refinement for Termination. SAS Byron Cook, Andreas Podelski, Andrey Rybalchenko
2005	A*	`conf`	Cogent: Accurate Theorem Proving for Program Verification. CAV Byron Cook, Daniel Kroening, Natasha Sharygina
2005	—	`conf`	Finding Bugs in Device Drivers with Static Driver Verifier. Abstract State Machines Byron Cook
2005	A*	`conf`	Predicate Abstraction via Symbolic Decision Procedures. CAV Shuvendu K. Lahiri, Thomas Ball, Byron Cook
2005	—	`conf`	Preface. SoftMC@CAV Byron Cook, Scott D. Stoller, Willem Visser
2005	—	`conf`	Symbolic Model Checking for Asynchronous Boolean Programs. SPIN Byron Cook, Daniel Kroening, Natasha Sharygina
2005	C	`conf`	Using Stålmarck's Algorithm to Prove Inequalities. ICFEM Byron Cook, Georges Gonthier
2004	C	`conf`	Accurate Theorem Proving for Program Verification. ISoLA Byron Cook, Daniel Kroening, Natasha Sharygina
2004	—	`conf`	Finding API usage rule violations in Windows device drivers using Static Driver Verifier. ISoLA (Preliminary proceedings) Byron Cook
2004	A	`conf`	Refining Approximations in Software Predicate Abstraction. TACAS Thomas Ball, Byron Cook, Satyaki Das, Sriram K. Rajamani
2004	B	`conf`	SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft. IFM Thomas Ball, Byron Cook, Vladimir Levin, Sriram K. Rajamani
2004	A*	`conf`	Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement. CAV Thomas Ball, Byron Cook, Shuvendu K. Lahiri, Lintao Zhang
2003	—	`ed.`	2003 Workshop on Software Model Checking, SoftMC 2003, Boulder, Colorado, USA, July 14, 2003 SoftMC Byron Cook, Scott D. Stoller, Willem Visser
2003	A*	`conf`	A Symbolic Approach to Predicate Abstraction. CAV Shuvendu K. Lahiri, Randal E. Bryant, Byron Cook
2003	J	`jnl`	A framework for superscalar microprocessor correctness statements. Int. J. Softw. Tools Technol. Transf. Mark D. Aagaard, Byron Cook, Nancy A. Day, Robert B. Jones
2003	J	`jnl`	Design automation with mixtures of proof strategies for propositional logic. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Gunnar Andersson, Per Bjesse, Byron Cook, Ziyad Hanna
2003	—	`conf`	SoftMC 2003: Workshop on Software Model Checking. SoftMC@CAV Byron Cook, Scott D. Stoller, Willem Visser
2002	A*	`conf`	A proof engine approach to solving combinational design automation problems. DAC Gunnar Andersson, Per Bjesse, Byron Cook, Ziyad Hanna
2001	—	`conf`	A Framework for Microprocessor Correctness Statements. CHARME Mark D. Aagaard, Byron Cook, Nancy A. Day, Robert B. Jones
2000	B	`conf`	Combining Stream-Based and State-Based Verification Techniques. FMCAD Nancy A. Day, Mark D. Aagaard, Byron Cook
1999	—	`conf`	Formal Verification of Explicitly Parallel Microprocessors. CHARME Byron Cook, John Launchbury, John Matthews, Richard B. Kieburtz
1999	A	`conf`	On Embedding a Microarchitectural Design Language within Haskell. ICFP John Launchbury, Jeffrey R. Lewis, Byron Cook
1999	—	`conf`	Symbolic Simulation of Microprocessor Models using Type Classes in Haskell. CHARME Nancy A. Day, Jeffrey R. Lewis, Byron Cook
1998	—	`conf`	Microprocessor Specification in Hawk. ICCL John Matthews, Byron Cook, John Launchbury
1997	A	`conf`	Disposable Memo Functions (Extended Abstract). ICFP Byron Cook, John Launchbury