Edit Profile (opens in new tab) Cook, Byron Compute Distance To: Compute Author ID: cook.byron Published as: Cook, Byron; Cook, B. Documents Indexed: 39 Publications since 2001 3 Contributions as Editor Co-Authors: 74 Co-Authors with 41 Joint Publications 1,291 Co-Co-Authors all top 5 Co-Authors 0 single-authored 10 Berdine, Josh 6 Kröning, Daniel 5 Gotsman, Alexey 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 Khazem, Kareem 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 Tasiran, Serdar 1 Tautschnig, Michael 1 Touili, Tayssir 1 Tuttle, Mark R. 1 Vafeiadis, Viktor 1 Varming, Carsten 1 Viswanathan, Deepa 1 Wies, Thomas 1 Worrell, James B. 1 Zhang, Lintao 1 Zuleger, Florian all top 5 Serials 4 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 42 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 37 Publications have been cited 261 times in 178 Documents Cited by ▼ Year ▼ Scalable shape analysis for systems code. Zbl 1155.68359Yang, Hongseok; Lee, Oukseh; Berdine, Josh; Calcagno, Cristiano; Cook, Byron; Distefano, Dino; O’Hearn, Peter 22 2008 Abstraction refinement for termination. Zbl 1141.68365Cook, Byron; Podelski, Andreas; Rybalchenko, Andrey 22 2005 Tractable reasoning in a fragment of separation logic. Zbl 1300.03017Cook, Byron; Haase, Christoph; Ouaknine, Joël; Parkinson, Matthew; Worrell, James 17 2011 Shape analysis for composite data structures. Zbl 1135.68372Berdine, Josh; Calcagno, Cristiano; Cook, Byron; Distefano, Dino; O’Hearn, Peter W.; Wies, Thomas; Yang, Hongseok 17 2007 Proving that non-blocking algorithms don’t block. Zbl 1315.68093Gotsman, Alexey; Cook, Byron; Parkinson, Matthew; Vafeiadis, Viktor 12 2009 Ranking function synthesis for bit-vector relations. Zbl 1284.68172Cook, Byron; Kroening, Daniel; Rümmer, Philipp; Wintersteiger, Christoph M. 11 2010 Local reasoning for storable locks and threads. Zbl 1137.68354Gotsman, Alexey; Berdine, Josh; Cook, Byron; Rinetzky, Noam; Sagiv, Mooly 11 2007 Proving conditional termination. Zbl 1155.68431Cook, Byron; Gulwani, Sumit; Lev-Ami, Tal; Rybalchenko, Andrey; Sagiv, Mooly 11 2008 Variance analyses from invariance analyses. Zbl 1295.68076Berdine, Josh; Chawdhary, Aziem; Cook, Byron; Distefano, Dino; O’Hearn, Peter 11 2007 Automatic termination proofs for programs with shape-shifting heaps. Zbl 1188.68109Berdine, Josh; Cook, Byron; Distefano, Dino; O’Hearn, Peter W. 10 2006 A symbolic approach to predicate abstraction. Zbl 1278.68181Lahiri, Shuvendu K.; Bryant, Randal E.; Cook, Byron 9 2003 Interprocedural shape analysis with separated heap abstractions. Zbl 1225.68072Gotsman, Alexey; Berdine, Josh; Cook, Byron 9 2006 Proving that programs eventually do something good. Zbl 1295.68083Cook, Byron; Gotsman, Alexey; Podelski, Andreas; Rybalchenko, Andrey; Vardi, Moshe Y. 9 2007 Zapato: Automatic theorem proving for predicate abstraction refinement. Zbl 1103.68604Ball, Thomas; Cook, Byron; Lahiri, Shuvendu K.; Zhang, Lintao 8 2004 On automation of \(\mathsf{CTL}^*\) verification for infinite-state systems. Zbl 1381.68154Cook, Byron; Khlaaf, Heidy; Piterman, Nir 7 2015 Ramsey versus lexicographic termination proving. Zbl 1381.68050Cook, Byron; See, Abigail; Zuleger, Florian 7 2013 Ranking abstractions. Zbl 1133.68317Chawdhary, Aziem; Cook, Byron; Gulwani, Sumit; Sagiv, Mooly; Yang, Hongseok 6 2008 Making prophecies with decision predicates. Zbl 1284.68389Cook, Byron; Koskinen, Eric 6 2011 Symbolic model checking for asynchronous Boolean programs. Zbl 1151.68367Cook, Byron; Kroening, Daniel; Sharygina, Natasha 5 2005 Arithmetic strengthening for shape analysis. Zbl 1211.68094Magill, Stephen; Berdine, Josh; Clarke, Edmund; Cook, Byron 5 2007 Verification of Boolean programs with unbounded thread creation. Zbl 1143.68043Cook, Byron; Kroening, Daniel; Sharygina, Natasha 5 2007 Proving stabilization of biological systems. Zbl 1318.92014Cook, Byron; Fisher, Jasmin; Krepska, Elzbieta; Piterman, Nir 4 2011 Refining approximations in software predicate abstraction. Zbl 1126.68344Ball, Thomas; Cook, Byron; Das, Satyaki; Rajamani, Sriram K. 4 2004 Ranking function synthesis for bit-vector relations. Zbl 1291.68138Cook, Byron; Kroening, Daniel; Rümmer, Philipp; Wintersteiger, Christoph M. 4 2013 Temporal property verification as a program analysis task. Zbl 1284.68171Cook, Byron; Koskinen, Eric; Vardi, Moshe 4 2012 Cogent: Accurate theorem proving for program verification. Zbl 1081.68673Cook, Byron; Kroening, Daniel; Sharygina, Natasha 4 2005 Predicate abstraction via symbolic decision procedures. Zbl 1081.68055Lahiri, Shuvendu K.; Ball, Thomas; Cook, Byron 4 2005 Summarization for termination: No return! Zbl 1185.68412Cook, Byron; Podelski, Andreas; Rybalchenko, Andrey 3 2009 Verifying increasingly expressive temporal logics for infinite-state systems. Zbl 1426.68166Cook, Byron; Khlaaf, Heidy; Piterman, Nir 3 2017 Repair of Boolean programs with an application to C. Zbl 1188.68188Griesmayer, Andreas; Bloem, Roderick; Cook, Byron 2 2006 Precision and the conjunction rule in concurrent separation logic. Zbl 1342.68085Gotsman, Alexey; Berdine, Josh; Cook, Byron 2 2011 Spatial interpolants. Zbl 1335.68040Albargouthi, Aws; Berdine, Josh; Cook, Byron; Kincaid, Zachary 2 2015 Stratified abstraction of access control policies. Zbl 1478.68029Backes, 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 1 2020 Computer aided verification. 22nd international conference, CAV 2010, Edinburgh, UK, July 15–19, 2010. Proceedings. Zbl 1193.68016 1 2010 Proving termination of nonlinear command sequences. Zbl 1298.68164Babić, Domagoj; Cook, Byron; Hu, Alan J.; Rakamarić, Zvonimir 1 2013 Predicate abstraction via symbolic decision procedures. Zbl 1128.03019Lahiri, Shuvendu Kumar; Ball, Thomas; Cook, Byron 1 2007 A framework for microprocessor correctness statements. Zbl 1002.68500Aagaard, Mark D.; Cook, Byron; Day, Nancy A.; Jones, Robert B. 1 2001 Stratified abstraction of access control policies. Zbl 1478.68029Backes, 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 1 2020 Verifying increasingly expressive temporal logics for infinite-state systems. Zbl 1426.68166Cook, Byron; Khlaaf, Heidy; Piterman, Nir 3 2017 On automation of \(\mathsf{CTL}^*\) verification for infinite-state systems. Zbl 1381.68154Cook, Byron; Khlaaf, Heidy; Piterman, Nir 7 2015 Spatial interpolants. Zbl 1335.68040Albargouthi, Aws; Berdine, Josh; Cook, Byron; Kincaid, Zachary 2 2015 Ramsey versus lexicographic termination proving. Zbl 1381.68050Cook, Byron; See, Abigail; Zuleger, Florian 7 2013 Ranking function synthesis for bit-vector relations. Zbl 1291.68138Cook, Byron; Kroening, Daniel; Rümmer, Philipp; Wintersteiger, Christoph M. 4 2013 Proving termination of nonlinear command sequences. Zbl 1298.68164Babić, Domagoj; Cook, Byron; Hu, Alan J.; Rakamarić, Zvonimir 1 2013 Temporal property verification as a program analysis task. Zbl 1284.68171Cook, Byron; Koskinen, Eric; Vardi, Moshe 4 2012 Tractable reasoning in a fragment of separation logic. Zbl 1300.03017Cook, Byron; Haase, Christoph; Ouaknine, Joël; Parkinson, Matthew; Worrell, James 17 2011 Making prophecies with decision predicates. Zbl 1284.68389Cook, Byron; Koskinen, Eric 6 2011 Proving stabilization of biological systems. Zbl 1318.92014Cook, Byron; Fisher, Jasmin; Krepska, Elzbieta; Piterman, Nir 4 2011 Precision and the conjunction rule in concurrent separation logic. Zbl 1342.68085Gotsman, Alexey; Berdine, Josh; Cook, Byron 2 2011 Ranking function synthesis for bit-vector relations. Zbl 1284.68172Cook, Byron; Kroening, Daniel; Rümmer, Philipp; Wintersteiger, Christoph M. 11 2010 Computer aided verification. 22nd international conference, CAV 2010, Edinburgh, UK, July 15–19, 2010. Proceedings. Zbl 1193.68016 1 2010 Proving that non-blocking algorithms don’t block. Zbl 1315.68093Gotsman, Alexey; Cook, Byron; Parkinson, Matthew; Vafeiadis, Viktor 12 2009 Summarization for termination: No return! Zbl 1185.68412Cook, Byron; Podelski, Andreas; Rybalchenko, Andrey 3 2009 Scalable shape analysis for systems code. Zbl 1155.68359Yang, Hongseok; Lee, Oukseh; Berdine, Josh; Calcagno, Cristiano; Cook, Byron; Distefano, Dino; O’Hearn, Peter 22 2008 Proving conditional termination. Zbl 1155.68431Cook, Byron; Gulwani, Sumit; Lev-Ami, Tal; Rybalchenko, Andrey; Sagiv, Mooly 11 2008 Ranking abstractions. Zbl 1133.68317Chawdhary, Aziem; Cook, Byron; Gulwani, Sumit; Sagiv, Mooly; Yang, Hongseok 6 2008 Shape analysis for composite data structures. Zbl 1135.68372Berdine, Josh; Calcagno, Cristiano; Cook, Byron; Distefano, Dino; O’Hearn, Peter W.; Wies, Thomas; Yang, Hongseok 17 2007 Local reasoning for storable locks and threads. Zbl 1137.68354Gotsman, Alexey; Berdine, Josh; Cook, Byron; Rinetzky, Noam; Sagiv, Mooly 11 2007 Variance analyses from invariance analyses. Zbl 1295.68076Berdine, Josh; Chawdhary, Aziem; Cook, Byron; Distefano, Dino; O’Hearn, Peter 11 2007 Proving that programs eventually do something good. Zbl 1295.68083Cook, Byron; Gotsman, Alexey; Podelski, Andreas; Rybalchenko, Andrey; Vardi, Moshe Y. 9 2007 Arithmetic strengthening for shape analysis. Zbl 1211.68094Magill, Stephen; Berdine, Josh; Clarke, Edmund; Cook, Byron 5 2007 Verification of Boolean programs with unbounded thread creation. Zbl 1143.68043Cook, Byron; Kroening, Daniel; Sharygina, Natasha 5 2007 Predicate abstraction via symbolic decision procedures. Zbl 1128.03019Lahiri, Shuvendu Kumar; Ball, Thomas; Cook, Byron 1 2007 Automatic termination proofs for programs with shape-shifting heaps. Zbl 1188.68109Berdine, Josh; Cook, Byron; Distefano, Dino; O’Hearn, Peter W. 10 2006 Interprocedural shape analysis with separated heap abstractions. Zbl 1225.68072Gotsman, Alexey; Berdine, Josh; Cook, Byron 9 2006 Repair of Boolean programs with an application to C. Zbl 1188.68188Griesmayer, Andreas; Bloem, Roderick; Cook, Byron 2 2006 Abstraction refinement for termination. Zbl 1141.68365Cook, Byron; Podelski, Andreas; Rybalchenko, Andrey 22 2005 Symbolic model checking for asynchronous Boolean programs. Zbl 1151.68367Cook, Byron; Kroening, Daniel; Sharygina, Natasha 5 2005 Cogent: Accurate theorem proving for program verification. Zbl 1081.68673Cook, Byron; Kroening, Daniel; Sharygina, Natasha 4 2005 Predicate abstraction via symbolic decision procedures. Zbl 1081.68055Lahiri, Shuvendu K.; Ball, Thomas; Cook, Byron 4 2005 Zapato: Automatic theorem proving for predicate abstraction refinement. Zbl 1103.68604Ball, Thomas; Cook, Byron; Lahiri, Shuvendu K.; Zhang, Lintao 8 2004 Refining approximations in software predicate abstraction. Zbl 1126.68344Ball, Thomas; Cook, Byron; Das, Satyaki; Rajamani, Sriram K. 4 2004 A symbolic approach to predicate abstraction. Zbl 1278.68181Lahiri, Shuvendu K.; Bryant, Randal E.; Cook, Byron 9 2003 A framework for microprocessor correctness statements. Zbl 1002.68500Aagaard, Mark D.; Cook, Byron; Day, Nancy A.; Jones, Robert B. 1 2001 all cited Publications top 5 cited Publications all top 5 Cited by 385 Authors 13 Kröning, Daniel 8 Cook, Byron 8 Demri, Stéphane P. 7 Cimatti, Alessandro 6 Giesl, Jürgen 6 Vojnar, Tomáš 5 Genaim, Samir 5 Griggio, Alberto 5 Iosif, Radu 5 Sharygina, Natasha 5 Wintersteiger, Christoph M. 4 Brockschmidt, Marc 4 Brotherston, James 4 Frohn, Florian 4 Hensel, Jera 4 Holík, Lukáš 4 Podelski, Andreas 4 Rogalewicz, Adam 4 Rybalchenko, Andrey 4 Sebastiani, Roberto 4 Ströder, Thomas 4 Zuleger, Florian 3 Albert, Elvira 3 Biere, Armin 3 Bouajjani, Ahmed 3 Bruttomesso, Roberto 3 Chin, Wei-Ngan 3 Deters, Morgan 3 Enea, Constantin 3 Fuhs, Carsten 3 Lengál, Ondřej 3 Lozes, Etienne 3 Martin-Martin, Enrique 3 Petersen, Rasmus Lerchedahl 3 Piterman, Nir 3 Qin, Shengchao 3 Schneider-Kamp, Peter 3 Sighireanu, Mihaela 3 Tonetta, Stefano 3 Tsitovich, Aliaksei 3 Wahl, Thomas 2 Appel, Andrew W. 2 Aschermann, Cornelius 2 Bagnara, Roberto 2 Birkedal, Lars 2 Bozga, Marius 2 Bozzano, Marco 2 Brochenin, Rémi 2 Chen, Taolue 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 Gardner, Philippa Anne 2 Gast, Holger 2 Ghardallou, Wided 2 Gupta, Aarti 2 Habermehl, Peter 2 He, Guanhua 2 Hobor, Aquinas 2 Hoenicke, Jochen 2 Jansen, Christina 2 Jobstmann, Barbara 2 Junttila, Tommi A. 2 Kaiser, Alexander D. 2 Kapur, Deepak 2 Kincaid, Zachary 2 Kobayashi, Naoki 2 Koskinen, Eric 2 Leavens, Gary T. 2 Magnago, Enrico 2 Mansutti, Alessio 2 Matheja, Christoph 2 McMillan, Kenneth L. 2 Mili, Ali 2 Noll, Thomas 2 O’Hearn, Peter W. 2 Otto, Carsten 2 Ouaknine, Joel O. 2 Pagel, Jens 2 Plücker, Martin 2 Pottier, François 2 Ranise, Silvio 2 Rival, Xavier 2 Rubio, Albert 2 Rümmer, Philipp 2 Sagiv, Mooly 2 Schellhorn, Gerhard 2 Tautschnig, Michael 2 van Rossum, Peter 2 von Essen, Christian 2 Weissenbacher, Georg 2 Worrell, James B. 2 Wu, Zhilin 2 Yang, Hongseok 2 Zaffanella, Enea 2 Zhao, Hengjun ...and 285 more Authors all top 5 Cited in 31 Serials 22 Formal Methods in System Design 11 Journal of Automated Reasoning 8 Theoretical Computer Science 8 Information and Computation 8 Formal Aspects of Computing 5 ACM Transactions on Computational Logic 4 Journal of Logical and Algebraic Methods in Programming 3 Annals of Mathematics and Artificial Intelligence 2 Artificial Intelligence 2 Journal of Computer and System Sciences 2 Programming and Computer Software 2 Annals of Pure and Applied Logic 2 Journal of Functional Programming 2 Theory of Computing Systems 2 Journal of the ACM 2 The Journal of Logic and Algebraic Programming 2 Computer Languages, Systems & Structures 1 Acta Informatica 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 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 9 Fields 175 Computer science (68-XX) 64 Mathematical logic and foundations (03-XX) 2 Biology and other natural sciences (92-XX) 1 Combinatorics (05-XX) 1 Category theory; homological algebra (18-XX) 1 Ordinary differential equations (34-XX) 1 Operations research, mathematical programming (90-XX) 1 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 1 Systems theory; control (93-XX) Citations by Year