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: Cook:Byron
Facilitated 3 volumes:
Ed
Ed
EdContributed to:
2015
2015
2015201420142013
2013
201320132012
20112011
201120112010
20092009200920082008200720072007
2007
20072007200620062006200520052004200420042003
2002
19991997201820182019Wrote 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.