BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Travelled to:
1 × Austria
1 × Canada
1 × Cyprus
1 × Denmark
1 × Hungary
1 × Italy
1 × Korea
1 × Poland
1 × Portugal
1 × Russia
1 × Spain
1 × The Netherlands
14 × USA
2 × Germany
4 × France
6 × United Kingdom
Collaborated with:
J.Berdine A.Rybalchenko A.Podelski E.Koskinen N.Piterman T.Ball A.Gotsman P.W.O'Hearn S.K.Lahiri M.Sagiv J.Launchbury S.Ishtiaq D.Distefano H.Khlaaf J.Fisher M.Y.Vardi D.Kröning C.Fuhs S.K.Rajamani H.Yang S.Gulwani A.Chawdhary M.Brockschmidt A.See F.Zuleger S.Magill A.Griesmayer R.Bloem N.Sharygina R.E.Bryant J.R.Lewis A.J.Hu C.Calcagno A.Albarghouthi Z.Kincaid E.Krepska P.Rümmer C.M.Wintersteiger M.J.Parkinson V.Vafeiadis E.M.Clarke D.Babic Z.Rakamaric L.Zhang V.Levin S.Das G.Andersson P.Bjesse Z.Hanna S.Tasiran A.S.Taylor C.Cockerton S.Bourton D.Benque H.Y.Chen K.Nimkar T.Lev-Ami R.Manevich G.Ramalingam B.A.Hall G.Juniwal K.Khazem D.Kroening M.Tautschnig M.R.Tuttle O.Lee T.Wies A.Chudnov N.Collins J.Dodds B.Huffman C.MacCárthaigh E.Mertens E.Mullen A.Tomb E.Westbrook J.Backes S.Bayless C.Dodge A.Gacek T.Kahsai B.Kocik E.Kotelnikov J.Kukovec S.McLaughlin J.R.0004 N.Rungta J.Sizemore M.A.Stalzer P.Srinivasan P.Subotic C.Varming B.Whaley
Talks about:
prove (14) termin (12) program (10) analysi (8) abstract (7) shape (7) system (6) predic (5) automat (4) biolog (4)

Person: Byron Cook

DBLP DBLP: Cook:Byron

Facilitated 3 volumes:

CAV 2010Ed
VMCAI 2007Ed
SMT 2006Ed

Contributed to:

CAV 20152015
ESOP 20152015
TACAS 20152015
CAV 20142014
TACAS 20142014
CAV 20132013
CHI 20132013
PLDI 20132013
TACAS 20132013
CAV 20122012
CADE 20112011
CAV 20112011
POPL 20112011
VMCAI 20112011
TACAS 20102010
IFM 20092009
POPL 20092009
VMCAI 20092009
CAV 20082008
ESOP 20082008
CAV 20072007
PLDI 20072007
POPL 20072007
SAS 20072007
SEFM 20072007
TACAS 20072007
CAV 20062006
PLDI 20062006
SAS 20062006
CAV 20052005
SAS 20052005
CAV 20042004
IFM 20042004
TACAS 20042004
CAV 20032003
DAC 20022002
ICFP 19991999
ICFP 19971997
CAV (1) 20182018
CAV (2) 20182018
CAV (2) 20192019

Wrote 51 papers:

CAV-2015-CookKP #automation #infinity #on the #verification
On Automation of CTL* Verification for Infinite-State Systems (BC, HK, NP), pp. 13–29.
ESOP-2015-AlbarghouthiBCK
Spatial Interpolants (AA, JB, BC, ZK), pp. 634–660.
TACAS-2015-CookKP #infinity
Fairness for Infinite-State Systems (BC, HK, NP), pp. 384–398.
CAV-2014-CookFHIJP #biology #modelling
Finding Instability in Biological Models (BC, JF, BAH, SI, GJ, NP), pp. 358–372.
TACAS-2014-ChenCFNO #proving #safety
Proving Nontermination via Safety (HYC, BC, CF, KN, PWO), pp. 156–171.
CAV-2013-BrockschmidtCF #proving #termination
Better Termination Proving through Cooperation (MB, BC, CF), pp. 413–429.
CHI-2013-TaylorPIFCCBB #biology #interface
At the interface of biology and computation (AST, NP, SI, JF, BC, CC, SB, DB), pp. 493–502.
PLDI-2013-CookK #nondeterminism #reasoning #source code
Reasoning about nondeterminism in programs (BC, EK), pp. 219–230.
TACAS-2013-CookSZ #proving #termination
Ramsey vs. Lexicographic Termination Proving (BC, AS, FZ), pp. 47–61.
CAV-2012-BenqueBCCFIPTV #biology #modelling #named #network #visual notation
Bma: Visual Tool for Modeling and Analyzing Biological Networks (DB, SB, CC, BC, JF, SI, NP, AST, MYV), pp. 686–692.
CADE-2011-Cook #liveness #proving #roadmap #termination
Advances in Proving Program Termination and Liveness (BC), p. 4.
CAV-2011-BerdineCI #memory management #named #safety
SLAyer: Memory Safety for Systems-Level Code (JB, BC, SI), pp. 178–183.
CAV-2011-CookKV #program analysis #verification
Temporal Property Verification as a Program Analysis Task (BC, EK, MYV), pp. 333–348.
POPL-2011-CookK
Making prophecies with decision predicates (BC, EK), pp. 399–410.
VMCAI-2011-CookFKP #biology #proving
Proving Stabilization of Biological Systems (BC, JF, EK, NP), pp. 134–149.
TACAS-2010-CookKRW #ranking #synthesis
Ranking Function Synthesis for Bit-Vector Relations (BC, DK, PR, CMW), pp. 236–250.
IFM-2009-Cook #bound #hardware #synthesis
Taming the Unbounded for Hardware Synthesis (BC), p. 39.
POPL-2009-GotsmanCPV #algorithm #proving
Proving that non-blocking algorithms don’t block (AG, BC, MJP, VV), pp. 16–28.
VMCAI-2009-Cook #liveness #roadmap #termination
Advances in Program Termination and Liveness (BC), p. 4.
CAV-2008-CookGLRS #proving #termination
Proving Conditional Termination (BC, SG, TLA, AR, MS), pp. 328–340.
CAV-2008-YangLBCCDO #analysis #scalability
Scalable Shape Analysis for Systems Code (HY, OL, JB, CC, BC, DD, PWO), pp. 385–398.
ESOP-2008-ChawdharyCGSY #abstraction #ranking
Ranking Abstractions (AC, BC, SG, MS, HY), pp. 148–162.
CAV-2007-BerdineCCDOWY #analysis #data type
Shape Analysis for Composite Data Structures (JB, CC, BC, DD, PWO, TW, HY), pp. 178–192.
CAV-2007-Cook #automation #proving #termination
Automatically Proving Program Termination (BC), p. 1.
PLDI-2007-CookPR #concurrent #proving #termination #thread
Proving thread termination (BC, AP, AR), pp. 320–330.
PLDI-2007-GotsmanBCS #analysis #thread
Thread-modular shape analysis (AG, JB, BC, MS), pp. 266–277.
POPL-2007-BerdineCCDO #analysis
Variance analyses from invariance analyses (JB, AC, BC, DD, PWO), pp. 211–224.
POPL-2007-CookGPRV #proving #source code
Proving that programs eventually do something good (BC, AG, AP, AR, MYV), pp. 265–276.
SAS-2007-MagillBCC #analysis
Arithmetic Strengthening for Shape Analysis (SM, JB, EMC, BC), pp. 419–436.
SEFM-2007-BabicHRC #proving #termination
Proving Termination by Divergence (DB, AJH, ZR, BC), pp. 93–102.
SEFM-2007-Cook #automation #concurrent #proving #source code
Automatically Proving Concurrent Programs Correct (BC), pp. 269–272.
TACAS-2007-ManevichBCRS #analysis #composition #graph
Shape Analysis by Graph Decomposition (RM, JB, BC, GR, MS), pp. 3–18.
CAV-2006-BerdineCDO #automation #proving #source code #termination
Automatic Termination Proofs for Programs with Shape-Shifting Heaps (JB, BC, DD, PWO), pp. 386–400.
CAV-2006-CookPR #named #safety
Terminator: Beyond Safety (BC, AP, AR), pp. 415–418.
CAV-2006-GriesmayerBC #c #source code
Repair of Boolean Programs with an Application to C (AG, RB, BC), pp. 358–371.
PLDI-2006-CookPR #proving #termination
Termination proofs for systems code (BC, AP, AR), pp. 415–426.
SAS-2006-GotsmanBC #abstraction #analysis #interprocedural
Interprocedural Shape Analysis with Separated Heap Abstractions (AG, JB, BC), pp. 240–260.
CAV-2005-CookKS #named #proving #theorem proving #verification
Cogent: Accurate Theorem Proving for Program Verification (BC, DK, NS), pp. 296–300.
CAV-2005-LahiriBC #abstraction
Predicate Abstraction via Symbolic Decision Procedures (SKL, TB, BC), pp. 24–38.
SAS-2005-CookPR #abstraction #refinement #termination
Abstraction Refinement for Termination (BC, AP, AR), pp. 87–101.
CAV-2004-BallCLZ #abstraction #automation #named #proving #refinement #theorem proving
Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement (TB, BC, SKL, LZ), pp. 457–461.
IFM-2004-BallCLR #formal method #verification
SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft (TB, BC, VL, SKR), pp. 1–20.
TACAS-2004-BallCDR #abstraction #approximate
Refining Approximations in Software Predicate Abstraction (TB, BC, SD, SKR), pp. 388–403.
CAV-2003-LahiriBC #abstraction #approach
A Symbolic Approach to Predicate Abstraction (SKL, REB, BC), pp. 141–153.
DAC-2002-AnderssonBCH #approach #automation #design #problem #proving
A proof engine approach to solving combinational design automation problems (GA, PB, BC, ZH), pp. 725–730.
ICFP-1999-LaunchburyLC #architecture #design #haskell #on the
On Embedding a Microarchitectural Design Language within Haskell (JL, JRL, BC), pp. 60–69.
ICFP-1997-CookL
Disposable Memo Functions (BC, JL), p. 310.
CAV-2018-Cook #reasoning #security #web #web service
Formal Reasoning About the Security of Amazon Web Services (BC), pp. 38–47.
CAV-2018-ChudnovCCDHMMMM #verification
Continuous Formal Verification of Amazon s2n (AC, NC, BC, JD, BH, CM, SM, EM, EM, ST, AT, EW), pp. 430–446.
CAV-2018-CookKKTTT #model checking
Model Checking Boot Code from AWS Data Centers (BC, KK, DK, ST, MT, MRT), pp. 467–486.
CAV-2019-BackesBCDGHKKKK #analysis #network #reachability
Reachability Analysis for AWS-Based Networks (JB, SB, BC, CD, AG, AJH, TK, BK, EK, JK, SM, JR0, NR, JS, MAS, PS, PS, CV, BW), pp. 231–241.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.