2009 |
59 | EE | Byron Cook:
Taming the Unbounded for Hardware Synthesis.
IFM 2009: 39 |
58 | EE | Alexey Gotsman,
Byron Cook,
Matthew J. Parkinson,
Viktor Vafeiadis:
Proving that non-blocking algorithms don't block.
POPL 2009: 16-28 |
57 | EE | Byron Cook:
Advances in Program Termination and Liveness.
VMCAI 2009: 4 |
2008 |
56 | EE | Byron Cook,
Sumit Gulwani,
Tal Lev-Ami,
Andrey Rybalchenko,
Mooly Sagiv:
Proving Conditional Termination.
CAV 2008: 328-340 |
55 | EE | 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 |
54 | EE | Aziem Chawdhary,
Byron Cook,
Sumit Gulwani,
Mooly Sagiv,
Hongseok Yang:
Ranking Abstractions.
ESOP 2008: 148-162 |
53 | EE | 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) |
2007 |
52 | | Franz Baader,
Byron Cook,
Jürgen Giesl,
Robert Nieuwenhuis:
Deduction and Decision Procedures, 30.09. - 05.10.2007
Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany 2007 |
51 | | Byron Cook,
Andreas Podelski:
Verification, Model Checking, and Abstract Interpretation, 8th International Conference, VMCAI 2007, Nice, France, January 14-16, 2007, Proceedings
Springer 2007 |
50 | EE | Alexey Gotsman,
Josh Berdine,
Byron Cook,
Noam Rinetzky,
Mooly Sagiv:
Local Reasoning for Storable Locks and Threads.
APLAS 2007: 19-37 |
49 | EE | Byron Cook:
Automatically Proving Program Termination.
CAV 2007: 1 |
48 | EE | 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 |
47 | EE | Franz Baader,
Byron Cook,
Jürgen Giesl,
Robert Nieuwenhuis:
07401 Abstracts Collection -- Deduction and Decision Procedures.
Deduction and Decision Procedures 2007 |
46 | EE | Franz Baader,
Byron Cook,
Jürgen Giesl,
Robert Nieuwenhuis:
07401 Executive Summary -- Deduction and Decision Procedures.
Deduction and Decision Procedures 2007 |
45 | EE | Byron Cook:
Bringing Hardware and Software Closer Together with Termination Analysis.
MEMOCODE 2007: 201 |
44 | EE | Alexey Gotsman,
Josh Berdine,
Byron Cook,
Mooly Sagiv:
Thread-modular shape analysis.
PLDI 2007: 266-277 |
43 | EE | Byron Cook,
Andreas Podelski,
Andrey Rybalchenko:
Proving thread termination.
PLDI 2007: 320-330 |
42 | EE | Josh Berdine,
Aziem Chawdhary,
Byron Cook,
Dino Distefano,
Peter W. O'Hearn:
Variance analyses from invariance analyses.
POPL 2007: 211-224 |
41 | EE | Byron Cook,
Alexey Gotsman,
Andreas Podelski,
Andrey Rybalchenko,
Moshe Y. Vardi:
Proving that programs eventually do something good.
POPL 2007: 265-276 |
40 | EE | Stephen Magill,
Josh Berdine,
Edmund M. Clarke,
Byron Cook:
Arithmetic Strengthening for Shape Analysis.
SAS 2007: 419-436 |
39 | EE | Byron Cook:
Automatically Proving Concurrent Programs Correct.
SEFM 2007: 269-272 |
38 | EE | Domagoj Babic,
Alan J. Hu,
Zvonimir Rakamaric,
Byron Cook:
Proving Termination by Divergence.
SEFM 2007: 93-102 |
37 | EE | Roman Manevich,
Josh Berdine,
Byron Cook,
G. Ramalingam,
Mooly Sagiv:
Shape Analysis by Graph Decomposition.
TACAS 2007: 3-18 |
36 | EE | Byron Cook,
Roberto Sebastiani:
Preface and Foreword.
Electr. Notes Theor. Comput. Sci. 174(8): 3-6 (2007) |
35 | EE | Byron Cook,
Roberto Sebastiani:
Preface.
JSAT 3(1-2): (2007) |
34 | EE | Shuvendu K. Lahiri,
Thomas Ball,
Byron Cook:
Predicate Abstraction via Symbolic Decision Procedures.
Logical Methods in Computer Science 3(2): (2007) |
33 | EE | Byron Cook,
Daniel Kroening,
Natasha Sharygina:
Verification of Boolean programs with unbounded thread creation.
Theor. Comput. Sci. 388(1-3): 227-242 (2007) |
2006 |
32 | EE | Andreas Griesmayer,
Roderick Bloem,
Byron Cook:
Repair of Boolean Programs with an Application to C.
CAV 2006: 358-371 |
31 | EE | Josh Berdine,
Byron Cook,
Dino Distefano,
Peter W. O'Hearn:
Automatic Termination Proofs for Programs with Shape-Shifting Heaps.
CAV 2006: 386-400 |
30 | EE | Byron Cook,
Andreas Podelski,
Andrey Rybalchenko:
Terminator: Beyond Safety.
CAV 2006: 415-418 |
29 | EE | 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 |
28 | EE | Byron Cook,
Daniel Kroening,
Natasha Sharygina:
Over-Approximating Boolean Programs with Unbounded Thread Creation.
FMCAD 2006: 53-59 |
27 | EE | Byron Cook,
Andreas Podelski,
Andrey Rybalchenko:
Termination proofs for systems code.
PLDI 2006: 415-426 |
26 | EE | Alexey Gotsman,
Josh Berdine,
Byron Cook:
Interprocedural Shape Analysis with Separated Heap Abstractions.
SAS 2006: 240-260 |
25 | EE | Shuvendu K. Lahiri,
Thomas Ball,
Byron Cook:
Predicate Abstraction via Symbolic Decision Procedures
CoRR abs/cs/0612003: (2006) |
24 | EE | Byron Cook,
Scott D. Stoller,
Willem Visser:
Preface.
Electr. Notes Theor. Comput. Sci. 144(3): 1-2 (2006) |
2005 |
23 | EE | Byron Cook:
Finding Bugs in Device Drivers with Static Driver Verifier.
Abstract State Machines 2005: 71 |
22 | EE | Shuvendu K. Lahiri,
Thomas Ball,
Byron Cook:
Predicate Abstraction via Symbolic Decision Procedures.
CAV 2005: 24-38 |
21 | EE | Byron Cook,
Daniel Kroening,
Natasha Sharygina:
Cogent: Accurate Theorem Proving for Program Verification.
CAV 2005: 296-300 |
20 | EE | Byron Cook,
Georges Gonthier:
Using Stålmarck's Algorithm to Prove Inequalities.
ICFEM 2005: 330-344 |
19 | EE | Byron Cook,
Andreas Podelski,
Andrey Rybalchenko:
Abstraction Refinement for Termination.
SAS 2005: 87-101 |
18 | EE | Byron Cook,
Daniel Kroening,
Natasha Sharygina:
Symbolic Model Checking for Asynchronous Boolean Programs.
SPIN 2005: 75-90 |
2004 |
17 | EE | Thomas Ball,
Byron Cook,
Shuvendu K. Lahiri,
Lintao Zhang:
Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement.
CAV 2004: 457-461 |
16 | EE | 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 |
15 | EE | Byron Cook,
Daniel Kroening,
Natasha Sharygina:
Accurate Theorem Proving for Program Verification.
ISoLA 2004: 96-114 |
14 | | Byron Cook:
Finding API usage rule violations in Windows device drivers using Static Driver Verifier.
ISoLA (Preliminary proceedings) 2004: 18-18 |
13 | EE | Thomas Ball,
Byron Cook,
Satyaki Das,
Sriram K. Rajamani:
Refining Approximations in Software Predicate Abstraction.
TACAS 2004: 388-403 |
2003 |
12 | EE | Shuvendu K. Lahiri,
Randal E. Bryant,
Byron Cook:
A Symbolic Approach to Predicate Abstraction.
CAV 2003: 141-153 |
11 | EE | Byron Cook,
Scott D. Stoller,
Willem Visser:
SoftMC 2003: Workshop on Software Model Checking.
Electr. Notes Theor. Comput. Sci. 89(3): (2003) |
10 | EE | 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) |
9 | EE | Mark Aagaard,
Byron Cook,
Nancy A. Day,
Robert B. Jones:
A framework for superscalar microprocessor correctness statements.
STTT 4(3): 298-312 (2003) |
2002 |
8 | EE | Gunnar Andersson,
Per Bjesse,
Byron Cook,
Ziyad Hanna:
A proof engine approach to solving combinational design automation problems.
DAC 2002: 725-730 |
2001 |
7 | EE | Mark Aagaard,
Byron Cook,
Nancy A. Day,
Robert B. Jones:
A Framework for Microprocessor Correctness Statements.
CHARME 2001: 433-448 |
2000 |
6 | EE | Nancy A. Day,
Mark Aagaard,
Byron Cook:
Combining Stream-Based and State-Based Verification Techniques.
FMCAD 2000: 126-142 |
1999 |
5 | EE | Byron Cook,
John Launchbury,
John Matthews,
Richard B. Kieburtz:
Formal Verification of Explicitly Parallel Microprocessors.
CHARME 1999: 23-36 |
4 | EE | Nancy A. Day,
Jeffrey R. Lewis,
Byron Cook:
Symbolic Simulation of Microprocessor Models using Type Classes in Haskell.
CHARME 1999: 346-349 |
3 | EE | John Launchbury,
Jeffrey R. Lewis,
Byron Cook:
On Embedding a Microarchitectural Design Language within Haskell.
ICFP 1999: 60-69 |
1998 |
2 | EE | John Matthews,
Byron Cook,
John Launchbury:
Microprocessor Specification in Hawk.
ICCL 1998: 90-101 |
1997 |
1 | | Byron Cook,
John Launchbury:
Disposable Memo Functions (Extended Abstract).
ICFP 1997: 310 |