Edit Profile (opens in new tab) Sharygina, Natasha Co-Author Distance Author ID: sharygina.natasha Published as: Sharygina, Natasha External Links: ORCID Documents Indexed: 51 Publications since 2001 3 Contributions as Editor Software Indexed: 15 Packages referenced 166 times in 120 Documents Co-Authors: 46 Co-Authors with 54 Joint Publications 1,057 Co-Co-Authors all top 5 Co-Authors 0 single-authored 14 Hyvärinen, Antti E. J. 11 Fedyukovich, Grigory 9 Kröning, Daniel 8 Blicha, Martin 8 Clarke, Edmund Melson jun. 6 Alberti, Francesco 6 Chaki, Sagar 6 Ghilardi, Silvio 5 Asadi, Sepideh 5 Marescotti, Matteo 5 Sinha, Nishant 4 Bruttomesso, Roberto 4 Chockler, Hana 4 Rollini, Simone Fulvio 4 Tsitovich, Aliaksei 3 Alt, Leonardo S. 3 Cook, Byron 3 Even-Mendoza, Karine 3 Gurfinkel, Arie 3 Ouaknine, Joel O. 3 Wintersteiger, Christoph M. 2 Britikov, Konstantin 2 Browne, James C. 2 Kofroň, Jan 2 Ranise, Silvio 2 Sankaranarayanan, Sriram 2 Tonetta, Stefano 2 Veith, Helmut 2 Yorav, Karen 1 Barone-Adesi, Katerina 1 Braghin, Chiara 1 Eugster, Patrick Th. 1 Grumberg, Orna 1 Ivers, James 1 Jančík, Pavel 1 Konnov, Igor Vladimirovich 1 Kukovec, Jure 1 Kurshan, Robert P. 1 Otoni, Rodrigo 1 Peled, Doron A. 1 Sadigova, Parvin 1 Šerý, Ondřej 1 Seshia, Sanjit Arunkumar 1 Touili, Tayssir 1 Tripakis, Stavros 1 Wallnau, Kurt C. Serials 8 Formal Methods in System Design 3 Lecture Notes in Computer Science 2 Formal Aspects of Computing 1 Theoretical Computer Science 1 Journal of Automated Reasoning Fields 54 Computer science (68-XX) 12 Mathematical logic and foundations (03-XX) 3 General and overarching topics; collections (00-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 46 Publications have been cited 297 times in 198 Documents Cited by ▼ Year ▼ SATABS: SAT-based predicate abstraction for ANSI-C. Zbl 1087.68586 Clarke, Edmund; Kroening, Daniel; Sharygina, Natasha; Yorav, Karen 25 2005 Lazy abstraction with interpolants for arrays. Zbl 1352.68141 Alberti, Francesco; Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio; Sharygina, Natasha 22 2012 Predicate abstraction of ANSI-C programs using SAT. Zbl 1090.68022 Clarke, Edmund; Kroening, Daniel; Sharygina, Natasha; Yorav, Karen 18 2004 State/event-based software model checking. Zbl 1196.68129 Chaki, Sagar; Clarke, Edmund M.; Ouaknine, Joël; Sharygina, Natasha; Sinha, Nishant 16 2004 OpenSMT2: an SMT solver for multi-core and cloud computing. Zbl 1475.68438 Hyvärinen, Antti E. J.; Marescotti, Matteo; Alt, Leonardo; Sharygina, Natasha 14 2016 Booster: an acceleration-based verification framework for array programs. Zbl 1448.68284 Alberti, Francesco; Ghilardi, Silvio; Sharygina, Natasha 12 2014 Transition power abstractions for deep counterexample detection. Zbl 1547.68412 Blicha, Martin; Fedyukovich, Grigory; Hyvärinen, Antti E. J.; Sharygina, Natasha 10 2022 Computer aided verification. 25th international conference, CAV 2013, Saint Petersburg, Russia, July 13–19, 2013. Proceedings. Zbl 1268.68032 9 2013 Resolution proof transformation for compression and interpolation. Zbl 1317.68123 Rollini, Simone Fulvio; Bruttomesso, Roberto; Sharygina, Natasha; Tsitovich, Aliaksei 9 2014 PeRIPLO: a framework for producing effective interpolants in SAT-based software verification. Zbl 1407.68303 Rollini, Simone Fulvio; Alt, Leonardo; Fedyukovich, Grigory; Hyvärinen, Antti E. J.; Sharygina, Natasha 9 2013 Concurrent software verification with states, events, and deadlocks. Zbl 1103.68609 Chaki, Sagar; Clarke, Edmund; Ouaknine, Joël; Sharygina, Natasha; Sinha, Nishant 8 2005 Decision procedures for flat array properties. Zbl 1356.03049 Alberti, Francesco; Ghilardi, Silvio; Sharygina, Natasha 8 2015 Decomposing Farkas interpolants. Zbl 1527.68126 Blicha, Martin; Hyvärinen, Antti E. J.; Kofroň, Jan; Sharygina, Natasha 8 2019 An extension of lazy abstraction with interpolation for programs with arrays. Zbl 1317.68107 Alberti, Francesco; Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio; Sharygina, Natasha 7 2014 An efficient and flexible approach to resolution proof reduction. Zbl 1325.68215 Rollini, Simone Fulvio; Bruttomesso, Roberto; Sharygina, Natasha 7 2011 Verification of Boolean programs with unbounded thread creation. Zbl 1143.68043 Cook, Byron; Kroening, Daniel; Sharygina, Natasha 6 2007 Automated discovery of simulation between programs. Zbl 1471.68061 Fedyukovich, Grigory; Gurfinkel, Arie; Sharygina, Natasha 6 2015 Loop summarization and termination analysis. Zbl 1315.68106 Tsitovich, Aliaksei; Sharygina, Natasha; Wintersteiger, Christoph M.; Kroening, Daniel 6 2011 Dynamic component substitutability analysis. Zbl 1120.68421 Sharygina, Natasha; Chaki, Sagar; Clarke, Edmund; Sinha, Nishant 6 2005 Cogent: Accurate theorem proving for program verification. Zbl 1081.68673 Cook, Byron; Kroening, Daniel; Sharygina, Natasha 6 2005 State/event software verification for branching-time specifications. Zbl 1137.68432 Chaki, Sagar; Clarke, Edmund; Grumberg, Orna; Ouaknine, Joël; Sharygina, Natasha; Touili, Tayssir; Veith, Helmut 5 2005 Symbolic model checking for asynchronous Boolean programs. Zbl 1151.68367 Cook, Byron; Kroening, Daniel; Sharygina, Natasha 5 2005 Approximating predicate images for bit-vector logic. Zbl 1180.68175 Kroening, Daniel; Sharygina, Natasha 5 2006 eVolCheck: incremental upgrade checker for C. Zbl 1381.68159 Fedyukovich, Grigory; Sery, Ondrej; Sharygina, Natasha 5 2013 Interpolation properties and SAT-based model checking. Zbl 1410.68229 Gurfinkel, Arie; Rollini, Simone Fulvio; Sharygina, Natasha 5 2013 Modeling for verification. Zbl 1392.68264 Seshia, Sanjit A.; Sharygina, Natasha; Tripakis, Stavros 5 2018 Property directed equivalence via abstract simulation. Zbl 1411.68065 Fedyukovich, Grigory; Gurfinkel, Arie; Sharygina, Natasha 5 2016 Function summarization modulo theories. Zbl 1415.68141 Asadi, Sepideh; Blicha, Martin; Fedyukovich, Grigory; Hyvärinen, Antti; Even-Mendoza, Karine; Sharygina, Natasha; Chockler, Hana 5 2018 Loop summarization using abstract transformers. Zbl 1183.68377 Kroening, Daniel; Sharygina, Natasha; Tonetta, Stefano; Tsitovich, Aliaksei; Wintersteiger, Christoph M. 5 2008 Definability of accelerated relations in a theory of arrays and its applications. Zbl 1397.68121 Alberti, Francesco; Ghilardi, Silvio; Sharygina, Natasha 5 2013 Verification of evolving software via component substitutability analysis. Zbl 1147.68047 Chaki, Sagar; Clarke, Edmund; Sharygina, Natasha; Sinha, Nishant 4 2008 Tools and algorithms for the construction and analysis of systems. 29th international conference, TACAS 2023, held as part of the European joint conferences on theory and practice of software, ETAPS 2023, Paris, France, April 22–27, 2023. Proceedings. Part II. Zbl 1533.68007 4 2023 A model checking-based approach for security policy verification of mobile systems. Zbl 1242.68153 Braghin, Chiara; Sharygina, Natasha; Barone-Adesi, Katerina 3 2011 Loop summarization using state and transition invariants. Zbl 1291.68262 Kroening, Daniel; Sharygina, Natasha; Tonetta, Stefano; Tsitovich, Aliaksei; Wintersteiger, Christoph M. 3 2013 A cooperative parallelization approach for property-directed \(k\)-induction. Zbl 1544.68086 Blicha, Martin; Hyvärinen, Antti E. J.; Marescotti, Matteo; Sharygina, Natasha 3 2020 SMTS: distributed, visualized constraint solving. Zbl 1415.68197 Marescotti, Matteo; Hyvärinen, Antti E. J.; Sharygina, Natasha 3 2018 The ComFoRT reasoning framework. Zbl 1081.68613 Chaki, Sagar; Ivers, James; Sharygina, Natasha; Wallnau, Kurt 3 2005 Search-space partitioning for parallelizing SMT solvers. Zbl 1471.68244 Hyvärinen, Antti E. J.; Marescotti, Matteo; Sharygina, Natasha 2 2015 The Golem Horn solver. Zbl 1545.68134 Blicha, Martin; Britikov, Konstantin; Sharygina, Natasha 2 2023 Farkas-based tree interpolation. Zbl 1474.68321 Asadi, Sepideh; Blicha, Martin; Hyvärinen, Antti; Fedyukovich, Grigory; Sharygina, Natasha 2 2020 Program compatibility approaches. Zbl 1196.68044 Clarke, Edmund; Sharygina, Natasha; Sinha, Nishant 1 2006 Theory refinement for program verification. Zbl 1496.68191 Hyvärinen, Antti E. J.; Asadi, Sepideh; Even-Mendoza, Karine; Fedyukovich, Grigory; Chockler, Hana; Sharygina, Natasha 1 2017 A combined testing and verification approach for software reliability. Zbl 0977.68572 Sharygina, Natasha; Peled, Doron 1 2001 A formal object-oriented analysis for software reliability: design for verification. Zbl 0977.68831 Sharygina, Natasha; Browne, James C.; Kurshan, Robert P. 1 2001 Tools and algorithms for the construction and analysis of systems. 29th international conference, TACAS 2023, held as part of the European joint conferences on theory and practice of software, ETAPS 2023, Paris, France, April 22–27, 2023. Proceedings. Part I. Zbl 1525.68003 1 2023 SMT-based verification of program changes through summary repair. Zbl 1552.68156 Asadi, Sepideh; Blicha, Martin; Hyvärinen, Antti E. J.; Fedyukovich, Grigory; Sharygina, Natasha 1 2022 Tools and algorithms for the construction and analysis of systems. 29th international conference, TACAS 2023, held as part of the European joint conferences on theory and practice of software, ETAPS 2023, Paris, France, April 22–27, 2023. Proceedings. Part II. Zbl 1533.68007 4 2023 The Golem Horn solver. Zbl 1545.68134 Blicha, Martin; Britikov, Konstantin; Sharygina, Natasha 2 2023 Tools and algorithms for the construction and analysis of systems. 29th international conference, TACAS 2023, held as part of the European joint conferences on theory and practice of software, ETAPS 2023, Paris, France, April 22–27, 2023. Proceedings. Part I. Zbl 1525.68003 1 2023 Transition power abstractions for deep counterexample detection. Zbl 1547.68412 Blicha, Martin; Fedyukovich, Grigory; Hyvärinen, Antti E. J.; Sharygina, Natasha 10 2022 SMT-based verification of program changes through summary repair. Zbl 1552.68156 Asadi, Sepideh; Blicha, Martin; Hyvärinen, Antti E. J.; Fedyukovich, Grigory; Sharygina, Natasha 1 2022 A cooperative parallelization approach for property-directed \(k\)-induction. Zbl 1544.68086 Blicha, Martin; Hyvärinen, Antti E. J.; Marescotti, Matteo; Sharygina, Natasha 3 2020 Farkas-based tree interpolation. Zbl 1474.68321 Asadi, Sepideh; Blicha, Martin; Hyvärinen, Antti; Fedyukovich, Grigory; Sharygina, Natasha 2 2020 Decomposing Farkas interpolants. Zbl 1527.68126 Blicha, Martin; Hyvärinen, Antti E. J.; Kofroň, Jan; Sharygina, Natasha 8 2019 Modeling for verification. Zbl 1392.68264 Seshia, Sanjit A.; Sharygina, Natasha; Tripakis, Stavros 5 2018 Function summarization modulo theories. Zbl 1415.68141 Asadi, Sepideh; Blicha, Martin; Fedyukovich, Grigory; Hyvärinen, Antti; Even-Mendoza, Karine; Sharygina, Natasha; Chockler, Hana 5 2018 SMTS: distributed, visualized constraint solving. Zbl 1415.68197 Marescotti, Matteo; Hyvärinen, Antti E. J.; Sharygina, Natasha 3 2018 Theory refinement for program verification. Zbl 1496.68191 Hyvärinen, Antti E. J.; Asadi, Sepideh; Even-Mendoza, Karine; Fedyukovich, Grigory; Chockler, Hana; Sharygina, Natasha 1 2017 OpenSMT2: an SMT solver for multi-core and cloud computing. Zbl 1475.68438 Hyvärinen, Antti E. J.; Marescotti, Matteo; Alt, Leonardo; Sharygina, Natasha 14 2016 Property directed equivalence via abstract simulation. Zbl 1411.68065 Fedyukovich, Grigory; Gurfinkel, Arie; Sharygina, Natasha 5 2016 Decision procedures for flat array properties. Zbl 1356.03049 Alberti, Francesco; Ghilardi, Silvio; Sharygina, Natasha 8 2015 Automated discovery of simulation between programs. Zbl 1471.68061 Fedyukovich, Grigory; Gurfinkel, Arie; Sharygina, Natasha 6 2015 Search-space partitioning for parallelizing SMT solvers. Zbl 1471.68244 Hyvärinen, Antti E. J.; Marescotti, Matteo; Sharygina, Natasha 2 2015 Booster: an acceleration-based verification framework for array programs. Zbl 1448.68284 Alberti, Francesco; Ghilardi, Silvio; Sharygina, Natasha 12 2014 Resolution proof transformation for compression and interpolation. Zbl 1317.68123 Rollini, Simone Fulvio; Bruttomesso, Roberto; Sharygina, Natasha; Tsitovich, Aliaksei 9 2014 An extension of lazy abstraction with interpolation for programs with arrays. Zbl 1317.68107 Alberti, Francesco; Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio; Sharygina, Natasha 7 2014 Computer aided verification. 25th international conference, CAV 2013, Saint Petersburg, Russia, July 13–19, 2013. Proceedings. Zbl 1268.68032 9 2013 PeRIPLO: a framework for producing effective interpolants in SAT-based software verification. Zbl 1407.68303 Rollini, Simone Fulvio; Alt, Leonardo; Fedyukovich, Grigory; Hyvärinen, Antti E. J.; Sharygina, Natasha 9 2013 eVolCheck: incremental upgrade checker for C. Zbl 1381.68159 Fedyukovich, Grigory; Sery, Ondrej; Sharygina, Natasha 5 2013 Interpolation properties and SAT-based model checking. Zbl 1410.68229 Gurfinkel, Arie; Rollini, Simone Fulvio; Sharygina, Natasha 5 2013 Definability of accelerated relations in a theory of arrays and its applications. Zbl 1397.68121 Alberti, Francesco; Ghilardi, Silvio; Sharygina, Natasha 5 2013 Loop summarization using state and transition invariants. Zbl 1291.68262 Kroening, Daniel; Sharygina, Natasha; Tonetta, Stefano; Tsitovich, Aliaksei; Wintersteiger, Christoph M. 3 2013 Lazy abstraction with interpolants for arrays. Zbl 1352.68141 Alberti, Francesco; Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio; Sharygina, Natasha 22 2012 An efficient and flexible approach to resolution proof reduction. Zbl 1325.68215 Rollini, Simone Fulvio; Bruttomesso, Roberto; Sharygina, Natasha 7 2011 Loop summarization and termination analysis. Zbl 1315.68106 Tsitovich, Aliaksei; Sharygina, Natasha; Wintersteiger, Christoph M.; Kroening, Daniel 6 2011 A model checking-based approach for security policy verification of mobile systems. Zbl 1242.68153 Braghin, Chiara; Sharygina, Natasha; Barone-Adesi, Katerina 3 2011 Loop summarization using abstract transformers. Zbl 1183.68377 Kroening, Daniel; Sharygina, Natasha; Tonetta, Stefano; Tsitovich, Aliaksei; Wintersteiger, Christoph M. 5 2008 Verification of evolving software via component substitutability analysis. Zbl 1147.68047 Chaki, Sagar; Clarke, Edmund; Sharygina, Natasha; Sinha, Nishant 4 2008 Verification of Boolean programs with unbounded thread creation. Zbl 1143.68043 Cook, Byron; Kroening, Daniel; Sharygina, Natasha 6 2007 Approximating predicate images for bit-vector logic. Zbl 1180.68175 Kroening, Daniel; Sharygina, Natasha 5 2006 Program compatibility approaches. Zbl 1196.68044 Clarke, Edmund; Sharygina, Natasha; Sinha, Nishant 1 2006 SATABS: SAT-based predicate abstraction for ANSI-C. Zbl 1087.68586 Clarke, Edmund; Kroening, Daniel; Sharygina, Natasha; Yorav, Karen 25 2005 Concurrent software verification with states, events, and deadlocks. Zbl 1103.68609 Chaki, Sagar; Clarke, Edmund; Ouaknine, Joël; Sharygina, Natasha; Sinha, Nishant 8 2005 Dynamic component substitutability analysis. Zbl 1120.68421 Sharygina, Natasha; Chaki, Sagar; Clarke, Edmund; Sinha, Nishant 6 2005 Cogent: Accurate theorem proving for program verification. Zbl 1081.68673 Cook, Byron; Kroening, Daniel; Sharygina, Natasha 6 2005 State/event software verification for branching-time specifications. Zbl 1137.68432 Chaki, Sagar; Clarke, Edmund; Grumberg, Orna; Ouaknine, Joël; Sharygina, Natasha; Touili, Tayssir; Veith, Helmut 5 2005 Symbolic model checking for asynchronous Boolean programs. Zbl 1151.68367 Cook, Byron; Kroening, Daniel; Sharygina, Natasha 5 2005 The ComFoRT reasoning framework. Zbl 1081.68613 Chaki, Sagar; Ivers, James; Sharygina, Natasha; Wallnau, Kurt 3 2005 Predicate abstraction of ANSI-C programs using SAT. Zbl 1090.68022 Clarke, Edmund; Kroening, Daniel; Sharygina, Natasha; Yorav, Karen 18 2004 State/event-based software model checking. Zbl 1196.68129 Chaki, Sagar; Clarke, Edmund M.; Ouaknine, Joël; Sharygina, Natasha; Sinha, Nishant 16 2004 A combined testing and verification approach for software reliability. Zbl 0977.68572 Sharygina, Natasha; Peled, Doron 1 2001 A formal object-oriented analysis for software reliability: design for verification. Zbl 0977.68831 Sharygina, Natasha; Browne, James C.; Kurshan, Robert P. 1 2001 all cited Publications top 5 cited Publications all top 5 Cited by 431 Authors 19 Sharygina, Natasha 13 Kröning, Daniel 10 Fedyukovich, Grigory 9 Ghilardi, Silvio 8 Rümmer, Philipp 7 Hyvärinen, Antti E. J. 6 Blicha, Martin 5 Clarke, Edmund Melson jun. 5 De Angelis, Emanuele 5 Kuncak, Viktor 4 Alberti, Francesco 4 Barrett, Clark W. 4 Bruttomesso, Roberto 4 Gupta, Ashutosh 4 Rybalchenko, Andrey 4 Tsitovich, Aliaksei 4 Weissenbacher, Georg 4 Wintersteiger, Christoph M. 3 Asadi, Sepideh 3 Beneš, Nikola 3 Černá, Ivana 3 Chaki, Sagar 3 Cook, Byron 3 Dong, JinSong 3 Farzan, Azadeh 3 Fioravanti, Fabio 3 Frohn, Florian 3 Gallagher, John P. 3 Giesl, Jürgen 3 Hoenicke, Jochen 3 Kincaid, Zachary 3 Liu, Yang 3 Martí-Oliet, Narciso 3 Martín, Óscar 3 Pagani, Elena 3 Pettorossi, Alberto 3 Podelski, Andreas 3 Proietti, Maurizio 3 Shoham, Sharon 3 Sun, Jun 3 Verdejo, Alberto 3 Wahl, Thomas 2 Alt, Leonardo S. 2 Amilon, Jesper 2 Avni, Guy 2 Beyer, Dirk 2 Biere, Armin 2 Brim, Luboš 2 Britikov, Konstantin 2 Brockschmidt, Marc 2 Chakraborty, Supratik 2 Chechik, Marsha 2 Donaldson, Alastair F. 2 Esen, Zafer 2 Ganty, Pierre 2 Ghorpade, Pranav 2 Gianola, Alessandro 2 Griggio, Alberto 2 Grumberg, Orna 2 Guha, Shibashis 2 Gupta, Aarti 2 Gurfinkel, Arie 2 Gurov, Dilian 2 Hari Govind, V. K. 2 Henzinger, Thomas A. 2 Hermenegildo, Manuel V. 2 Heule, Marijn J. H. 2 Irfan, Ahmed 2 Jha, Somesh 2 Kafle, Bishoksan 2 Kaiser, Alexander D. 2 Kofroň, Jan 2 Koskinen, Eric 2 Kwiatkowska, Marta Z. 2 Lidström, Christian 2 Madhusudan, Parthasarathy 2 Majumdar, Rupak 2 Mann, Makai 2 Marescotti, Matteo 2 McMillan, Kenneth L. 2 Meseguer Guaita, José 2 Padon, Oded 2 Peuter, Dennis 2 Pnueli, Amir 2 Rakamarić, Zvonimir 2 Ranise, Silvio 2 Raya, Rodrigo 2 Reynolds, Andrew 2 Roscoe, Andrew William 2 Sochor, Jiri 2 Sofronie-Stokkermans, Viorica 2 Tinelli, Cesare 2 Tonetta, Stefano 2 Totla, Nishant 2 Unadkat, Divyesh 2 Vařeková, Pavlina 2 Vojnar, Tomáš 2 Wendler, Philipp 2 Wies, Thomas 2 Woltzenlogel Paleo, Bruno ...and 331 more Authors all top 5 Cited in 27 Serials 31 Formal Methods in System Design 14 Journal of Automated Reasoning 11 Formal Aspects of Computing 8 Theory and Practice of Logic Programming 5 Science of Computer Programming 4 Journal of Logical and Algebraic Methods in Programming 2 Acta Informatica 2 Theoretical Computer Science 2 Information and Computation 2 Constraints 2 ACM Transactions on Computational Logic 2 Logical Methods in Computer Science 1 International Journal of General Systems 1 Programming and Computer Software 1 International Journal of Approximate Reasoning 1 Journal of Parallel and Distributed Computing 1 Real-Time Systems 1 Journal of Logic and Computation 1 Mathematical Structures in Computer Science 1 The Journal of Artificial Intelligence Research (JAIR) 1 Mathematical Problems in Engineering 1 Journal of the ACM 1 Fundamenta Informaticae 1 Computer Languages, Systems & Structures 1 ACM Journal of Experimental Algorithmics 1 Science in China. Series F 1 Frontiers of Computer Science all top 5 Cited in 9 Fields 192 Computer science (68-XX) 52 Mathematical logic and foundations (03-XX) 5 Information and communication theory, circuits (94-XX) 3 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 2 Operations research, mathematical programming (90-XX) 1 Order, lattices, ordered algebraic structures (06-XX) 1 Algebraic geometry (14-XX) 1 Biology and other natural sciences (92-XX) 1 Systems theory; control (93-XX) Citations by Year