Byron Cook

Domagoj Babic, Byron Cook, Alan J. Hu, Zvonimir Rakamaric: Proving termination of nonlinear command sequences. Formal Asp. Comput. 25(3): 389-403 (2013)

Alex S. Taylor, Nir Piterman, Samin Ishtiaq, Jasmin Fisher, Byron Cook, Caitlin Cockerton, Sam Bourton, David Benque: At the interface of biology and computation. CHI 2013: 493-502

Byron Cook, Abigail See, Florian Zuleger: Ramsey vs. Lexicographic Termination Proving. TACAS 2013: 47-61

Byron Cook, Eric Koskinen, Moshe Y. Vardi: Temporal property verification as a program analysis task - Extended Version. Formal Methods in System Design 41(1): 66-82 (2012)

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

Byron Cook, Andreas Podelski, Andrey Rybalchenko: Proving program termination. Commun. ACM 54(5): 88-98 (2011)

Alexey Gotsman, Josh Berdine, Byron Cook: Precision and the Conjunction Rule in Concurrent Separation Logic. Electr. Notes Theor. Comput. Sci. 276: 171-190 (2011)

Byron Cook: Advances in Proving Program Termination and Liveness. CADE 2011: 4

Josh Berdine, Byron Cook, Samin Ishtiaq: SLAyer: Memory Safety for Systems-Level Code. CAV 2011: 178-183

Byron Cook, Eric Koskinen, Moshe Y. Vardi: Temporal Property Verification as a Program Analysis Task. CAV 2011: 333-348

Byron Cook, Christoph Haase, Joël Ouaknine, Matthew J. Parkinson, James Worrell: Tractable Reasoning in a Fragment of Separation Logic. CONCUR 2011: 235-249

Byron Cook, Eric Koskinen: Making prophecies with decision predicates. POPL 2011: 399-410

Byron Cook, Jasmin Fisher, Elzbieta Krepska, Nir Piterman: Proving Stabilization of Biological Systems. VMCAI 2011: 134-149

Byron Cook, Daniel Kroening, Philipp Rümmer, Christoph M. Wintersteiger: Ranking Function Synthesis for Bit-Vector Relations. TACAS 2010: 236-250

Tayssir Touili, Byron Cook, Paul Jackson (Eds.): 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

Byron Cook, Andreas Podelski, Andrey Rybalchenko: Summarization for termination: no return! Formal Methods in System Design 35(3): 369-387 (2009)

Byron Cook, Ashutosh Gupta, Stephen Magill, Andrey Rybalchenko, Jirí Simsa, Satnam Singh, Viktor Vafeiadis: Finding heap-bounds for hardware synthesis. FMCAD 2009: 205-212

Byron Cook: Taming the Unbounded for Hardware Synthesis. IFM 2009: 39

Alexey Gotsman, Byron Cook, Matthew J. Parkinson, Viktor Vafeiadis: Proving that non-blocking algorithms don't block. POPL 2009: 16-28

Byron Cook: Advances in Program Termination and Liveness. VMCAI 2009: 4

María Alpuente, Byron Cook, Christophe Joubert (Eds.): 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

Mike Hinchey, Michael Jackson, Patrick Cousot, Byron Cook, Jonathan P. Bowen, Tiziana Margaria: Software engineering and formal methods. Commun. ACM 51(9): 54-59 (2008)

Byron Cook, Sumit Gulwani, Tal Lev-Ami, Andrey Rybalchenko, Mooly Sagiv: Proving Conditional Termination. CAV 2008: 328-340

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

Aziem Chawdhary, Byron Cook, Sumit Gulwani, Mooly Sagiv, Hongseok Yang: Ranking Abstractions. ESOP 2008: 148-162

Byron Cook, Roberto Sebastiani: Preface and Foreword. Electr. Notes Theor. Comput. Sci. 174(8): 3-6 (2007)

Byron Cook, Roberto Sebastiani: Preface. JSAT 3(1-2) (2007)

Shuvendu K. Lahiri, Thomas Ball, Byron Cook: Predicate Abstraction via Symbolic Decision Procedures. Logical Methods in Computer Science 3(2) (2007)

Byron Cook, Daniel Kroening, Natasha Sharygina: Verification of Boolean programs with unbounded thread creation. Theor. Comput. Sci. 388(1-3): 227-242 (2007)

Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky, Mooly Sagiv: Local Reasoning for Storable Locks and Threads. APLAS 2007: 19-37

Byron Cook: Automatically Proving Program Termination. CAV 2007: 1

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

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

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

Byron Cook: Bringing Hardware and Software Closer Together with Termination Analysis. MEMOCODE 2007: 201

Alexey Gotsman, Josh Berdine, Byron Cook, Mooly Sagiv: Thread-modular shape analysis. PLDI 2007: 266-277

Byron Cook, Andreas Podelski, Andrey Rybalchenko: Proving thread termination. PLDI 2007: 320-330

Josh Berdine, Aziem Chawdhary, Byron Cook, Dino Distefano, Peter W. O'Hearn: Variance analyses from invariance analyses. POPL 2007: 211-224

Byron Cook, Alexey Gotsman, Andreas Podelski, Andrey Rybalchenko, Moshe Y. Vardi: Proving that programs eventually do something good. POPL 2007: 265-276

Stephen Magill, Josh Berdine, Edmund M. Clarke, Byron Cook: Arithmetic Strengthening for Shape Analysis. SAS 2007: 419-436

Domagoj Babic, Alan J. Hu, Zvonimir Rakamaric, Byron Cook: Proving Termination by Divergence. SEFM 2007: 93-102

Byron Cook: Automatically Proving Concurrent Programs Correct. SEFM 2007: 269-272

Roman Manevich, Josh Berdine, Byron Cook, G. Ramalingam, Mooly Sagiv: Shape Analysis by Graph Decomposition. TACAS 2007: 3-18

Franz Baader, Byron Cook, Jürgen Giesl, Robert Nieuwenhuis (Eds.): Deduction and Decision Procedures, 30.09. - 05.10.2007. Dagstuhl Seminar Proceedings 07401, Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany 2007

Byron Cook, Andreas Podelski (Eds.): 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

Byron Cook, Scott D. Stoller, Willem Visser: Preface. Electr. Notes Theor. Comput. Sci. 144(3): 1-2 (2006)

Andreas Griesmayer, Roderick Bloem, Byron Cook: Repair of Boolean Programs with an Application to C. CAV 2006: 358-371

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

Byron Cook, Andreas Podelski, Andrey Rybalchenko: Terminator: Beyond Safety. CAV 2006: 415-418

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

Byron Cook, Daniel Kroening, Natasha Sharygina: Over-Approximating Boolean Programs with Unbounded Thread Creation. FMCAD 2006: 53-59

Byron Cook, Andreas Podelski, Andrey Rybalchenko: Termination proofs for systems code. PLDI 2006: 415-426

Alexey Gotsman, Josh Berdine, Byron Cook: Interprocedural Shape Analysis with Separated Heap Abstractions. SAS 2006: 240-260

Shuvendu K. Lahiri, Thomas Ball, Byron Cook: Predicate Abstraction via Symbolic Decision Procedures. CoRR abs/cs/0612003 (2006)

Byron Cook: Finding Bugs in Device Drivers with Static Driver Verifier. Abstract State Machines 2005: 71

Shuvendu K. Lahiri, Thomas Ball, Byron Cook: Predicate Abstraction via Symbolic Decision Procedures. CAV 2005: 24-38

Byron Cook, Daniel Kroening, Natasha Sharygina: Cogent: Accurate Theorem Proving for Program Verification. CAV 2005: 296-300

Byron Cook, Georges Gonthier: Using Stålmarck's Algorithm to Prove Inequalities. ICFEM 2005: 330-344

Byron Cook, Andreas Podelski, Andrey Rybalchenko: Abstraction Refinement for Termination. SAS 2005: 87-101

Byron Cook, Daniel Kroening, Natasha Sharygina: Symbolic Model Checking for Asynchronous Boolean Programs. SPIN 2005: 75-90

Thomas Ball, Byron Cook, Shuvendu K. Lahiri, Lintao Zhang: Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement. CAV 2004: 457-461

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

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

Byron Cook, Daniel Kroening, Natasha Sharygina: Accurate Theorem Proving for Program Verification. ISoLA 2004: 96-114

Thomas Ball, Byron Cook, Satyaki Das, Sriram K. Rajamani: Refining Approximations in Software Predicate Abstraction. TACAS 2004: 388-403

Byron Cook, Scott D. Stoller, Willem Visser: SoftMC 2003: Workshop on Software Model Checking. Electr. Notes Theor. Comput. Sci. 89(3): 377 (2003)

Mark Aagaard, Byron Cook, Nancy A. Day, Robert B. Jones: A framework for superscalar microprocessor correctness statements. STTT 4(3): 298-312 (2003)

Gunnar Andersson, Per Bjesse, Byron Cook, Ziyad Hanna: Design automation with mixtures of proof strategies for propositional logic. IEEE Trans. on CAD of Integrated Circuits and Systems 22(8): 1042-1048 (2003)

Shuvendu K. Lahiri, Randal E. Bryant, Byron Cook: A Symbolic Approach to Predicate Abstraction. CAV 2003: 141-153

Gunnar Andersson, Per Bjesse, Byron Cook, Ziyad Hanna: A proof engine approach to solving combinational design automation problems. DAC 2002: 725-730

Mark Aagaard, Byron Cook, Nancy A. Day, Robert B. Jones: A Framework for Microprocessor Correctness Statements. CHARME 2001: 433-448

Nancy A. Day, Mark Aagaard, Byron Cook: Combining Stream-Based and State-Based Verification Techniques. FMCAD 2000: 126-142

Byron Cook, John Launchbury, John Matthews, Richard B. Kieburtz: Formal Verification of Explicitly Parallel Microprocessors. CHARME 1999: 23-36

Nancy A. Day, Jeffrey R. Lewis, Byron Cook: Symbolic Simulation of Microprocessor Models using Type Classes in Haskell. CHARME 1999: 346-349

John Launchbury, Jeffrey R. Lewis, Byron Cook: On Embedding a Microarchitectural Design Language within Haskell. ICFP 1999: 60-69

John Matthews, Byron Cook, John Launchbury: Microprocessor Specification in Hawk. ICCL 1998: 90-101

Byron Cook, John Launchbury: Disposable Memo Functions (Extended Abstract). ICFP 1997: 310