Edit Profile (opens in new tab) Kröning, Daniel Co-Author Distance Author ID: kroning.daniel Published as: Kroening, Daniel; Kröning, Daniel; Kroening, D. more...less External Links: ORCID Documents Indexed: 89 Publications since 2000, including 3 Books 7 Contributions as Editor Software Indexed: 16 Packages Co-Authors: 104 Co-Authors with 95 Joint Publications 1,911 Co-Co-Authors all top 5 Co-Authors 1 single-authored 11 Strichman, Ofer 11 Wahl, Thomas 10 D’silva, Vijay 9 Abate, Alessandro 9 Sharygina, Natasha 8 David, Cristina 8 Haller, Leopold 8 Rümmer, Philipp 7 Brain, Martin 6 Clarke, Edmund Melson jun. 6 Kesseli, Pascal 6 Schrammel, Peter 6 Wintersteiger, Christoph M. 5 Chebiryak, Yury 5 Cook, Byron 5 Weissenbacher, Georg 4 Brillout, Angelo 4 Cattaruzza, Dario 4 Griggio, Alberto 4 Kaiser, Alexander D. 4 Ouaknine, Joel O. 4 Tautschnig, Michael 3 Bessa, Iury 3 Cordeiro, Lucas C. 3 Donaldson, Alastair F. 3 Mazzucchi, Michele 3 Polgreen, Elizabeth 3 Purandare, Mitra 3 Sousa, Marcelo S. 3 Tsitovich, Aliaksei 3 Zinovik, Igor 2 Abbott, John A. 2 Ábrahám, Erika 2 Basler, Gérard 2 Becker, Bernd 2 Biere, Armin 2 Bigatti, Anna Maria 2 Buchberger, Bruno 2 Chockler, Hana 2 Cimatti, Alessandro 2 Davenport, James Harold 2 England, Matthew 2 Fontaine, Pascal 2 Forrest, Stephen 2 Groce, Alex 2 Grumberg, Orna 2 Lerda, Flavio 2 Martins, Ruben 2 Melham, Tom 2 Păsăreanu, S. 2 Paul, Wolfgang Jakob 2 Rodríguez, César Marín 2 Seiler, Werner M. 2 Seshia, Sanjit Arunkumar 2 Sturm, Thomas 2 Tonetta, Stefano 2 Yorav, Karen 1 Alglave, Jade 1 Barbosa, Haniel 1 Barner, Sharon 1 Barrett, Clark W. 1 Beyer, Sven 1 Bienmüller, Tom 1 Bjørner, Nikolaj S. 1 Brady, Bryan A. 1 Bryant, Randal E. 1 Chapman, Martin 1 Chaves, Lennon 1 de Moura, Leonardo 1 Giannakopoulou, Dimitra 1 Hadarean, Liana 1 Hasanbeig, Hosein 1 Hasanbeig, Mohammadhosein 1 He, Nannan 1 Horn, Alex 1 Huang, Xiaowei 1 Jacobi, Chris 1 Jain, Himanshu 1 Jeppu, Natasha Yogananda 1 Jussila, Toni 1 Kugler, Hillel 1 Leinenbach, Dirk C. 1 Leroux, Jérôme 1 Margaria, Tiziana 1 Mukherjee, Rajdeep 1 Müller, Silvia Melitta 1 Nimal, Vincent 1 Peled, Doron A. 1 Poetzl, Daniel 1 Raz, Orna 1 Reynolds, Andrew 1 Ruan, Wenjie 1 Rybalchenko, Andrey 1 Seghir, Mohamed Nassim 1 Sharma, Subodh K. 1 Sharp, James D. 1 Sinz, Carsten 1 Sun, Youcheng 1 Teige, Tino 1 Thamo, Emese ...and 7 more Co-Authors all top 5 Serials 11 Formal Methods in System Design 4 Journal of Automated Reasoning 4 Formal Aspects of Computing 4 Lecture Notes in Computer Science 2 IEEE Transactions on Information Theory 2 Texts in Theoretical Computer Science. An EATCS Series 1 Acta Informatica 1 Artificial Intelligence 1 Theoretical Computer Science 1 Information and Computation 1 The Journal of Artificial Intelligence Research (JAIR) 1 Journal of Satisfiability, Boolean Modeling and Computation 1 ACM Communications in Computer Algebra 1 Computer Science Review 1 The Cyber Physical Systems Series all top 5 Fields 90 Computer science (68-XX) 13 Mathematical logic and foundations (03-XX) 7 General and overarching topics; collections (00-XX) 3 Systems theory; control (93-XX) 2 Combinatorics (05-XX) 2 Numerical analysis (65-XX) 2 Biology and other natural sciences (92-XX) 1 Order, lattices, ordered algebraic structures (06-XX) 1 Operations research, mathematical programming (90-XX) 1 Information and communication theory, circuits (94-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 79 Publications have been cited 811 times in 562 Documents Cited by ▼ Year ▼ A tool for checking ANSI-C programs. Zbl 1126.68470 Clarke, Edmund; Kroening, Daniel; Lerda, Flavio 98 2004 Model checking. 2nd expanded and updated edition. Zbl 1423.68002 Clarke, Edmund M. jun.; Grumberg, Orna; Kroening, Daniel; Peled, Doron; Veith, Helmut 86 2018 Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant. Zbl 1149.68071 Kroening, Daniel; Strichman, Ofer 59 2008 Deep reinforcement learning with temporal logics. Zbl 1455.68190 Hasanbeig, Mohammadhosein; Kroening, Daniel; Abate, Alessandro 32 2020 Interpolant strength. Zbl 1273.68225 D’Silva, Vijay; Kroening, Daniel; Purandare, Mitra; Weissenbacher, Georg 27 2010 SATABS: SAT-based predicate abstraction for ANSI-C. Zbl 1087.68586 Clarke, Edmund; Kroening, Daniel; Sharygina, Natasha; Yorav, Karen 25 2005 Decision procedures. An algorithmic point of view. 2nd edition. Zbl 1358.68002 Kroening, Daniel; Strichman, Ofer 24 2016 Software verification for weak memory via program transformation. Zbl 1381.68143 Alglave, Jade; Kroening, Daniel; Nimal, Vincent; Tautschnig, Michael 23 2013 Completeness and complexity of bounded model checking. Zbl 1202.68244 Clarke, Edmund; Kroening, Daniel; Ouaknine, Joël; Strichman, Ofer 19 2004 Deciding floating-point logic with abstract conflict driven clause learning. Zbl 1317.68110 Brain, Martin; D’Silva, Vijay; Griggio, Alberto; Haller, Leopold; Kroening, Daniel 19 2014 Predicate abstraction of ANSI-C programs using SAT. Zbl 1090.68022 Clarke, Edmund; Kroening, Daniel; Sharygina, Natasha; Yorav, Karen 18 2004 Deciding bit-vector arithmetic with abstraction. Zbl 1186.68281 Bryant, Randal E.; Kroening, Daniel; Ouaknine, Joël; Seshia, Sanjit A.; Strichman, Ofer; Brady, Bryan 18 2007 An interpolating sequent calculus for quantifier-free Presburger arithmetic. Zbl 1291.03112 Brillout, Angelo; Kroening, Daniel; Rümmer, Philipp; Wahl, Thomas 18 2010 Efficient computation of recurrence diameters. Zbl 1022.68579 Kroening, Daniel; Strichman, Ofer 16 2003 SC\(^2\): satisfiability checking meets symbolic computation. (Project paper). Zbl 1344.68198 Ábrahám, Erika; Abbott, John; Becker, Bernd; Bigatti, Anna M.; Brain, Martin; Buchberger, Bruno; Cimatti, Alessandro; Davenport, James H.; England, Matthew; Fontaine, Pascal; Forrest, Stephen; Griggio, Alberto; Kroening, Daniel; Seiler, Werner M.; Sturm, Thomas 16 2016 A first step towards a unified proof checker for QBF. Zbl 1214.68334 Jussila, Toni; Biere, Armin; Sinz, Carsten; Kröning, Daniel; Wintersteiger, Christoph M. 14 2007 Beyond quantifier-free interpolation in extensions of Presburger arithmetic. Zbl 1318.03045 Brillout, Angelo; Kroening, Daniel; Rümmer, Philipp; Wahl, Thomas 14 2011 Ranking function synthesis for bit-vector relations. Zbl 1284.68172 Cook, Byron; Kroening, Daniel; Rümmer, Philipp; Wintersteiger, Christoph M. 13 2010 A survey of safety and trustworthiness of deep neural networks: verification, testing, adversarial attack and defence, and interpretability. Zbl 1478.68308 Huang, Xiaowei; Kroening, Daniel; Ruan, Wenjie; Sharp, James; Sun, Youcheng; Thamo, Emese; Wu, Min; Yi, Xinping 13 2020 Symbolic counter abstraction for concurrent software. Zbl 1242.68055 Basler, Gérard; Mazzucchi, Michele; Wahl, Thomas; Kroening, Daniel 11 2009 Numeric bounds analysis with conflict-driven learning. Zbl 1352.68060 D’Silva, Vijay; Haller, Leopold; Kroening, Daniel; Tautschnig, Michael 11 2012 An interpolating sequent calculus for quantifier-free Presburger arithmetic. Zbl 1259.03043 Brillout, Angelo; Kroening, Daniel; Rümmer, Philipp; Wahl, Thomas 10 2011 Abstract conflict driven learning. Zbl 1301.68156 D’Silva, Vijay; Haller, Leopold; Kroening, Daniel 9 2013 Linear completeness thresholds for bounded model checking. Zbl 1360.68592 Kroening, Daniel; Ouaknine, Joël; Strichman, Ofer; Wahl, Thomas; Worrell, James 9 2011 Computing binary combinatorial Gray codes via exhaustive search with SAT solvers. Zbl 1328.94095 Zinovik, Igor; Kroening, Daniel; Chebiryak, Yury 8 2008 Under-approximating loops in C programs for fast counterexample detection. Zbl 1322.68054 Kroening, Daniel; Lewis, Matt; Weissenbacher, Georg 8 2015 Learning the language of error. Zbl 1471.68101 Chapman, Martin; Chockler, Hana; Kesseli, Pascal; Kroening, Daniel; Strichman, Ofer; Tautschnig, Michael 8 2015 Counterexample guided inductive synthesis modulo theories. Zbl 1511.68064 Abate, Alessandro; David, Cristina; Kesseli, Pascal; Kroening, Daniel; Polgreen, Elizabeth 8 2018 Unfolding-based partial order reduction. Zbl 1374.68342 Rodríguez, César; Sousa, Marcelo; Sharma, Subodh; Kroening, Daniel 8 2015 Loop summarization and termination analysis. Zbl 1315.68106 Tsitovich, Aliaksei; Sharygina, Natasha; Wintersteiger, Christoph M.; Kroening, Daniel 7 2011 Towards a classification of Hamiltonian cycles in the 6-cube. Zbl 1147.68703 Chebiryak, Yury; Kroening, Daniel 6 2008 Cogent: Accurate theorem proving for program verification. Zbl 1081.68673 Cook, Byron; Kroening, Daniel; Sharygina, Natasha 6 2005 Abstraction-based satisfiability solving of Presburger arithmetic. Zbl 1103.68626 Kroening, Daniel; Ouaknine, Joël; Seshia, Sanjit A.; Strichman, Ofer 6 2004 Understanding counterexamples with explain. Zbl 1103.68620 Groce, Alex; Kroening, Daniel; Lerda, Flavio 6 2004 Unbounded-time analysis of guarded LTI systems with inputs by abstract acceleration. Zbl 1419.68041 Cattaruzza, Dario; Abate, Alessandro; Schrammel, Peter; Kroening, Daniel 6 2015 Efficient coverability analysis by proof minimization. Zbl 1364.68138 Kaiser, Alexander; Kroening, Daniel; Wahl, Thomas 6 2012 Abstract satisfaction. Zbl 1284.68392 D’Silva, Vijay; Haller, Leopold; Kroening, Daniel 6 2014 Interpolating quantifier-free Presburger arithmetic. Zbl 1306.68148 Kroening, Daniel; Leroux, Jérôme; Rümmer, Philipp 6 2010 Symbolic model checking for asynchronous Boolean programs. Zbl 1151.68367 Cook, Byron; Kroening, Daniel; Sharygina, Natasha 5 2005 Loop summarization using abstract transformers. Zbl 1183.68377 Kroening, Daniel; Sharygina, Natasha; Tonetta, Stefano; Tsitovich, Aliaksei; Wintersteiger, Christoph M. 5 2008 Verification of Boolean programs with unbounded thread creation. Zbl 1143.68043 Cook, Byron; Kroening, Daniel; Sharygina, Natasha 5 2007 Automatic generation of propagation complete SAT encodings. Zbl 1475.68218 Brain, Martin; Hadarean, Liana; Kroening, Daniel; Martins, Ruben 5 2016 Modular demand-driven analysis of semantic difference for program versions. Zbl 1420.68076 Trostanetski, Anna; Grumberg, Orna; Kroening, Daniel 5 2017 Periodic orbits and equilibria in Glass models for gene regulatory networks. Zbl 1366.92052 Zinovik, Igor; Chebiryak, Yury; Kroening, Daniel 5 2010 Ranking function synthesis for bit-vector relations. Zbl 1291.68138 Cook, Byron; Kroening, Daniel; Rümmer, Philipp; Wintersteiger, Christoph M. 5 2013 Approximating predicate images for bit-vector logic. Zbl 1180.68175 Kroening, Daniel; Sharygina, Natasha 5 2006 SAT-based model checking. Zbl 1392.68232 Biere, Armin; Kröning, Daniel 5 2018 Unrestricted termination and non-termination arguments for bit-vector programs. Zbl 1335.68050 David, Cristina; Kroening, Daniel; Lewis, Matt 4 2015 Automatic analysis of DMA races using model checking and \(k\)-induction. Zbl 1233.68124 Donaldson, Alastair F.; Kroening, Daniel; Rümmer, Philipp 4 2011 Verification of SpecC using predicate abstraction. Zbl 1117.68046 Clarke, Edmund; Jain, Himanshu; Kroening, Daniel 4 2007 Counterexample-guided abstraction refinement for symmetric concurrent programs. Zbl 1284.68179 Donaldson, Alastair F.; Kaiser, Alexander; Kroening, Daniel; Tautschnig, Michael; Wahl, Thomas 4 2012 Instantiating uninterpreted functional units and memory system: Functional verification of the VAMP. Zbl 1179.68009 Beyer, Sven; Jacobi, Chris; Kröning, Daniel; Leinenbach, Dirk; Paul, Wolfgang J. 4 2003 Approximation refinement for interpolation-based model checking. Zbl 1138.68444 D’Silva, Vijay; Purandare, Mitra; Kroening, Daniel 3 2008 Computing over-approximations with bounded model checking. Zbl 1272.68264 Kroening, Daniel 3 2006 Making the most of BMC counterexamples. Zbl 1272.68252 Groce, Alex; Kroening, Daniel 3 2005 Learning the language of software errors. Zbl 1437.68071 Chockler, Hana; Kesseli, Pascal; Kroening, Daniel; Strichman, Ofer 3 2020 An abstract interpretation of DPLL(T). Zbl 1426.68249 Brain, Martin; D’silva, Vijay; Haller, Leopold; Griggio, Alberto; Kroening, Daniel 3 2013 An algebraic algorithm for the identification of glass networks with periodic orbits along cyclic attractors. Zbl 1127.92004 Zinovik, Igor; Kroening, Daniel; Chebiryak, Yury 2 2007 Using program synthesis for program analysis. Zbl 1471.68056 David, Cristina; Kroening, Daniel; Lewis, Matt 2 2015 Sound and automated synthesis of digital stabilizing controllers for continuous plants. Zbl 1369.93189 Abate, Alessandro; Bessa, Iury; Cattaruzza, Dario; Cordeiro, Lucas; David, Cristina; Kesseli, Pascal; Kroening, Daniel 2 2017 Strengthening induction-based race checking with lightweight static analysis. Zbl 1317.68113 Donaldson, Alastair F.; Haller, Leopold; Kroening, Daniel 2 2011 Context-aware counter abstraction. Zbl 1213.68362 Basler, Gérard; Mazzucchi, Michele; Wahl, Thomas; Kroening, Daniel 2 2010 Automated formal synthesis of provably safe digital controllers for continuous plants. Zbl 1441.93171 Abate, Alessandro; Bessa, Iury; Cordeiro, Lucas; David, Cristina; Kesseli, Pascal; Kroening, Daniel; Polgreen, Elizabeth 2 2020 Loop summarization using state and transition invariants. Zbl 1291.68262 Kroening, Daniel; Sharygina, Natasha; Tonetta, Stefano; Tsitovich, Aliaksei; Wintersteiger, Christoph M. 2 2013 Lost in abstraction: monotonicity in multi-threaded programs. Zbl 1417.68133 Kaiser, Alexander; Kroening, Daniel; Wahl, Thomas 2 2014 Verification and falsification of programs with loops using predicate abstraction. Zbl 1215.68130 Kroening, Daniel; Weissenbacher, Georg 2 2010 Certified reinforcement learning with logic guidance. Zbl 07732224 Hasanbeig, Hosein; Kroening, Daniel; Abate, Alessandro 2 2023 Incremental bounded model checking for embedded software. Zbl 1375.68081 Schrammel, Peter; Kroening, Daniel; Brain, Martin; Martins, Ruben; Teige, Tino; Bienmüller, Tom 2 2017 Abstract interpretation with unfoldings. Zbl 1494.68044 Sousa, Marcelo; Rodríguez, César; D’Silva, Vijay; Kroening, Daniel 2 2017 Formalizing and checking thread refinement for data-race-free execution models. Zbl 1420.68072 Poetzl, Daniel; Kroening, Daniel 1 2016 Propositional reasoning about safety and termination of heap-manipulating programs. Zbl 1335.68051 David, Cristina; Kroening, Daniel; Lewis, Matt 1 2015 Counterexample-guided precondition inference. Zbl 1381.68180 Seghir, Mohamed Nassim; Kroening, Daniel 1 2013 Mutation-based test case generation for Simulink models. Zbl 1312.68130 Brillout, Angelo; He, Nannan; Mazzucchi, Michele; Kroening, Daniel; Purandare, Mitra; Rümmer, Philipp; Weissenbacher, Georg 1 2010 Proving safety with trace automata and bounded model checking. Zbl 1427.68047 Kroening, Daniel; Lewis, Matt; Weissenbacher, Georg 1 2015 Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration. Zbl 1543.68198 Cattaruzza, Dario; Abate, Alessandro; Schrammel, Peter; Kroening, Daniel 1 2021 Lost in abstraction: monotonicity in multi-threaded programs. Zbl 1355.68055 Kaiser, Alexander; Kroening, Daniel; Wahl, Thomas 1 2017 On partial order semantics for SAT/SMT-based symbolic encodings of weak memory concurrency. Zbl 1347.68268 Horn, Alex; Kroening, Daniel 1 2015 Sound numerical computations in abstract acceleration. Zbl 1515.65344 Cattaruzza, Dario; Abate, Alessandro; Schrammel, Peter; Kroening, Daniel 1 2017 Lifting CDCL to template-based abstract domains for program verification. Zbl 1495.68139 Mukherjee, Rajdeep; Schrammel, Peter; Haller, Leopold; Kroening, Daniel; Melham, Tom 1 2017 Certified reinforcement learning with logic guidance. Zbl 07732224 Hasanbeig, Hosein; Kroening, Daniel; Abate, Alessandro 2 2023 Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration. Zbl 1543.68198 Cattaruzza, Dario; Abate, Alessandro; Schrammel, Peter; Kroening, Daniel 1 2021 Deep reinforcement learning with temporal logics. Zbl 1455.68190 Hasanbeig, Mohammadhosein; Kroening, Daniel; Abate, Alessandro 32 2020 A survey of safety and trustworthiness of deep neural networks: verification, testing, adversarial attack and defence, and interpretability. Zbl 1478.68308 Huang, Xiaowei; Kroening, Daniel; Ruan, Wenjie; Sharp, James; Sun, Youcheng; Thamo, Emese; Wu, Min; Yi, Xinping 13 2020 Learning the language of software errors. Zbl 1437.68071 Chockler, Hana; Kesseli, Pascal; Kroening, Daniel; Strichman, Ofer 3 2020 Automated formal synthesis of provably safe digital controllers for continuous plants. Zbl 1441.93171 Abate, Alessandro; Bessa, Iury; Cordeiro, Lucas; David, Cristina; Kesseli, Pascal; Kroening, Daniel; Polgreen, Elizabeth 2 2020 Model checking. 2nd expanded and updated edition. Zbl 1423.68002 Clarke, Edmund M. jun.; Grumberg, Orna; Kroening, Daniel; Peled, Doron; Veith, Helmut 86 2018 Counterexample guided inductive synthesis modulo theories. Zbl 1511.68064 Abate, Alessandro; David, Cristina; Kesseli, Pascal; Kroening, Daniel; Polgreen, Elizabeth 8 2018 SAT-based model checking. Zbl 1392.68232 Biere, Armin; Kröning, Daniel 5 2018 Modular demand-driven analysis of semantic difference for program versions. Zbl 1420.68076 Trostanetski, Anna; Grumberg, Orna; Kroening, Daniel 5 2017 Sound and automated synthesis of digital stabilizing controllers for continuous plants. Zbl 1369.93189 Abate, Alessandro; Bessa, Iury; Cattaruzza, Dario; Cordeiro, Lucas; David, Cristina; Kesseli, Pascal; Kroening, Daniel 2 2017 Incremental bounded model checking for embedded software. Zbl 1375.68081 Schrammel, Peter; Kroening, Daniel; Brain, Martin; Martins, Ruben; Teige, Tino; Bienmüller, Tom 2 2017 Abstract interpretation with unfoldings. Zbl 1494.68044 Sousa, Marcelo; Rodríguez, César; D’Silva, Vijay; Kroening, Daniel 2 2017 Lost in abstraction: monotonicity in multi-threaded programs. Zbl 1355.68055 Kaiser, Alexander; Kroening, Daniel; Wahl, Thomas 1 2017 Sound numerical computations in abstract acceleration. Zbl 1515.65344 Cattaruzza, Dario; Abate, Alessandro; Schrammel, Peter; Kroening, Daniel 1 2017 Lifting CDCL to template-based abstract domains for program verification. Zbl 1495.68139 Mukherjee, Rajdeep; Schrammel, Peter; Haller, Leopold; Kroening, Daniel; Melham, Tom 1 2017 Decision procedures. An algorithmic point of view. 2nd edition. Zbl 1358.68002 Kroening, Daniel; Strichman, Ofer 24 2016 SC\(^2\): satisfiability checking meets symbolic computation. (Project paper). Zbl 1344.68198 Ábrahám, Erika; Abbott, John; Becker, Bernd; Bigatti, Anna M.; Brain, Martin; Buchberger, Bruno; Cimatti, Alessandro; Davenport, James H.; England, Matthew; Fontaine, Pascal; Forrest, Stephen; Griggio, Alberto; Kroening, Daniel; Seiler, Werner M.; Sturm, Thomas 16 2016 Automatic generation of propagation complete SAT encodings. Zbl 1475.68218 Brain, Martin; Hadarean, Liana; Kroening, Daniel; Martins, Ruben 5 2016 Formalizing and checking thread refinement for data-race-free execution models. Zbl 1420.68072 Poetzl, Daniel; Kroening, Daniel 1 2016 Under-approximating loops in C programs for fast counterexample detection. Zbl 1322.68054 Kroening, Daniel; Lewis, Matt; Weissenbacher, Georg 8 2015 Learning the language of error. Zbl 1471.68101 Chapman, Martin; Chockler, Hana; Kesseli, Pascal; Kroening, Daniel; Strichman, Ofer; Tautschnig, Michael 8 2015 Unfolding-based partial order reduction. Zbl 1374.68342 Rodríguez, César; Sousa, Marcelo; Sharma, Subodh; Kroening, Daniel 8 2015 Unbounded-time analysis of guarded LTI systems with inputs by abstract acceleration. Zbl 1419.68041 Cattaruzza, Dario; Abate, Alessandro; Schrammel, Peter; Kroening, Daniel 6 2015 Unrestricted termination and non-termination arguments for bit-vector programs. Zbl 1335.68050 David, Cristina; Kroening, Daniel; Lewis, Matt 4 2015 Using program synthesis for program analysis. Zbl 1471.68056 David, Cristina; Kroening, Daniel; Lewis, Matt 2 2015 Propositional reasoning about safety and termination of heap-manipulating programs. Zbl 1335.68051 David, Cristina; Kroening, Daniel; Lewis, Matt 1 2015 Proving safety with trace automata and bounded model checking. Zbl 1427.68047 Kroening, Daniel; Lewis, Matt; Weissenbacher, Georg 1 2015 On partial order semantics for SAT/SMT-based symbolic encodings of weak memory concurrency. Zbl 1347.68268 Horn, Alex; Kroening, Daniel 1 2015 Deciding floating-point logic with abstract conflict driven clause learning. Zbl 1317.68110 Brain, Martin; D’Silva, Vijay; Griggio, Alberto; Haller, Leopold; Kroening, Daniel 19 2014 Abstract satisfaction. Zbl 1284.68392 D’Silva, Vijay; Haller, Leopold; Kroening, Daniel 6 2014 Lost in abstraction: monotonicity in multi-threaded programs. Zbl 1417.68133 Kaiser, Alexander; Kroening, Daniel; Wahl, Thomas 2 2014 Software verification for weak memory via program transformation. Zbl 1381.68143 Alglave, Jade; Kroening, Daniel; Nimal, Vincent; Tautschnig, Michael 23 2013 Abstract conflict driven learning. Zbl 1301.68156 D’Silva, Vijay; Haller, Leopold; Kroening, Daniel 9 2013 Ranking function synthesis for bit-vector relations. Zbl 1291.68138 Cook, Byron; Kroening, Daniel; Rümmer, Philipp; Wintersteiger, Christoph M. 5 2013 An abstract interpretation of DPLL(T). Zbl 1426.68249 Brain, Martin; D’silva, Vijay; Haller, Leopold; Griggio, Alberto; Kroening, Daniel 3 2013 Loop summarization using state and transition invariants. Zbl 1291.68262 Kroening, Daniel; Sharygina, Natasha; Tonetta, Stefano; Tsitovich, Aliaksei; Wintersteiger, Christoph M. 2 2013 Counterexample-guided precondition inference. Zbl 1381.68180 Seghir, Mohamed Nassim; Kroening, Daniel 1 2013 Numeric bounds analysis with conflict-driven learning. Zbl 1352.68060 D’Silva, Vijay; Haller, Leopold; Kroening, Daniel; Tautschnig, Michael 11 2012 Efficient coverability analysis by proof minimization. Zbl 1364.68138 Kaiser, Alexander; Kroening, Daniel; Wahl, Thomas 6 2012 Counterexample-guided abstraction refinement for symmetric concurrent programs. Zbl 1284.68179 Donaldson, Alastair F.; Kaiser, Alexander; Kroening, Daniel; Tautschnig, Michael; Wahl, Thomas 4 2012 Beyond quantifier-free interpolation in extensions of Presburger arithmetic. Zbl 1318.03045 Brillout, Angelo; Kroening, Daniel; Rümmer, Philipp; Wahl, Thomas 14 2011 An interpolating sequent calculus for quantifier-free Presburger arithmetic. Zbl 1259.03043 Brillout, Angelo; Kroening, Daniel; Rümmer, Philipp; Wahl, Thomas 10 2011 Linear completeness thresholds for bounded model checking. Zbl 1360.68592 Kroening, Daniel; Ouaknine, Joël; Strichman, Ofer; Wahl, Thomas; Worrell, James 9 2011 Loop summarization and termination analysis. Zbl 1315.68106 Tsitovich, Aliaksei; Sharygina, Natasha; Wintersteiger, Christoph M.; Kroening, Daniel 7 2011 Automatic analysis of DMA races using model checking and \(k\)-induction. Zbl 1233.68124 Donaldson, Alastair F.; Kroening, Daniel; Rümmer, Philipp 4 2011 Strengthening induction-based race checking with lightweight static analysis. Zbl 1317.68113 Donaldson, Alastair F.; Haller, Leopold; Kroening, Daniel 2 2011 Interpolant strength. Zbl 1273.68225 D’Silva, Vijay; Kroening, Daniel; Purandare, Mitra; Weissenbacher, Georg 27 2010 An interpolating sequent calculus for quantifier-free Presburger arithmetic. Zbl 1291.03112 Brillout, Angelo; Kroening, Daniel; Rümmer, Philipp; Wahl, Thomas 18 2010 Ranking function synthesis for bit-vector relations. Zbl 1284.68172 Cook, Byron; Kroening, Daniel; Rümmer, Philipp; Wintersteiger, Christoph M. 13 2010 Interpolating quantifier-free Presburger arithmetic. Zbl 1306.68148 Kroening, Daniel; Leroux, Jérôme; Rümmer, Philipp 6 2010 Periodic orbits and equilibria in Glass models for gene regulatory networks. Zbl 1366.92052 Zinovik, Igor; Chebiryak, Yury; Kroening, Daniel 5 2010 Context-aware counter abstraction. Zbl 1213.68362 Basler, Gérard; Mazzucchi, Michele; Wahl, Thomas; Kroening, Daniel 2 2010 Verification and falsification of programs with loops using predicate abstraction. Zbl 1215.68130 Kroening, Daniel; Weissenbacher, Georg 2 2010 Mutation-based test case generation for Simulink models. Zbl 1312.68130 Brillout, Angelo; He, Nannan; Mazzucchi, Michele; Kroening, Daniel; Purandare, Mitra; Rümmer, Philipp; Weissenbacher, Georg 1 2010 Symbolic counter abstraction for concurrent software. Zbl 1242.68055 Basler, Gérard; Mazzucchi, Michele; Wahl, Thomas; Kroening, Daniel 11 2009 Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant. Zbl 1149.68071 Kroening, Daniel; Strichman, Ofer 59 2008 Computing binary combinatorial Gray codes via exhaustive search with SAT solvers. Zbl 1328.94095 Zinovik, Igor; Kroening, Daniel; Chebiryak, Yury 8 2008 Towards a classification of Hamiltonian cycles in the 6-cube. Zbl 1147.68703 Chebiryak, Yury; Kroening, Daniel 6 2008 Loop summarization using abstract transformers. Zbl 1183.68377 Kroening, Daniel; Sharygina, Natasha; Tonetta, Stefano; Tsitovich, Aliaksei; Wintersteiger, Christoph M. 5 2008 Approximation refinement for interpolation-based model checking. Zbl 1138.68444 D’Silva, Vijay; Purandare, Mitra; Kroening, Daniel 3 2008 Deciding bit-vector arithmetic with abstraction. Zbl 1186.68281 Bryant, Randal E.; Kroening, Daniel; Ouaknine, Joël; Seshia, Sanjit A.; Strichman, Ofer; Brady, Bryan 18 2007 A first step towards a unified proof checker for QBF. Zbl 1214.68334 Jussila, Toni; Biere, Armin; Sinz, Carsten; Kröning, Daniel; Wintersteiger, Christoph M. 14 2007 Verification of Boolean programs with unbounded thread creation. Zbl 1143.68043 Cook, Byron; Kroening, Daniel; Sharygina, Natasha 5 2007 Verification of SpecC using predicate abstraction. Zbl 1117.68046 Clarke, Edmund; Jain, Himanshu; Kroening, Daniel 4 2007 An algebraic algorithm for the identification of glass networks with periodic orbits along cyclic attractors. Zbl 1127.92004 Zinovik, Igor; Kroening, Daniel; Chebiryak, Yury 2 2007 Approximating predicate images for bit-vector logic. Zbl 1180.68175 Kroening, Daniel; Sharygina, Natasha 5 2006 Computing over-approximations with bounded model checking. Zbl 1272.68264 Kroening, Daniel 3 2006 SATABS: SAT-based predicate abstraction for ANSI-C. Zbl 1087.68586 Clarke, Edmund; Kroening, Daniel; Sharygina, Natasha; Yorav, Karen 25 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 Making the most of BMC counterexamples. Zbl 1272.68252 Groce, Alex; Kroening, Daniel 3 2005 A tool for checking ANSI-C programs. Zbl 1126.68470 Clarke, Edmund; Kroening, Daniel; Lerda, Flavio 98 2004 Completeness and complexity of bounded model checking. Zbl 1202.68244 Clarke, Edmund; Kroening, Daniel; Ouaknine, Joël; Strichman, Ofer 19 2004 Predicate abstraction of ANSI-C programs using SAT. Zbl 1090.68022 Clarke, Edmund; Kroening, Daniel; Sharygina, Natasha; Yorav, Karen 18 2004 Abstraction-based satisfiability solving of Presburger arithmetic. Zbl 1103.68626 Kroening, Daniel; Ouaknine, Joël; Seshia, Sanjit A.; Strichman, Ofer 6 2004 Understanding counterexamples with explain. Zbl 1103.68620 Groce, Alex; Kroening, Daniel; Lerda, Flavio 6 2004 Efficient computation of recurrence diameters. Zbl 1022.68579 Kroening, Daniel; Strichman, Ofer 16 2003 Instantiating uninterpreted functional units and memory system: Functional verification of the VAMP. Zbl 1179.68009 Beyer, Sven; Jacobi, Chris; Kröning, Daniel; Leinenbach, Dirk; Paul, Wolfgang J. 4 2003 all cited Publications top 5 cited Publications all top 5 Cited by 1,199 Authors 39 Kröning, Daniel 14 Abate, Alessandro 13 Rümmer, Philipp 12 Sharygina, Natasha 8 Biere, Armin 8 Cimatti, Alessandro 8 Podelski, Andreas 8 Wahl, Thomas 7 Barrett, Clark W. 7 Bruttomesso, Roberto 7 Davenport, James Harold 7 Griggio, Alberto 7 Sebastiani, Roberto 7 Veith, Helmut 7 Wintersteiger, Christoph M. 6 D’silva, Vijay 6 England, Matthew 6 Fedyukovich, Grigory 6 Frohn, Florian 6 Ganesh, Vijay 6 Giesl, Jürgen 6 Gurfinkel, Arie 6 Henzinger, Thomas A. 6 King, Andy 6 Kuncak, Viktor 6 Strichman, Ofer 6 Sturm, Thomas 6 Weissenbacher, Georg 5 Ábrahám, Erika 5 Atig, Mohamed Faouzi 5 Bonacina, Maria Paola 5 Gupta, Ashutosh 5 Haller, Leopold 5 Hensel, Jera 5 Hoenicke, Jochen 5 Hyvärinen, Antti E. J. 5 Kincaid, Zachary 5 Seshia, Sanjit Arunkumar 5 Tinelli, Cesare 5 Wies, Thomas 4 Abdulla, Parosh Aziz 4 Bouajjani, Ahmed 4 Bozzano, Marco 4 Brain, Martin 4 Bright, Curtis 4 Clarke, Edmund Melson jun. 4 David, Cristina 4 Donaldson, Alastair F. 4 Duan, Zhenhua 4 Fisman, Dana 4 Frenkel, Hadar 4 Ghilardi, Silvio 4 Grumberg, Orna 4 Gupta, Aarti 4 Inverso, Omar 4 Junges, Sebastian 4 Konnov, Igor Vladimirovich 4 Kotsireas, Ilias S. 4 Lin, Anthony Widjaja 4 Niemetz, Aina 4 Ouaknine, Joel O. 4 Polgreen, Elizabeth 4 Preiner, Mathias 4 Ranise, Silvio 4 Reynolds, Andrew 4 Rybalchenko, Andrey 4 Strejček, Jan 4 Tonetta, Stefano 4 Tsitovich, Aliaksei 4 Wehrheim, Heike 3 Ahmed, Daniele 3 Asadi, Sepideh 3 Bardin, Sébastien 3 Becker, Bernd 3 Bessa, Iury 3 Blicha, Martin 3 Brauer, Jörg 3 Brillout, Angelo 3 Brockschmidt, Marc 3 Cattaruzza, Dario 3 Chaki, Sagar 3 Chakraborty, Supratik 3 Chen, Mingshuai 3 Cordeiro, Lucas C. 3 Dasgupta, Pallab 3 Dietsch, Daniel 3 Farzan, Azadeh 3 Fujita, Masahiro 3 Gutierrez, Julian 3 Heule, Marijn J. H. 3 Huang, Xiaowei 3 Johansson, Moa 3 Jonáš, Martin 3 Kapur, Deepak 3 Katoen, Joost-Pieter 3 Kesseli, Pascal 3 Kupferman, Orna 3 Miné, Antoine 3 Monniaux, David P. 3 Norrish, Michael ...and 1,099 more Authors all top 5 Cited in 71 Serials 54 Formal Methods in System Design 37 Journal of Automated Reasoning 19 Formal Aspects of Computing 15 Journal of Logical and Algebraic Methods in Programming 11 Theoretical Computer Science 10 Logical Methods in Computer Science 9 Acta Informatica 7 Artificial Intelligence 7 Information and Computation 6 Journal of Symbolic Computation 5 Annals of Mathematics and Artificial Intelligence 4 Automatica 4 Fundamenta Informaticae 4 Mathematics in Computer Science 3 Information Processing Letters 3 Journal of Computer and System Sciences 3 Programming and Computer Software 3 Science of Computer Programming 3 Machine Learning 3 Discrete Event Dynamic Systems 3 The Journal of Artificial Intelligence Research (JAIR) 3 Theory of Computing Systems 3 Theory and Practice of Logic Programming 2 Discrete Applied Mathematics 2 Journal of Computer Science and Technology 2 International Journal of Parallel Programming 2 Designs, Codes and Cryptography 2 The Electronic Journal of Combinatorics 2 Constraints 2 Journal of the ACM 2 International Journal of Applied Mathematics and Computer Science 2 The Journal of Logic and Algebraic Programming 2 Journal of Applied Mathematics 2 Computer Languages, Systems & Structures 2 ACM Transactions on Computational Logic 2 Journal of Applied Logic 2 Modelirovanie i Analiz Informatsionnykh Sistem 1 ACM Computing Surveys 1 American Mathematical Monthly 1 International Journal of General Systems 1 Computing 1 Information Sciences 1 Journal of Combinatorial Theory. Series B 1 Annals of Pure and Applied Logic 1 Graphs and Combinatorics 1 European Journal of Applied Mathematics 1 Real-Time Systems 1 International Journal of Foundations of Computer Science 1 Acta Mathematica Universitatis Comenianae. New Series 1 International Journal of Bifurcation and Chaos in Applied Sciences and Engineering 1 Cybernetics and Systems Analysis 1 Journal of Computer and Systems Sciences International 1 ACM Transactions on Modeling and Computer Simulation 1 INFORMS Journal on Computing 1 Optimization Methods & Software 1 Journal of Combinatorial Optimization 1 Informatica (Vilnius) 1 SIAM Journal on Applied Dynamical Systems 1 ACM Journal of Experimental Algorithmics 1 Mathematical Biosciences and Engineering 1 Discrete Optimization 1 Journal of Zhejiang University. Science A 1 Journal of Satisfiability, Boolean Modeling and Computation 1 Nonlinear Analysis. Hybrid Systems 1 Foundations and Trends in Theoretical Computer Science 1 ACM Communications in Computer Algebra 1 Diskretnyĭ Analiz i Issledovanie Operatsiĭ 1 Central European Journal of Computer Science 1 Journal of Theoretical Biology 1 Computer Science Review 1 SN Operations Research Forum all top 5 Cited in 23 Fields 523 Computer science (68-XX) 102 Mathematical logic and foundations (03-XX) 24 Systems theory; control (93-XX) 23 Information and communication theory, circuits (94-XX) 21 Operations research, mathematical programming (90-XX) 19 Combinatorics (05-XX) 11 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 9 Order, lattices, ordered algebraic structures (06-XX) 8 Numerical analysis (65-XX) 7 Biology and other natural sciences (92-XX) 5 General and overarching topics; collections (00-XX) 5 Ordinary differential equations (34-XX) 4 Number theory (11-XX) 4 Probability theory and stochastic processes (60-XX) 4 Statistics (62-XX) 2 Commutative algebra (13-XX) 2 Algebraic geometry (14-XX) 2 Category theory; homological algebra (18-XX) 2 Convex and discrete geometry (52-XX) 1 Field theory and polynomials (12-XX) 1 Dynamical systems and ergodic theory (37-XX) 1 General topology (54-XX) 1 Fluid mechanics (76-XX) Citations by Year