# Byron Cook

According to our database

Collaborative distances:

^{1}, Byron Cook authored at least 90 papers between 1997 and 2018.Collaborative distances:

## Timeline

#### Legend:

Book In proceedings Article PhD thesis Other## Links

#### On csauthors.net:

## Bibliography

2018

SideTrail: Verifying Time-Balancing of Cryptosystems.

Proceedings of the Verified Software. Theories, Tools, and Experiments, 2018

Semantic-based Automated Reasoning for AWS Access Policies using SMT.

Proceedings of the 2018 Formal Methods in Computer Aided Design, 2018

Model Checking Boot Code from AWS Data Centers.

Proceedings of the Computer Aided Verification - 30th International Conference, 2018

Formal Reasoning About the Security of Amazon Web Services.

Proceedings of the Computer Aided Verification - 30th International Conference, 2018

Continuous Formal Verification of Amazon s2n.

Proceedings of the Computer Aided Verification - 30th International Conference, 2018

2017

Verifying Increasingly Expressive Temporal Logics for Infinite-State Systems.

J. ACM, 2017

Automated formal reasoning about amazon web services (keynote).

Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, 2017

Automated formal reasoning about AWS systems.

Proceedings of the 2017 Formal Methods in Computer Aided Design, 2017

2016

T2: Temporal Property Verification.

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2016

2015

Embracing Overapproximation for Proving Nontermination.

TinyToCS, 2015

Fairness for Infinite-State Systems.

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2015

Spatial Interpolants.

Proceedings of the Programming Languages and Systems, 2015

On Automation of CTL* Verification for Infinite-State Systems.

Proceedings of the Computer Aided Verification - 27th International Conference, 2015

2014

Proving Nontermination via Safety.

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2014

Faster temporal reasoning for infinite-state programs.

Proceedings of the Formal Methods in Computer-Aided Design, 2014

Disproving termination with overapproximation.

Proceedings of the Formal Methods in Computer-Aided Design, 2014

Finding Instability in Biological Models.

Proceedings of the Computer Aided Verification - 26th International Conference, 2014

2013

Proving termination of nonlinear command sequences.

Formal Asp. Comput., 2013

Ramsey vs. Lexicographic Termination Proving.

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2013

Reasoning about nondeterminism in programs.

Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2013

At the interface of biology and computation.

Proceedings of the 2013 ACM SIGCHI Conference on Human Factors in Computing Systems, 2013

Better Termination Proving through Cooperation.

Proceedings of the Computer Aided Verification - 25th International Conference, 2013

2012

Temporal property verification as a program analysis task - Extended Version.

Formal Methods in System Design, 2012

Bma: Visual Tool for Modeling and Analyzing Biological Networks.

Proceedings of the Computer Aided Verification - 24th International Conference, 2012

2011

Precision and the Conjunction Rule in Concurrent Separation Logic.

Electr. Notes Theor. Comput. Sci., 2011

Proving program termination.

Commun. ACM, 2011

Proving Stabilization of Biological Systems.

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2011

Making prophecies with decision predicates.

Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2011

Tractable Reasoning in a Fragment of Separation Logic.

Proceedings of the CONCUR 2011 - Concurrency Theory - 22nd International Conference, 2011

Temporal Property Verification as a Program Analysis Task.

Proceedings of the Computer Aided Verification - 23rd International Conference, 2011

SLAyer: Memory Safety for Systems-Level Code.

Proceedings of the Computer Aided Verification - 23rd International Conference, 2011

Advances in Proving Program Termination and Liveness.

Proceedings of the Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31, 2011

2010

Ranking Function Synthesis for Bit-Vector Relations.

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2010

2009

Summarization for termination: no return!

Formal Methods in System Design, 2009

Advances in Program Termination and Liveness.

Proceedings of the Verification, 2009

Proving that non-blocking algorithms don't block.

Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2009

Taming the Unbounded for Hardware Synthesis.

Proceedings of the Integrated Formal Methods, 7th International Conference, 2009

Finding heap-bounds for hardware synthesis.

Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, 2009

2008

Software engineering and formal methods.

Commun. ACM, 2008

Ranking Abstractions.

Proceedings of the Programming Languages and Systems, 2008

Scalable Shape Analysis for Systems Code.

Proceedings of the Computer Aided Verification, 20th International Conference, 2008

Proving Conditional Termination.

Proceedings of the Computer Aided Verification, 20th International Conference, 2008

2007

Verification of Boolean programs with unbounded thread creation.

Theor. Comput. Sci., 2007

Preface to Special Issue on Satisfiability Modulo Theories.

JSAT, 2007

Preface and Foreword.

Electr. Notes Theor. Comput. Sci., 2007

Shape Analysis by Graph Decomposition.

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

Automatically Proving Concurrent Programs Correct.

Proceedings of the Fifth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007), 2007

Proving Termination by Divergence.

Proceedings of the Fifth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007), 2007

Arithmetic Strengthening for Shape Analysis.

Proceedings of the Static Analysis, 14th International Symposium, 2007

Proving that programs eventually do something good.

Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2007

Variance analyses from invariance analyses.

Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2007

Thread-modular shape analysis.

Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, 2007

Proving thread termination.

Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, 2007

Bringing Hardware and Software Closer Together with Termination Analysis.

Proceedings of the 5th ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2007), May 30, 2007

07401 Abstracts Collection -- Deduction and Decision Procedures.

Proceedings of the Deduction and Decision Procedures, 30.09. - 05.10.2007, 2007

07401 Executive Summary -- Deduction and Decision Procedures.

Proceedings of the Deduction and Decision Procedures, 30.09. - 05.10.2007, 2007

Automatically Proving Program Termination.

Proceedings of the Computer Aided Verification, 19th International Conference, 2007

Shape Analysis for Composite Data Structures.

Proceedings of the Computer Aided Verification, 19th International Conference, 2007

Local Reasoning for Storable Locks and Threads.

Proceedings of the Programming Languages and Systems, 5th Asian Symposium, 2007

2006

Preface.

Electr. Notes Theor. Comput. Sci., 2006

Interprocedural Shape Analysis with Separated Heap Abstractions.

Proceedings of the Static Analysis, 13th International Symposium, 2006

Termination proofs for systems code.

Proceedings of the ACM SIGPLAN 2006 Conference on Programming Language Design and Implementation, 2006

Over-Approximating Boolean Programs with Unbounded Thread Creation.

Proceedings of the Formal Methods in Computer-Aided Design, 6th International Conference, 2006

Thorough static analysis of device drivers.

Proceedings of the 2006 EuroSys Conference, Leuven, Belgium, April 18-21, 2006, 2006

Repair of Boolean Programs with an Application to C.

Proceedings of the Computer Aided Verification, 18th International Conference, 2006

Terminator: Beyond Safety.

Proceedings of the Computer Aided Verification, 18th International Conference, 2006

Automatic Termination Proofs for Programs with Shape-Shifting Heaps.

Proceedings of the Computer Aided Verification, 18th International Conference, 2006

2005

Symbolic Model Checking for Asynchronous Boolean Programs.

Proceedings of the Model Checking Software, 2005

Abstraction Refinement for Termination.

Proceedings of the Static Analysis, 12th International Symposium, 2005

Using Stålmarck's Algorithm to Prove Inequalities.

Proceedings of the Formal Methods and Software Engineering, 2005

Predicate Abstraction via Symbolic Decision Procedures.

Proceedings of the Computer Aided Verification, 17th International Conference, 2005

Cogent: Accurate Theorem Proving for Program Verification.

Proceedings of the Computer Aided Verification, 17th International Conference, 2005

Finding Bugs in Device Drivers with Static Driver Verifier.

Proceedings of the 12th International Workshop on Abstract State Machines, 2005

2004

Refining Approximations in Software Predicate Abstraction.

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2004

Accurate Theorem Proving for Program Verification.

Proceedings of the Leveraging Applications of Formal Methods, 2004

Finding API usage rule violations in Windows device drivers using Static Driver Verifier.

Proceedings of the International Symposium on Leveraging Applications of Formal Methods, 2004

SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft.

Proceedings of the Integrated Formal Methods, 4th International Conference, 2004

Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement.

Proceedings of the Computer Aided Verification, 16th International Conference, 2004

2003

Design automation with mixtures of proof strategies for propositional logic.

IEEE Trans. on CAD of Integrated Circuits and Systems, 2003

A framework for superscalar microprocessor correctness statements.

STTT, 2003

SoftMC 2003: Workshop on Software Model Checking.

Electr. Notes Theor. Comput. Sci., 2003

A Symbolic Approach to Predicate Abstraction.

Proceedings of the Computer Aided Verification, 15th International Conference, 2003

2002

A proof engine approach to solving combinational design automation problems.

Proceedings of the 39th Design Automation Conference, 2002

2001

A Framework for Microprocessor Correctness Statements.

Proceedings of the Correct Hardware Design and Verification Methods, 2001

2000

Combining Stream-Based and State-Based Verification Techniques.

Proceedings of the Formal Methods in Computer-Aided Design, Third International Conference, 2000

1999

On Embedding a Microarchitectural Design Language within Haskell.

Proceedings of the fourth ACM SIGPLAN International Conference on Functional Programming (ICFP '99), 1999

Symbolic Simulation of Microprocessor Models using Type Classes in Haskell.

Proceedings of the Correct Hardware Design and Verification Methods, 1999

Formal Verification of Explicitly Parallel Microprocessors.

Proceedings of the Correct Hardware Design and Verification Methods, 1999

1998

Microprocessor Specification in Hawk.

Proceedings of the 1998 International Conference on Computer Languages, 1998

1997

Disposable Memo Functions (Extended Abstract).

Proceedings of the 1997 ACM SIGPLAN International Conference on Functional Programming (ICFP '97), 1997