| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Alexey Gotsman, Josh Berdine, Byron Cook |
Precision and the Conjunction Rule in Concurrent Separation Logic.  |
Electr. Notes Theor. Comput. Sci.  |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Byron Cook, Andreas Podelski, Andrey Rybalchenko |
Proving program termination. |
Commun. ACM |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Byron Cook, Christoph Haase, Joël Ouaknine, Matthew J. Parkinson, James Worrell |
Tractable Reasoning in a Fragment of Separation Logic. |
CONCUR |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Byron Cook |
Advances in Proving Program Termination and Liveness. |
CADE |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Byron Cook, Eric Koskinen |
Making prophecies with decision predicates. |
POPL |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Josh Berdine, Byron Cook, Samin Ishtiaq |
SLAyer: Memory Safety for Systems-Level Code. |
CAV |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Byron Cook, Eric Koskinen, Moshe Y. Vardi |
Temporal Property Verification as a Program Analysis Task. |
CAV |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Byron Cook, Jasmin Fisher, Elzbieta Krepska, Nir Piterman |
Proving Stabilization of Biological Systems. |
VMCAI |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Byron Cook, Daniel Kroening, Philipp Rümmer, Christoph M. Wintersteiger |
Ranking Function Synthesis for Bit-Vector Relations. |
TACAS |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Tayssir Touili, Byron Cook, Paul Jackson (eds.) |
Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings |
CAV |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Byron Cook, Andreas Podelski, Andrey Rybalchenko |
Summarization for termination: no return! |
Formal Methods in System Design |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Byron Cook, Ashutosh Gupta, Stephen Magill, Andrey Rybalchenko, Jirí Simsa, Satnam Singh, Viktor Vafeiadis |
Finding heap-bounds for hardware synthesis. |
FMCAD |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
FMICS |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Alexey Gotsman, Byron Cook, Matthew J. Parkinson, Viktor Vafeiadis |
Proving that non-blocking algorithms don't block. |
POPL |
2009 |
DBLP DOI BibTeX RDF |
formal verification, concurrent programming, termination, liveness |
| 1 | Byron Cook |
Taming the Unbounded for Hardware Synthesis. |
IFM |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Byron Cook |
Advances in Program Termination and Liveness. |
VMCAI |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Mike Hinchey, Michael Jackson, Patrick Cousot, Byron Cook, Jonathan P. Bowen, Tiziana Margaria |
Software engineering and formal methods. |
Commun. ACM |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Byron Cook, Sumit Gulwani, Tal Lev-Ami, Andrey Rybalchenko, Mooly Sagiv |
Proving Conditional Termination. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Hongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn |
Scalable Shape Analysis for Systems Code. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Aziem Chawdhary, Byron Cook, Sumit Gulwani, Mooly Sagiv, Hongseok Yang |
Ranking Abstractions. |
ESOP |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Byron Cook, Daniel Kroening, Natasha Sharygina |
Verification of Boolean programs with unbounded thread creation. |
Theor. Comput. Sci. |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Byron Cook, Roberto Sebastiani |
Preface. |
JSAT |
2007 |
DBLP BibTeX RDF |
|
| 1 | Shuvendu K. Lahiri, Thomas Ball, Byron Cook |
Predicate Abstraction via Symbolic Decision Procedures. |
Logical Methods in Computer Science |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Byron Cook, Roberto Sebastiani |
Preface and Foreword. |
Electr. Notes Theor. Comput. Sci. |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Byron Cook, Andreas Podelski, Andrey Rybalchenko |
Proving thread termination. |
PLDI |
2007 |
DBLP DOI BibTeX RDF |
model checking, concurrency, formal verification, program verification, threads, termination |
| 1 | Alexey Gotsman, Josh Berdine, Byron Cook, Mooly Sagiv |
Thread-modular shape analysis. |
PLDI |
2007 |
DBLP DOI BibTeX RDF |
static analysis, abstract interpretation, concurrent programming, shape analysis |
| 1 | Domagoj Babic, Alan J. Hu, Zvonimir Rakamaric, Byron Cook |
Proving Termination by Divergence. |
SEFM |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Byron Cook |
Automatically Proving Concurrent Programs Correct. |
SEFM |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Byron Cook |
Bringing Hardware and Software Closer Together with Termination Analysis. |
MEMOCODE |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Roman Manevich, Josh Berdine, Byron Cook, G. Ramalingam, Mooly Sagiv |
Shape Analysis by Graph Decomposition. |
TACAS |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Byron Cook, Alexey Gotsman, Andreas Podelski, Andrey Rybalchenko, Moshe Y. Vardi |
Proving that programs eventually do something good. |
POPL |
2007 |
DBLP DOI BibTeX RDF |
formal verification, termination, liveness, software model checking |
| 1 | Josh Berdine, Aziem Chawdhary, Byron Cook, Dino Distefano, Peter W. O'Hearn |
Variance analyses from invariance analyses. |
POPL |
2007 |
DBLP DOI BibTeX RDF |
formal verification, program analysis, termination, liveness, software model checking |
| 1 | Franz Baader, Byron Cook, Jürgen Giesl, Robert Nieuwenhuis |
07401 Executive Summary -- Deduction and Decision Procedures. |
Deduction and Decision Procedures |
2007 |
DBLP BibTeX RDF |
|
| 1 | Franz Baader, Byron Cook, Jürgen Giesl, Robert Nieuwenhuis (eds.) |
Deduction and Decision Procedures, 30.09. - 05.10.2007 |
Deduction and Decision Procedures |
2007 |
DBLP BibTeX RDF |
|
| 1 | Franz Baader, Byron Cook, Jürgen Giesl, Robert Nieuwenhuis |
07401 Abstracts Collection -- Deduction and Decision Procedures. |
Deduction and Decision Procedures |
2007 |
DBLP BibTeX RDF |
|
| 1 | Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky, Mooly Sagiv |
Local Reasoning for Storable Locks and Threads. |
APLAS |
2007 |
DBLP DOI BibTeX RDF |
|
| 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 |
DBLP DOI BibTeX RDF |
|
| 1 | Byron Cook |
Automatically Proving Program Termination. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Stephen Magill, Josh Berdine, Edmund M. Clarke, Byron Cook |
Arithmetic Strengthening for Shape Analysis. |
SAS |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Byron Cook, Andreas Podelski (eds.) |
Verification, Model Checking, and Abstract Interpretation, 8th International Conference, VMCAI 2007, Nice, France, January 14-16, 2007, Proceedings |
VMCAI |
2007 |
DBLP BibTeX RDF |
|
| 1 | Byron Cook, Scott D. Stoller, Willem Visser |
Preface. |
Electr. Notes Theor. Comput. Sci. |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Shuvendu K. Lahiri, Thomas Ball, Byron Cook |
Predicate Abstraction via Symbolic Decision Procedures |
CoRR |
2006 |
DBLP BibTeX RDF |
|
| 1 | Byron Cook, Andreas Podelski, Andrey Rybalchenko |
Termination proofs for systems code. |
PLDI |
2006 |
DBLP DOI BibTeX RDF |
model checking, formal verification, program verification, program termination |
| 1 | Byron Cook, Daniel Kroening, Natasha Sharygina |
Over-Approximating Boolean Programs with Unbounded Thread Creation. |
FMCAD |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
DBLP DOI BibTeX RDF |
formal verification, software model checking |
| 1 | Byron Cook, Andreas Podelski, Andrey Rybalchenko |
Terminator: Beyond Safety. |
CAV |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Josh Berdine, Byron Cook, Dino Distefano, Peter W. O'Hearn |
Automatic Termination Proofs for Programs with Shape-Shifting Heaps. |
CAV |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Andreas Griesmayer, Roderick Bloem, Byron Cook |
Repair of Boolean Programs with an Application to C. |
CAV |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Alexey Gotsman, Josh Berdine, Byron Cook |
Interprocedural Shape Analysis with Separated Heap Abstractions. |
SAS |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Byron Cook, Georges Gonthier |
Using Stålmarck's Algorithm to Prove Inequalities. |
ICFEM |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Byron Cook, Daniel Kroening, Natasha Sharygina |
Symbolic Model Checking for Asynchronous Boolean Programs. |
SPIN |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Shuvendu K. Lahiri, Thomas Ball, Byron Cook |
Predicate Abstraction via Symbolic Decision Procedures. |
CAV |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Byron Cook, Daniel Kroening, Natasha Sharygina |
Cogent: Accurate Theorem Proving for Program Verification. |
CAV |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Byron Cook, Andreas Podelski, Andrey Rybalchenko |
Abstraction Refinement for Termination. |
SAS |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Byron Cook |
Finding Bugs in Device Drivers with Static Driver Verifier. |
Abstract State Machines |
2005 |
DBLP BibTeX RDF |
|
| 1 | Thomas Ball, Byron Cook, Satyaki Das, Sriram K. Rajamani |
Refining Approximations in Software Predicate Abstraction. |
TACAS |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Thomas Ball, Byron Cook, Vladimir Levin, Sriram K. Rajamani |
SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft. |
IFM |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Thomas Ball, Byron Cook, Shuvendu K. Lahiri, Lintao Zhang |
Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement. |
CAV |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Byron Cook, Daniel Kroening, Natasha Sharygina |
Accurate Theorem Proving for Program Verification. |
ISoLA |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Byron Cook |
Finding API usage rule violations in Windows device drivers using Static Driver Verifier. |
ISoLA (Preliminary proceedings) |
2004 |
DBLP BibTeX RDF |
|
| 1 | Byron Cook, Scott D. Stoller, Willem Visser |
SoftMC 2003: Workshop on Software Model Checking. |
Electr. Notes Theor. Comput. Sci. |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Mark Aagaard, Byron Cook, Nancy A. Day, Robert B. Jones |
A framework for superscalar microprocessor correctness statements. |
STTT |
2003 |
DBLP DOI BibTeX RDF |
Microprocessor correctness, Commuting diagrams, Formal verification, Pipelines |
| 1 | Shuvendu K. Lahiri, Randal E. Bryant, Byron Cook |
A Symbolic Approach to Predicate Abstraction. |
CAV |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Gunnar Andersson, Per Bjesse, Byron Cook, Ziyad Hanna |
A proof engine approach to solving combinational design automation problems. |
DAC |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Mark Aagaard, Byron Cook, Nancy A. Day, Robert B. Jones |
A Framework for Microprocessor Correctness Statements. |
CHARME |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Nancy A. Day, Mark Aagaard, Byron Cook |
Combining Stream-Based and State-Based Verification Techniques. |
FMCAD |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Nancy A. Day, Jeffrey R. Lewis, Byron Cook |
Symbolic Simulation of Microprocessor Models using Type Classes in Haskell. |
CHARME |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Byron Cook, John Launchbury, John Matthews, Richard B. Kieburtz |
Formal Verification of Explicitly Parallel Microprocessors. |
CHARME |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | John Launchbury, Jeffrey R. Lewis, Byron Cook |
On Embedding a Microarchitectural Design Language within Haskell. |
ICFP |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | John Matthews, Byron Cook, John Launchbury |
Microprocessor Specification in Hawk. (PDF / PS) |
ICCL |
1998 |
DBLP DOI BibTeX RDF |
Microprocessor Verification, Domain-Specific Language, Functional Language, Hardware Verification |
| 1 | Byron Cook, John Launchbury |
Disposable Memo Functions (Extended Abstract). |
ICFP |
1997 |
DBLP DOI BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")