Byron Cook

Byron Cook: Research papers
  • Proving that non-blocking algorithms don't block (Draft)
    Alexey Gotsman, Byron Cook, Matthew Parkinson, and Viktor Vafeiadis
    Submitted for publication

  • Principles of program termination (Draft)
    Byron Cook
    Notes from the 2008 Marktoberdorf summer school

  • Proving conditional termination
    Byron Cook, Sumit Gulwani, Tal Lev-Ami, Andrey Rybalchenko, and Mooly Sagiv
    CAV'08 [International Conference on Computer-Aided Verification] (Princeton)

  • Scalable shape analysis for systems code
    Hongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, and Peter O'Hearn
    CAV'08 [International Conference on Computer-Aided Verification] (Princeton)

  • Ranking abstractions
    Aziem Chawdhary, Byron Cook, Sumit Gulwani, Mooly Sagiv, and Hongseok Yang
    ESOP'08 [European Symposium on Programming] (Budapest)

  • Verification of Boolean programs with unbounded thread creation
    Byron Cook, Daniel Kroening, and Natasha Sharygina
    Journal of Theoretical Computer Science, Vol. 388, 2007, pp. 227-242

  • Predicate abstraction via symbolic decision procedures
    Shuvendu Lahiri, Thomas Ball and Byron Cook
    Journal of Logical Methods in Computer Science, Vol. 3, 2007, pp. 1-20

  • Proving thread termination
    Byron Cook, Andreas Podelski, and Andrey Rybalchenko
    PLDI'07 [Conference on Programming Language Design and Implementation] (San Diego)

  • Thread-modular shape analysis
    Alexey Gotsman, Josh Berdine, Byron Cook, and Mooly Sagiv
    PLDI'07 [Conference on Programming Language Design and Implementation] (San Diego)

  • Local reasoning for storable locks and threads
    Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky, and Mooly Sagiv
    APLAS'07 [Asian Symposium on Programming Languages and Systems] (Singapore)

  • Shape analysis for composite data structures
    Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter O'Hearn, Thomas Wies, and Hongseok Yang
    CAV'07 [International Conference on Computer-Aided Verification] (Berlin)

  • Proving termination by divergence
    Domagoj Babic, Byron Cook, Alan Hu, Zvonimir Rakamaric
    SEFM'07 [ International Conference on Software Engineering and Formal Methods] (London)

  • Arithmetic strengthening for shape analysis
    Stephen Magill, Josh Berdine, Edmund Clarke, and Byron Cook.
    SAS'07 [International Static Analysis Symposium] (Denmark)

  • Proving that programs eventually do something good
    Byron Cook, Alexey Gotsman, Andreas Podelski, Andrey Rybalchenko, and Moshe Vardi
    POPL'07 [Symposium on Principles of Programming Languages] (Nice)

  • Variance analyses from invariance analyses
    Josh Berdine, Aziem Chawdhary, Byron Cook, Dino Distefano, and Peter O'Hearn
    POPL'07 [Symposium on Principles of Programming Languages] (Nice)

  • Shape analysis by graph decomposition
    Roman Manevich, Josh Berdine, Byron Cook, Ganesan Ramalingam, and Mooly Sagiv
    TACAS'07 [International Conference on Tools and Algorithms for the Construction and Analysis of Systems] (Braga)

  • Automatic termination proofs for programs with shape-shifting heaps
    Josh Berdine, Byron Cook, Dino Distefano, and Peter O'Hearn
    CAV'06 [International Conference on Computer-Aided Verification] (Seattle)

  • Terminator: Beyond safety (short tool description paper)
    Byron Cook, Andreas Podelski, and Andrey Rybalchenko
    CAV'06 [International Conference on Computer-Aided Verification] (Seattle)

  • Repair of Boolean programs with an application to C
    Andreas Griesmayer, Roderick Bloem, and Byron Cook
    CAV'06 [International Conference on Computer-Aided Verification] (Seattle)

  • Termination proofs for systems code
    Byron Cook, Andreas Podelski, and Andrey Rybalchenko
    PLDI'06 [Conference on Programming Language Design and Implementation] (Ottawa)

  • 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
    EuroSys'06 [European Systems Conference] (Leuven)

  • Over-approximating Boolean programs with unbounded thread creation
    Byron Cook, Daniel Kroening, Natasha Sharygina
    FMCAD'06 [Formal Methods in Computer Aided Design] (San Jose)

  • Interprocedural shape analysis with separated heap abstractions
    Alexey Gotsman, Josh Berdine, and Byron Cook
    SAS'06 [International Static Analysis Symposium] (Seoul)

  • Abstraction refinement for termination
    Byron Cook, Andreas Podelski, Andrey Rybalchenko
    SAS'05 [International Static Analysis Symposium] (London)

  • Using Stalmarck's algorithm to prove inequalities
    Byron Cook, Georges Gonthier
    ICFEM'05 [International Conference on Formal Engineering Methods] (Manchester)

  • Symbolic model checking for asynchronous Boolean programs
    Byron Cook, Daniel Kroening, Natasha Sharygina
    SPIN'05 (San Francisco)

  • Predicate abstraction via symbolic decision procedures
    Shuvendu Lahiri, Thomas Ball and Byron Cook
    CAV'05 [International Conference on Computer-Aided Verification] (Edinburgh)

  • Cogent: Accurate theorem proving for program verification (short tool description paper)
    Byron Cook, Daniel Kroening, Natasha Sharygina
    CAV'05 [International Conference on Computer-Aided Verification] (Edinburgh)

  • Zapato: Automatic theorem proving for predicate abstraction refinement (short tool description paper)
    Thomas Ball, Byron Cook, Shuvendu K. Lahriri, and Lintao Zhang
    CAV'04 [International Conference on Computer-Aided Verification] (Boston)

  • Refining approximations in software predicate abstraction
    Thomas Ball, Byron Cook, Satyaki Das, and Sriram K. Rajamani
    TACAS'04 (Tenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems)

  • A symbolic approach to predicate abstraction
    Shuvendu K. Lahiri, Randal E. Bryant, and Byron Cook
    CAV'03 [International Conference on Computer-Aided Verification] (Boulder)

  • Design automation with mixtures of proof strategies for propositional logic
    Gunnar Andersson, Per Bjesse, Byron Cook and Ziyad Hanna
    IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol. 22(8) 2003

  • A proof engine approach to solving combinational design automation problems
    Gunnar Andersson, Per Bjesse, Byron Cook, and Ziyad Hanna
    DAC'02 [Design Automation Conference] (Las Vegas)

  • A framework for microprocessor correctness statements
    Mark Aagaard, Byron Cook, Nancy Day, and Robert Jones
    International Journal on Software Tools for Technology Transfer, Vol. 4(3), 2003

  • A framework for microprocessor correctness statements
    Mark Aagaard, Byron Cook, Nancy Day, and Robert Jones
    CHARME'01 [Correct Hardware Design and Verification Methods] (Edinburgh)

  • Combining stream-based and state-based verification techniques for microarchitectures
    Mark Aagaard, Byron Cook, and Nancy Day
    FMCAD'00 [International Conference on Formal Methods in Computer Aided Design] (Austin)

  • Formal verification of explicitly parallel microprocessors
    Byron Cook, John Launchbury, John Matthews, and Dick Kieburtz CHARME'99 [Conference on Correct Hardware Design and Verification Methods] (Bad Herrenalb)

  • On embedding a microarchitectural design language within Haskell
    John Launchbury, Jeff Lewis and Byron Cook
    ICFP'99 [International Conference on Functional Programming] (Paris)

  • Specifying superscalar microprocessors in Hawk
    Byron Cook, John Launchbury, and John Matthews
    1998 Workshop on Formal Techniques for Hardware (Marstrand)

  • Microprocessor specification in Hawk
    John Matthews, John Launchbury, and Byron Cook
    ICL'98 [International Conference on Computer Languages] (Chicago)

  • Disposable memo functions
    Byron Cook and John Launchbury
    1997 Haskell Workshop Proceedings (Amsterdam)


See my new paper: "Proving that non-blocking algorithms don't block".

Navigation:

Projects:

Upcoming events:



Last modified: Mon Jul 28 08:43:01 GMTDT 2008