Edit Profile (opens in new tab) Cook, Byron Co-Author Distance Author ID: cook.byron Published as: Cook, Byron; Cook, B. Documents Indexed: 38 Publications since 2001 3 Contributions as Editor Co-Authors: 70 Co-Authors with 40 Joint Publications 1,335 Co-Co-Authors all top 5 Co-Authors 0 single-authored 10 Berdine, Josh 5 Gotsman, Alexey 5 Kröning, Daniel 4 Ball, Thomas 4 Distefano, Dino 4 Lahiri, Shuvendu Kumar 4 O’Hearn, Peter W. 4 Piterman, Nir 4 Podelski, Andreas 4 Rybalchenko, Andrey 4 Sagiv, Mooly 3 Khlaaf, Heidy 3 Sharygina, Natasha 3 Yang, Hongseok 2 Calcagno, Cristiano 2 Chawdhary, Aziem 2 Gulwani, Sumit 2 Koskinen, Eric 2 Parkinson, Matthew J. 2 Rümmer, Philipp 2 Vardi, Moshe Ya’akov 2 Wintersteiger, Christoph M. 1 Aagaard, Mark D. 1 Albargouthi, Aws 1 Babić, Domagoj 1 Backes, John 1 Berrueco, Ulises 1 Bloem, Roderick 1 Bray, Tyler 1 Brim, Daniel 1 Bryant, Randal E. 1 Clarke, Edmund Melson jun. 1 Das, Satyaki 1 Day, Nancy A. 1 Fisher, Jasmin 1 Gacek, Andrew 1 Griesmayer, Andreas 1 Haase, Christoph 1 Hu, Alan J. 1 Jhala, Ranjit 1 Jones, Robert B. 1 Kincaid, Zachary 1 Krepska, Elzbieta 1 Lee, Oukseh 1 Lev-Ami, Tal 1 Luckow, Kasper Søe 1 Magill, Stephen 1 Manevich, Roman 1 McLaughlin, Sean 1 Menon, Madhav 1 Ouaknine, Joel O. 1 Peebles, Daniel 1 Pugalia, Ujjwal 1 Rajamani, Sriram K. 1 Rakamarić, Zvonimir 1 Ramalingam, Ganesan 1 Rinetzky, Noam 1 Rungta, Neha 1 Schlesinger, Cole 1 Schodde, Adam 1 Sebastiani, Roberto 1 See, Abigail 1 Tanuku, Anvesh 1 Touili, Tayssir 1 Vafeiadis, Viktor 1 Varming, Carsten 1 Viswanathan, Deepa 1 Wies, Thomas 1 Worrell, James Benjamin 1 Zhang, Lintao 1 Zuleger, Florian all top 5 Serials 3 Formal Methods in System Design 2 Lecture Notes in Computer Science 1 Theoretical Computer Science 1 Formal Aspects of Computing 1 Journal of the ACM 1 Electronic Notes in Theoretical Computer Science 1 Logical Methods in Computer Science Fields 41 Computer science (68-XX) 11 Mathematical logic and foundations (03-XX) 3 General and overarching topics; collections (00-XX) 1 Biology and other natural sciences (92-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 39 Publications have been cited 374 times in 258 Documents Cited by ▼ Year ▼ Scalable shape analysis for systems code. Zbl 1155.68359 Yang, Hongseok; Lee, Oukseh; Berdine, Josh; Calcagno, Cristiano; Cook, Byron; Distefano, Dino; O’Hearn, Peter 32 2008 Shape analysis for composite data structures. Zbl 1135.68372 Berdine, Josh; Calcagno, Cristiano; Cook, Byron; Distefano, Dino; O’Hearn, Peter W.; Wies, Thomas; Yang, Hongseok 30 2007 Abstraction refinement for termination. Zbl 1141.68365 Cook, Byron; Podelski, Andreas; Rybalchenko, Andrey 28 2005 Tractable reasoning in a fragment of separation logic. Zbl 1300.03017 Cook, Byron; Haase, Christoph; Ouaknine, Joël; Parkinson, Matthew; Worrell, James 23 2011 Automatic termination proofs for programs with shape-shifting heaps. Zbl 1188.68109 Berdine, Josh; Cook, Byron; Distefano, Dino; O’Hearn, Peter W. 18 2006 Arithmetic strengthening for shape analysis. Zbl 1211.68094 Magill, Stephen; Berdine, Josh; Clarke, Edmund; Cook, Byron 15 2007 Local reasoning for storable locks and threads. Zbl 1137.68354 Gotsman, Alexey; Berdine, Josh; Cook, Byron; Rinetzky, Noam; Sagiv, Mooly 15 2007 Variance analyses from invariance analyses. Zbl 1295.68076 Berdine, Josh; Chawdhary, Aziem; Cook, Byron; Distefano, Dino; O’Hearn, Peter 15 2007 Proving that non-blocking algorithms don’t block. Zbl 1315.68093 Gotsman, Alexey; Cook, Byron; Parkinson, Matthew; Vafeiadis, Viktor 15 2009 Proving that programs eventually do something good. Zbl 1295.68083 Cook, Byron; Gotsman, Alexey; Podelski, Andreas; Rybalchenko, Andrey; Vardi, Moshe Y. 14 2007 Ranking function synthesis for bit-vector relations. Zbl 1284.68172 Cook, Byron; Kroening, Daniel; Rümmer, Philipp; Wintersteiger, Christoph M. 13 2010 Proving conditional termination. Zbl 1155.68431 Cook, Byron; Gulwani, Sumit; Lev-Ami, Tal; Rybalchenko, Andrey; Sagiv, Mooly 13 2008 Ramsey versus lexicographic termination proving. Zbl 1381.68050 Cook, Byron; See, Abigail; Zuleger, Florian 13 2013 Interprocedural shape analysis with separated heap abstractions. Zbl 1225.68072 Gotsman, Alexey; Berdine, Josh; Cook, Byron 13 2006 A symbolic approach to predicate abstraction. Zbl 1278.68181 Lahiri, Shuvendu K.; Bryant, Randal E.; Cook, Byron 12 2003 Zapato: Automatic theorem proving for predicate abstraction refinement. Zbl 1103.68604 Ball, Thomas; Cook, Byron; Lahiri, Shuvendu K.; Zhang, Lintao 10 2004 Making prophecies with decision predicates. Zbl 1284.68389 Cook, Byron; Koskinen, Eric 10 2011 Ranking abstractions. Zbl 1133.68317 Chawdhary, Aziem; Cook, Byron; Gulwani, Sumit; Sagiv, Mooly; Yang, Hongseok 8 2008 On automation of \(\mathsf{CTL}^*\) verification for infinite-state systems. Zbl 1381.68154 Cook, Byron; Khlaaf, Heidy; Piterman, Nir 7 2015 Cogent: Accurate theorem proving for program verification. Zbl 1081.68673 Cook, Byron; Kroening, Daniel; Sharygina, Natasha 6 2005 Verifying increasingly expressive temporal logics for infinite-state systems. Zbl 1426.68166 Cook, Byron; Khlaaf, Heidy; Piterman, Nir 5 2017 Refining approximations in software predicate abstraction. Zbl 1126.68344 Ball, Thomas; Cook, Byron; Das, Satyaki; Rajamani, Sriram K. 5 2004 Verification of Boolean programs with unbounded thread creation. Zbl 1143.68043 Cook, Byron; Kroening, Daniel; Sharygina, Natasha 5 2007 Temporal property verification as a program analysis task. Zbl 1284.68171 Cook, Byron; Koskinen, Eric; Vardi, Moshe 5 2012 Symbolic model checking for asynchronous Boolean programs. Zbl 1151.68367 Cook, Byron; Kroening, Daniel; Sharygina, Natasha 5 2005 Ranking function synthesis for bit-vector relations. Zbl 1291.68138 Cook, Byron; Kroening, Daniel; Rümmer, Philipp; Wintersteiger, Christoph M. 5 2013 Summarization for termination: No return! Zbl 1185.68412 Cook, Byron; Podelski, Andreas; Rybalchenko, Andrey 4 2009 Repair of Boolean programs with an application to C. Zbl 1188.68188 Griesmayer, Andreas; Bloem, Roderick; Cook, Byron 4 2006 Precision and the conjunction rule in concurrent separation logic. Zbl 1342.68085 Gotsman, Alexey; Berdine, Josh; Cook, Byron 4 2011 Proving stabilization of biological systems. Zbl 1318.92014 Cook, Byron; Fisher, Jasmin; Krepska, Elzbieta; Piterman, Nir 4 2011 Predicate abstraction via symbolic decision procedures. Zbl 1081.68055 Lahiri, Shuvendu K.; Ball, Thomas; Cook, Byron 4 2005 Spatial interpolants. Zbl 1335.68040 Albargouthi, Aws; Berdine, Josh; Cook, Byron; Kincaid, Zachary 3 2015 Predicate abstraction via symbolic decision procedures. Zbl 1128.03019 Lahiri, Shuvendu Kumar; Ball, Thomas; Cook, Byron 2 2007 Shape analysis by graph decomposition. Zbl 1186.68115 Manevich, R.; Berdine, J.; Cook, B.; Ramalingam, G.; Sagiv, M. 2 2007 Computer aided verification. 22nd international conference, CAV 2010, Edinburgh, UK, July 15–19, 2010. Proceedings. Zbl 1193.68016 2 2010 Stratified abstraction of access control policies. Zbl 1478.68029 Backes, John; Berrueco, Ulises; Bray, Tyler; Brim, Daniel; Cook, Byron; Gacek, Andrew; Jhala, Ranjit; Luckow, Kasper; McLaughlin, Sean; Menon, Madhav; Peebles, Daniel; Pugalia, Ujjwal; Rungta, Neha; Schlesinger, Cole; Schodde, Adam; Tanuku, Anvesh; Varming, Carsten; Viswanathan, Deepa 2 2020 Proving termination of nonlinear command sequences. Zbl 1298.68164 Babić, Domagoj; Cook, Byron; Hu, Alan J.; Rakamarić, Zvonimir 1 2013 A framework for microprocessor correctness statements. Zbl 1002.68500 Aagaard, Mark D.; Cook, Byron; Day, Nancy A.; Jones, Robert B. 1 2001 Fairness for infinite-state systems. Zbl 1420.68122 Cook, Byron; Khlaaf, Heidy; Piterman, Nir 1 2015 Stratified abstraction of access control policies. Zbl 1478.68029 Backes, John; Berrueco, Ulises; Bray, Tyler; Brim, Daniel; Cook, Byron; Gacek, Andrew; Jhala, Ranjit; Luckow, Kasper; McLaughlin, Sean; Menon, Madhav; Peebles, Daniel; Pugalia, Ujjwal; Rungta, Neha; Schlesinger, Cole; Schodde, Adam; Tanuku, Anvesh; Varming, Carsten; Viswanathan, Deepa 2 2020 Verifying increasingly expressive temporal logics for infinite-state systems. Zbl 1426.68166 Cook, Byron; Khlaaf, Heidy; Piterman, Nir 5 2017 On automation of \(\mathsf{CTL}^*\) verification for infinite-state systems. Zbl 1381.68154 Cook, Byron; Khlaaf, Heidy; Piterman, Nir 7 2015 Spatial interpolants. Zbl 1335.68040 Albargouthi, Aws; Berdine, Josh; Cook, Byron; Kincaid, Zachary 3 2015 Fairness for infinite-state systems. Zbl 1420.68122 Cook, Byron; Khlaaf, Heidy; Piterman, Nir 1 2015 Ramsey versus lexicographic termination proving. Zbl 1381.68050 Cook, Byron; See, Abigail; Zuleger, Florian 13 2013 Ranking function synthesis for bit-vector relations. Zbl 1291.68138 Cook, Byron; Kroening, Daniel; Rümmer, Philipp; Wintersteiger, Christoph M. 5 2013 Proving termination of nonlinear command sequences. Zbl 1298.68164 Babić, Domagoj; Cook, Byron; Hu, Alan J.; Rakamarić, Zvonimir 1 2013 Temporal property verification as a program analysis task. Zbl 1284.68171 Cook, Byron; Koskinen, Eric; Vardi, Moshe 5 2012 Tractable reasoning in a fragment of separation logic. Zbl 1300.03017 Cook, Byron; Haase, Christoph; Ouaknine, Joël; Parkinson, Matthew; Worrell, James 23 2011 Making prophecies with decision predicates. Zbl 1284.68389 Cook, Byron; Koskinen, Eric 10 2011 Precision and the conjunction rule in concurrent separation logic. Zbl 1342.68085 Gotsman, Alexey; Berdine, Josh; Cook, Byron 4 2011 Proving stabilization of biological systems. Zbl 1318.92014 Cook, Byron; Fisher, Jasmin; Krepska, Elzbieta; Piterman, Nir 4 2011 Ranking function synthesis for bit-vector relations. Zbl 1284.68172 Cook, Byron; Kroening, Daniel; Rümmer, Philipp; Wintersteiger, Christoph M. 13 2010 Computer aided verification. 22nd international conference, CAV 2010, Edinburgh, UK, July 15–19, 2010. Proceedings. Zbl 1193.68016 2 2010 Proving that non-blocking algorithms don’t block. Zbl 1315.68093 Gotsman, Alexey; Cook, Byron; Parkinson, Matthew; Vafeiadis, Viktor 15 2009 Summarization for termination: No return! Zbl 1185.68412 Cook, Byron; Podelski, Andreas; Rybalchenko, Andrey 4 2009 Scalable shape analysis for systems code. Zbl 1155.68359 Yang, Hongseok; Lee, Oukseh; Berdine, Josh; Calcagno, Cristiano; Cook, Byron; Distefano, Dino; O’Hearn, Peter 32 2008 Proving conditional termination. Zbl 1155.68431 Cook, Byron; Gulwani, Sumit; Lev-Ami, Tal; Rybalchenko, Andrey; Sagiv, Mooly 13 2008 Ranking abstractions. Zbl 1133.68317 Chawdhary, Aziem; Cook, Byron; Gulwani, Sumit; Sagiv, Mooly; Yang, Hongseok 8 2008 Shape analysis for composite data structures. Zbl 1135.68372 Berdine, Josh; Calcagno, Cristiano; Cook, Byron; Distefano, Dino; O’Hearn, Peter W.; Wies, Thomas; Yang, Hongseok 30 2007 Arithmetic strengthening for shape analysis. Zbl 1211.68094 Magill, Stephen; Berdine, Josh; Clarke, Edmund; Cook, Byron 15 2007 Local reasoning for storable locks and threads. Zbl 1137.68354 Gotsman, Alexey; Berdine, Josh; Cook, Byron; Rinetzky, Noam; Sagiv, Mooly 15 2007 Variance analyses from invariance analyses. Zbl 1295.68076 Berdine, Josh; Chawdhary, Aziem; Cook, Byron; Distefano, Dino; O’Hearn, Peter 15 2007 Proving that programs eventually do something good. Zbl 1295.68083 Cook, Byron; Gotsman, Alexey; Podelski, Andreas; Rybalchenko, Andrey; Vardi, Moshe Y. 14 2007 Verification of Boolean programs with unbounded thread creation. Zbl 1143.68043 Cook, Byron; Kroening, Daniel; Sharygina, Natasha 5 2007 Predicate abstraction via symbolic decision procedures. Zbl 1128.03019 Lahiri, Shuvendu Kumar; Ball, Thomas; Cook, Byron 2 2007 Shape analysis by graph decomposition. Zbl 1186.68115 Manevich, R.; Berdine, J.; Cook, B.; Ramalingam, G.; Sagiv, M. 2 2007 Automatic termination proofs for programs with shape-shifting heaps. Zbl 1188.68109 Berdine, Josh; Cook, Byron; Distefano, Dino; O’Hearn, Peter W. 18 2006 Interprocedural shape analysis with separated heap abstractions. Zbl 1225.68072 Gotsman, Alexey; Berdine, Josh; Cook, Byron 13 2006 Repair of Boolean programs with an application to C. Zbl 1188.68188 Griesmayer, Andreas; Bloem, Roderick; Cook, Byron 4 2006 Abstraction refinement for termination. Zbl 1141.68365 Cook, Byron; Podelski, Andreas; Rybalchenko, Andrey 28 2005 Cogent: Accurate theorem proving for program verification. Zbl 1081.68673 Cook, Byron; Kroening, Daniel; Sharygina, Natasha 6 2005 Symbolic model checking for asynchronous Boolean programs. Zbl 1151.68367 Cook, Byron; Kroening, Daniel; Sharygina, Natasha 5 2005 Predicate abstraction via symbolic decision procedures. Zbl 1081.68055 Lahiri, Shuvendu K.; Ball, Thomas; Cook, Byron 4 2005 Zapato: Automatic theorem proving for predicate abstraction refinement. Zbl 1103.68604 Ball, Thomas; Cook, Byron; Lahiri, Shuvendu K.; Zhang, Lintao 10 2004 Refining approximations in software predicate abstraction. Zbl 1126.68344 Ball, Thomas; Cook, Byron; Das, Satyaki; Rajamani, Sriram K. 5 2004 A symbolic approach to predicate abstraction. Zbl 1278.68181 Lahiri, Shuvendu K.; Bryant, Randal E.; Cook, Byron 12 2003 A framework for microprocessor correctness statements. Zbl 1002.68500 Aagaard, Mark D.; Cook, Byron; Day, Nancy A.; Jones, Robert B. 1 2001 all cited Publications top 5 cited Publications all top 5 Cited by 510 Authors 12 Cook, Byron 12 Kröning, Daniel 10 Cimatti, Alessandro 9 Demri, Stéphane P. 8 Podelski, Andreas 8 Rybalchenko, Andrey 7 Genaim, Samir 7 Giesl, Jürgen 7 Griggio, Alberto 6 Iosif, Radu 6 Vojnar, Tomáš 5 Brotherston, James 5 Gotsman, Alexey 5 Hensel, Jera 5 Koskinen, Eric 5 O’Hearn, Peter W. 5 Sharygina, Natasha 5 Wintersteiger, Christoph M. 4 Ben-Amram, Amir M. 4 Bouajjani, Ahmed 4 Brockschmidt, Marc 4 Chatterjee, Krishnendu 4 Frohn, Florian 4 Holík, Lukáš 4 Kobayashi, Naoki 4 Lozes, Etienne 4 Rival, Xavier 4 Rogalewicz, Adam 4 Sagiv, Mooly 4 Sebastiani, Roberto 4 Ströder, Thomas 4 Tonetta, Stefano 4 Yang, Hongseok 4 Zuleger, Florian 3 Albert, Elvira 3 Appel, Andrew W. 3 Bagnara, Roberto 3 Berdine, Josh 3 Biere, Armin 3 Birkedal, Lars 3 Brochenin, Rémi 3 Bruttomesso, Roberto 3 Calcagno, Cristiano 3 Chin, Wei-Ngan 3 Deters, Morgan 3 Distefano, Dino 3 Enea, Constantin 3 Feng, Xinyu 3 Fuhs, Carsten 3 Gardner, Philippa Anne 3 Gulwani, Sumit 3 Henzinger, Thomas A. 3 Jobstmann, Barbara 3 Kimura, Daisuke 3 Kincaid, Zachary 3 Lengál, Ondřej 3 Magnago, Enrico 3 Martin-Martin, Enrique 3 Matheja, Christoph 3 Noll, Thomas 3 Novotný, Petr 3 Petersen, Rasmus Lerchedahl 3 Piterman, Nir 3 Qin, Shengchao 3 Schneider-Kamp, Peter 3 Sighireanu, Mihaela 3 Tatsuta, Makoto 3 Tsitovich, Aliaksei 3 Vafeiadis, Viktor 3 Wahl, Thomas 3 Zaffanella, Enea 2 Abdulla, Parosh Aziz 2 Aschermann, Cornelius 2 Beyene, Tewodros A. 2 Bloem, Roderick 2 Bouissou, Olivier 2 Bozga, Marius 2 Bozzano, Marco 2 Černý, Pavol 2 Chang, Bor-Yuh Evan 2 Chen, Taolue 2 Cousot, Patrick 2 Cousot, Radhia 2 de Moura, Leonardo 2 Donaldson, Alastair F. 2 Dragoi, Cezara 2 Ernst, Gidon 2 Falke, Stephan 2 Fisher, Jasmin 2 Flores-Montoya, Antonio 2 Gast, Holger 2 Ghardallou, Wided 2 Gupta, Aarti 2 Habermehl, Peter 2 He, Guanhua 2 Hill, Patricia M. 2 Hobor, Aquinas 2 Hoenicke, Jochen 2 Hu, Alan J. 2 Hurlin, Clément ...and 410 more Authors all top 5 Cited in 32 Serials 22 Formal Methods in System Design 13 Journal of Automated Reasoning 10 Theoretical Computer Science 9 Information and Computation 8 Formal Aspects of Computing 5 ACM Transactions on Computational Logic 4 Journal of Logical and Algebraic Methods in Programming 3 Journal of Functional Programming 3 Annals of Mathematics and Artificial Intelligence 2 Acta Informatica 2 Artificial Intelligence 2 Journal of Computer and System Sciences 2 Programming and Computer Software 2 Annals of Pure and Applied Logic 2 Theory of Computing Systems 2 Journal of the ACM 2 The Journal of Logic and Algebraic Programming 2 Computer Languages, Systems & Structures 1 Information Processing Letters 1 Science of Computer Programming 1 Journal of Symbolic Computation 1 International Journal of Parallel Programming 1 Real-Time Systems 1 Journal of Applied Non-Classical Logics 1 The Journal of Artificial Intelligence Research (JAIR) 1 Fundamenta Informaticae 1 Journal of Systems Science and Complexity 1 Sādhanā 1 ACM Journal of Experimental Algorithmics 1 Logical Methods in Computer Science 1 Science China. Information Sciences 1 Frontiers of Computer Science all top 5 Cited in 11 Fields 253 Computer science (68-XX) 96 Mathematical logic and foundations (03-XX) 3 Systems theory; control (93-XX) 2 Operations research, mathematical programming (90-XX) 2 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 2 Biology and other natural sciences (92-XX) 1 Combinatorics (05-XX) 1 Number theory (11-XX) 1 Category theory; homological algebra (18-XX) 1 Ordinary differential equations (34-XX) 1 Probability theory and stochastic processes (60-XX) Citations by Year