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: 88 Publications since 2000, including 3 Books 7 Contributions as Editor Co-Authors: 103 Co-Authors with 94 Joint Publications 1,840 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 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 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 Jussila, Toni 1 Kugler, Hillel 1 Leinenbach, Dirk C. 1 Leroux, Jérôme 1 Margaria, Tiziana 1 Melham, Tom 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 1 Tinelli, Cesare ...and 6 more Co-Authors all top 5 Serials 10 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 89 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 72 Publications have been cited 639 times in 434 Documents Cited by ▼ Year ▼ A tool for checking ANSI-C programs. Zbl 1126.68470Clarke, Edmund; Kroening, Daniel; Lerda, Flavio 73 2004 Model checking. 2nd expanded and updated edition. Zbl 1423.68002Clarke, Edmund M. jun.; Grumberg, Orna; Kroening, Daniel; Peled, Doron; Veith, Helmut 64 2018 Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant. Zbl 1149.68071Kroening, Daniel; Strichman, Ofer 52 2008 Interpolant strength. Zbl 1273.68225D’Silva, Vijay; Kroening, Daniel; Purandare, Mitra; Weissenbacher, Georg 23 2010 Deep reinforcement learning with temporal logics. Zbl 1455.68190Hasanbeig, Mohammadhosein; Kroening, Daniel; Abate, Alessandro 20 2020 SATABS: SAT-based predicate abstraction for ANSI-C. Zbl 1087.68586Clarke, Edmund; Kroening, Daniel; Sharygina, Natasha; Yorav, Karen 20 2005 Software verification for weak memory via program transformation. Zbl 1381.68143Alglave, Jade; Kroening, Daniel; Nimal, Vincent; Tautschnig, Michael 17 2013 Deciding floating-point logic with abstract conflict driven clause learning. Zbl 1317.68110Brain, Martin; D’Silva, Vijay; Griggio, Alberto; Haller, Leopold; Kroening, Daniel 17 2014 An interpolating sequent calculus for quantifier-free Presburger arithmetic. Zbl 1291.03112Brillout, Angelo; Kroening, Daniel; Rümmer, Philipp; Wahl, Thomas 17 2010 Decision procedures. An algorithmic point of view. 2nd edition. Zbl 1358.68002Kroening, Daniel; Strichman, Ofer 17 2016 Completeness and complexity of bounded model checking. Zbl 1202.68244Clarke, Edmund; Kroening, Daniel; Ouaknine, Joël; Strichman, Ofer 16 2004 Predicate abstraction of ANSI-C programs using SAT. Zbl 1090.68022Clarke, Edmund; Kroening, Daniel; Sharygina, Natasha; Yorav, Karen 16 2004 Deciding bit-vector arithmetic with abstraction. Zbl 1186.68281Bryant, Randal E.; Kroening, Daniel; Ouaknine, Joël; Seshia, Sanjit A.; Strichman, Ofer; Brady, Bryan 15 2007 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 13 2016 A first step towards a unified proof checker for QBF. Zbl 1214.68334Jussila, Toni; Biere, Armin; Sinz, Carsten; Kröning, Daniel; Wintersteiger, Christoph M. 13 2007 Ranking function synthesis for bit-vector relations. Zbl 1284.68172Cook, Byron; Kroening, Daniel; Rümmer, Philipp; Wintersteiger, Christoph M. 11 2010 Beyond quantifier-free interpolation in extensions of Presburger arithmetic. Zbl 1318.03045Brillout, Angelo; Kroening, Daniel; Rümmer, Philipp; Wahl, Thomas 11 2011 A survey of safety and trustworthiness of deep neural networks: verification, testing, adversarial attack and defence, and interpretability. Zbl 1478.68308Huang, Xiaowei; Kroening, Daniel; Ruan, Wenjie; Sharp, James; Sun, Youcheng; Thamo, Emese; Wu, Min; Yi, Xinping 9 2020 An interpolating sequent calculus for quantifier-free Presburger arithmetic. Zbl 1259.03043Brillout, Angelo; Kroening, Daniel; Rümmer, Philipp; Wahl, Thomas 9 2011 Symbolic counter abstraction for concurrent software. Zbl 1242.68055Basler, Gérard; Mazzucchi, Michele; Wahl, Thomas; Kroening, Daniel 9 2009 Efficient computation of recurrence diameters. Zbl 1022.68579Kroening, Daniel; Strichman, Ofer 9 2003 Numeric bounds analysis with conflict-driven learning. Zbl 1352.68060D’Silva, Vijay; Haller, Leopold; Kroening, Daniel; Tautschnig, Michael 8 2012 Abstract conflict driven learning. Zbl 1301.68156D’Silva, Vijay; Haller, Leopold; Kroening, Daniel 8 2013 Learning the language of error. Zbl 1471.68101Chapman, Martin; Chockler, Hana; Kesseli, Pascal; Kroening, Daniel; Strichman, Ofer; Tautschnig, Michael 8 2015 Loop summarization and termination analysis. Zbl 1315.68106Tsitovich, Aliaksei; Sharygina, Natasha; Wintersteiger, Christoph M.; Kroening, Daniel 7 2011 Linear completeness thresholds for bounded model checking. Zbl 1360.68592Kroening, Daniel; Ouaknine, Joël; Strichman, Ofer; Wahl, Thomas; Worrell, James 7 2011 Under-approximating loops in C programs for fast counterexample detection. Zbl 1322.68054Kroening, Daniel; Lewis, Matt; Weissenbacher, Georg 7 2015 Efficient coverability analysis by proof minimization. Zbl 1364.68138Kaiser, Alexander; Kroening, Daniel; Wahl, Thomas 6 2012 Computing binary combinatorial Gray codes via exhaustive search with SAT solvers. Zbl 1328.94095Zinovik, Igor; Kroening, Daniel; Chebiryak, Yury 6 2008 Understanding counterexamples with explain. Zbl 1103.68620Groce, Alex; Kroening, Daniel; Lerda, Flavio 6 2004 Towards a classification of Hamiltonian cycles in the 6-cube. Zbl 1147.68703Chebiryak, Yury; Kroening, Daniel 6 2008 Unfolding-based partial order reduction. Zbl 1374.68342Rodríguez, César; Sousa, Marcelo; Sharma, Subodh; Kroening, Daniel 6 2015 Interpolating quantifier-free Presburger arithmetic. Zbl 1306.68148Kroening, Daniel; Leroux, Jérôme; Rümmer, Philipp 5 2010 Abstract satisfaction. Zbl 1284.68392D’Silva, Vijay; Haller, Leopold; Kroening, Daniel 5 2014 Abstraction-based satisfiability solving of Presburger arithmetic. Zbl 1103.68626Kroening, Daniel; Ouaknine, Joël; Seshia, Sanjit A.; Strichman, Ofer 5 2004 Verification of Boolean programs with unbounded thread creation. Zbl 1143.68043Cook, Byron; Kroening, Daniel; Sharygina, Natasha 5 2007 Symbolic model checking for asynchronous Boolean programs. Zbl 1151.68367Cook, Byron; Kroening, Daniel; Sharygina, Natasha 5 2005 Loop summarization using abstract transformers. Zbl 1183.68377Kroening, Daniel; Sharygina, Natasha; Tonetta, Stefano; Tsitovich, Aliaksei; Wintersteiger, Christoph M. 5 2008 Periodic orbits and equilibria in Glass models for gene regulatory networks. Zbl 1366.92052Zinovik, Igor; Chebiryak, Yury; Kroening, Daniel 5 2010 Approximating predicate images for bit-vector logic. Zbl 1180.68175Kroening, Daniel; Sharygina, Natasha 4 2006 Verification of SpecC using predicate abstraction. Zbl 1117.68046Clarke, Edmund; Jain, Himanshu; Kroening, Daniel 4 2007 Instantiating uninterpreted functional units and memory system: Functional verification of the VAMP. Zbl 1179.68009Beyer, Sven; Jacobi, Chris; Kröning, Daniel; Leinenbach, Dirk; Paul, Wolfgang J. 4 2003 Cogent: Accurate theorem proving for program verification. Zbl 1081.68673Cook, Byron; Kroening, Daniel; Sharygina, Natasha 4 2005 Ranking function synthesis for bit-vector relations. Zbl 1291.68138Cook, Byron; Kroening, Daniel; Rümmer, Philipp; Wintersteiger, Christoph M. 4 2013 Unbounded-time analysis of guarded LTI systems with inputs by abstract acceleration. Zbl 1419.68041Cattaruzza, Dario; Abate, Alessandro; Schrammel, Peter; Kroening, Daniel 4 2015 Automatic generation of propagation complete SAT encodings. Zbl 1475.68218Brain, Martin; Hadarean, Liana; Kroening, Daniel; Martins, Ruben 4 2016 An abstract interpretation of DPLL(T). Zbl 1426.68249Brain, Martin; D’silva, Vijay; Haller, Leopold; Griggio, Alberto; Kroening, Daniel 3 2013 Computing over-approximations with bounded model checking. Zbl 1272.68264Kroening, Daniel 3 2006 Making the most of BMC counterexamples. Zbl 1272.68252Groce, Alex; Kroening, Daniel 3 2005 Unrestricted termination and non-termination arguments for bit-vector programs. Zbl 1335.68050David, Cristina; Kroening, Daniel; Lewis, Matt 3 2015 Automatic analysis of DMA races using model checking and \(k\)-induction. Zbl 1233.68124Donaldson, Alastair F.; Kroening, Daniel; Rümmer, Philipp 3 2011 SAT-based model checking. Zbl 1392.68232Biere, Armin; Kröning, Daniel 3 2018 Counterexample guided inductive synthesis modulo theories. Zbl 1511.68064Abate, Alessandro; David, Cristina; Kesseli, Pascal; Kroening, Daniel; Polgreen, Elizabeth 2 2018 Automated formal synthesis of provably safe digital controllers for continuous plants. Zbl 1441.93171Abate, Alessandro; Bessa, Iury; Cordeiro, Lucas; David, Cristina; Kesseli, Pascal; Kroening, Daniel; Polgreen, Elizabeth 2 2020 Learning the language of software errors. Zbl 1437.68071Chockler, Hana; Kesseli, Pascal; Kroening, Daniel; Strichman, Ofer 2 2020 Modular demand-driven analysis of semantic difference for program versions. Zbl 1420.68076Trostanetski, Anna; Grumberg, Orna; Kroening, Daniel 2 2017 Counterexample-guided abstraction refinement for symmetric concurrent programs. Zbl 1284.68179Donaldson, Alastair F.; Kaiser, Alexander; Kroening, Daniel; Tautschnig, Michael; Wahl, Thomas 2 2012 Loop summarization using state and transition invariants. Zbl 1291.68262Kroening, Daniel; Sharygina, Natasha; Tonetta, Stefano; Tsitovich, Aliaksei; Wintersteiger, Christoph M. 2 2013 Verification and falsification of programs with loops using predicate abstraction. Zbl 1215.68130Kroening, Daniel; Weissenbacher, Georg 2 2010 An algebraic algorithm for the identification of glass networks with periodic orbits along cyclic attractors. Zbl 1127.92004Zinovik, Igor; Kroening, Daniel; Chebiryak, Yury 2 2007 Approximation refinement for interpolation-based model checking. Zbl 1138.68444D’Silva, Vijay; Purandare, Mitra; Kroening, Daniel 2 2008 Context-aware counter abstraction. Zbl 1213.68362Basler, Gérard; Mazzucchi, Michele; Wahl, Thomas; Kroening, Daniel 2 2010 Strengthening induction-based race checking with lightweight static analysis. Zbl 1317.68113Donaldson, Alastair F.; Haller, Leopold; Kroening, Daniel 2 2011 Sound and automated synthesis of digital stabilizing controllers for continuous plants. Zbl 1369.93189Abate, Alessandro; Bessa, Iury; Cattaruzza, Dario; Cordeiro, Lucas; David, Cristina; Kesseli, Pascal; Kroening, Daniel 2 2017 Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration. Zbl 07356971Cattaruzza, Dario; Abate, Alessandro; Schrammel, Peter; Kroening, Daniel 1 2021 Proving safety with trace automata and bounded model checking. Zbl 1427.68047Kroening, Daniel; Lewis, Matt; Weissenbacher, Georg 1 2015 Certified reinforcement learning with logic guidance. Zbl 07732224Hasanbeig, Hosein; Kroening, Daniel; Abate, Alessandro 1 2023 On partial order semantics for SAT/SMT-based symbolic encodings of weak memory concurrency. Zbl 1347.68268Horn, Alex; Kroening, Daniel 1 2015 Lost in abstraction: monotonicity in multi-threaded programs. Zbl 1355.68055Kaiser, Alexander; Kroening, Daniel; Wahl, Thomas 1 2017 Incremental bounded model checking for embedded software. Zbl 1375.68081Schrammel, Peter; Kroening, Daniel; Brain, Martin; Martins, Ruben; Teige, Tino; Bienmüller, Tom 1 2017 Abstract interpretation with unfoldings. Zbl 1494.68044Sousa, Marcelo; Rodríguez, César; D’Silva, Vijay; Kroening, Daniel 1 2017 Lifting CDCL to template-based abstract domains for program verification. Zbl 1495.68139Mukherjee, Rajdeep; Schrammel, Peter; Haller, Leopold; Kroening, Daniel; Melham, Tom 1 2017 Certified reinforcement learning with logic guidance. Zbl 07732224Hasanbeig, Hosein; Kroening, Daniel; Abate, Alessandro 1 2023 Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration. Zbl 07356971Cattaruzza, Dario; Abate, Alessandro; Schrammel, Peter; Kroening, Daniel 1 2021 Deep reinforcement learning with temporal logics. Zbl 1455.68190Hasanbeig, Mohammadhosein; Kroening, Daniel; Abate, Alessandro 20 2020 A survey of safety and trustworthiness of deep neural networks: verification, testing, adversarial attack and defence, and interpretability. Zbl 1478.68308Huang, Xiaowei; Kroening, Daniel; Ruan, Wenjie; Sharp, James; Sun, Youcheng; Thamo, Emese; Wu, Min; Yi, Xinping 9 2020 Automated formal synthesis of provably safe digital controllers for continuous plants. Zbl 1441.93171Abate, Alessandro; Bessa, Iury; Cordeiro, Lucas; David, Cristina; Kesseli, Pascal; Kroening, Daniel; Polgreen, Elizabeth 2 2020 Learning the language of software errors. Zbl 1437.68071Chockler, Hana; Kesseli, Pascal; Kroening, Daniel; Strichman, Ofer 2 2020 Model checking. 2nd expanded and updated edition. Zbl 1423.68002Clarke, Edmund M. jun.; Grumberg, Orna; Kroening, Daniel; Peled, Doron; Veith, Helmut 64 2018 SAT-based model checking. Zbl 1392.68232Biere, Armin; Kröning, Daniel 3 2018 Counterexample guided inductive synthesis modulo theories. Zbl 1511.68064Abate, Alessandro; David, Cristina; Kesseli, Pascal; Kroening, Daniel; Polgreen, Elizabeth 2 2018 Modular demand-driven analysis of semantic difference for program versions. Zbl 1420.68076Trostanetski, Anna; Grumberg, Orna; Kroening, Daniel 2 2017 Sound and automated synthesis of digital stabilizing controllers for continuous plants. Zbl 1369.93189Abate, Alessandro; Bessa, Iury; Cattaruzza, Dario; Cordeiro, Lucas; David, Cristina; Kesseli, Pascal; Kroening, Daniel 2 2017 Lost in abstraction: monotonicity in multi-threaded programs. Zbl 1355.68055Kaiser, Alexander; Kroening, Daniel; Wahl, Thomas 1 2017 Incremental bounded model checking for embedded software. Zbl 1375.68081Schrammel, Peter; Kroening, Daniel; Brain, Martin; Martins, Ruben; Teige, Tino; Bienmüller, Tom 1 2017 Abstract interpretation with unfoldings. Zbl 1494.68044Sousa, Marcelo; Rodríguez, César; D’Silva, Vijay; Kroening, Daniel 1 2017 Lifting CDCL to template-based abstract domains for program verification. Zbl 1495.68139Mukherjee, Rajdeep; Schrammel, Peter; Haller, Leopold; Kroening, Daniel; Melham, Tom 1 2017 Decision procedures. An algorithmic point of view. 2nd edition. Zbl 1358.68002Kroening, Daniel; Strichman, Ofer 17 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 13 2016 Automatic generation of propagation complete SAT encodings. Zbl 1475.68218Brain, Martin; Hadarean, Liana; Kroening, Daniel; Martins, Ruben 4 2016 Learning the language of error. Zbl 1471.68101Chapman, Martin; Chockler, Hana; Kesseli, Pascal; Kroening, Daniel; Strichman, Ofer; Tautschnig, Michael 8 2015 Under-approximating loops in C programs for fast counterexample detection. Zbl 1322.68054Kroening, Daniel; Lewis, Matt; Weissenbacher, Georg 7 2015 Unfolding-based partial order reduction. Zbl 1374.68342Rodríguez, César; Sousa, Marcelo; Sharma, Subodh; Kroening, Daniel 6 2015 Unbounded-time analysis of guarded LTI systems with inputs by abstract acceleration. Zbl 1419.68041Cattaruzza, Dario; Abate, Alessandro; Schrammel, Peter; Kroening, Daniel 4 2015 Unrestricted termination and non-termination arguments for bit-vector programs. Zbl 1335.68050David, Cristina; Kroening, Daniel; Lewis, Matt 3 2015 Proving safety with trace automata and bounded model checking. Zbl 1427.68047Kroening, Daniel; Lewis, Matt; Weissenbacher, Georg 1 2015 On partial order semantics for SAT/SMT-based symbolic encodings of weak memory concurrency. Zbl 1347.68268Horn, Alex; Kroening, Daniel 1 2015 Deciding floating-point logic with abstract conflict driven clause learning. Zbl 1317.68110Brain, Martin; D’Silva, Vijay; Griggio, Alberto; Haller, Leopold; Kroening, Daniel 17 2014 Abstract satisfaction. Zbl 1284.68392D’Silva, Vijay; Haller, Leopold; Kroening, Daniel 5 2014 Software verification for weak memory via program transformation. Zbl 1381.68143Alglave, Jade; Kroening, Daniel; Nimal, Vincent; Tautschnig, Michael 17 2013 Abstract conflict driven learning. Zbl 1301.68156D’Silva, Vijay; Haller, Leopold; Kroening, Daniel 8 2013 Ranking function synthesis for bit-vector relations. Zbl 1291.68138Cook, Byron; Kroening, Daniel; Rümmer, Philipp; Wintersteiger, Christoph M. 4 2013 An abstract interpretation of DPLL(T). Zbl 1426.68249Brain, Martin; D’silva, Vijay; Haller, Leopold; Griggio, Alberto; Kroening, Daniel 3 2013 Loop summarization using state and transition invariants. Zbl 1291.68262Kroening, Daniel; Sharygina, Natasha; Tonetta, Stefano; Tsitovich, Aliaksei; Wintersteiger, Christoph M. 2 2013 Numeric bounds analysis with conflict-driven learning. Zbl 1352.68060D’Silva, Vijay; Haller, Leopold; Kroening, Daniel; Tautschnig, Michael 8 2012 Efficient coverability analysis by proof minimization. Zbl 1364.68138Kaiser, Alexander; Kroening, Daniel; Wahl, Thomas 6 2012 Counterexample-guided abstraction refinement for symmetric concurrent programs. Zbl 1284.68179Donaldson, Alastair F.; Kaiser, Alexander; Kroening, Daniel; Tautschnig, Michael; Wahl, Thomas 2 2012 Beyond quantifier-free interpolation in extensions of Presburger arithmetic. Zbl 1318.03045Brillout, Angelo; Kroening, Daniel; Rümmer, Philipp; Wahl, Thomas 11 2011 An interpolating sequent calculus for quantifier-free Presburger arithmetic. Zbl 1259.03043Brillout, Angelo; Kroening, Daniel; Rümmer, Philipp; Wahl, Thomas 9 2011 Loop summarization and termination analysis. Zbl 1315.68106Tsitovich, Aliaksei; Sharygina, Natasha; Wintersteiger, Christoph M.; Kroening, Daniel 7 2011 Linear completeness thresholds for bounded model checking. Zbl 1360.68592Kroening, Daniel; Ouaknine, Joël; Strichman, Ofer; Wahl, Thomas; Worrell, James 7 2011 Automatic analysis of DMA races using model checking and \(k\)-induction. Zbl 1233.68124Donaldson, Alastair F.; Kroening, Daniel; Rümmer, Philipp 3 2011 Strengthening induction-based race checking with lightweight static analysis. Zbl 1317.68113Donaldson, Alastair F.; Haller, Leopold; Kroening, Daniel 2 2011 Interpolant strength. Zbl 1273.68225D’Silva, Vijay; Kroening, Daniel; Purandare, Mitra; Weissenbacher, Georg 23 2010 An interpolating sequent calculus for quantifier-free Presburger arithmetic. Zbl 1291.03112Brillout, Angelo; Kroening, Daniel; Rümmer, Philipp; Wahl, Thomas 17 2010 Ranking function synthesis for bit-vector relations. Zbl 1284.68172Cook, Byron; Kroening, Daniel; Rümmer, Philipp; Wintersteiger, Christoph M. 11 2010 Interpolating quantifier-free Presburger arithmetic. Zbl 1306.68148Kroening, Daniel; Leroux, Jérôme; Rümmer, Philipp 5 2010 Periodic orbits and equilibria in Glass models for gene regulatory networks. Zbl 1366.92052Zinovik, Igor; Chebiryak, Yury; Kroening, Daniel 5 2010 Verification and falsification of programs with loops using predicate abstraction. Zbl 1215.68130Kroening, Daniel; Weissenbacher, Georg 2 2010 Context-aware counter abstraction. Zbl 1213.68362Basler, Gérard; Mazzucchi, Michele; Wahl, Thomas; Kroening, Daniel 2 2010 Symbolic counter abstraction for concurrent software. Zbl 1242.68055Basler, Gérard; Mazzucchi, Michele; Wahl, Thomas; Kroening, Daniel 9 2009 Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant. Zbl 1149.68071Kroening, Daniel; Strichman, Ofer 52 2008 Computing binary combinatorial Gray codes via exhaustive search with SAT solvers. Zbl 1328.94095Zinovik, Igor; Kroening, Daniel; Chebiryak, Yury 6 2008 Towards a classification of Hamiltonian cycles in the 6-cube. Zbl 1147.68703Chebiryak, Yury; Kroening, Daniel 6 2008 Loop summarization using abstract transformers. Zbl 1183.68377Kroening, Daniel; Sharygina, Natasha; Tonetta, Stefano; Tsitovich, Aliaksei; Wintersteiger, Christoph M. 5 2008 Approximation refinement for interpolation-based model checking. Zbl 1138.68444D’Silva, Vijay; Purandare, Mitra; Kroening, Daniel 2 2008 Deciding bit-vector arithmetic with abstraction. Zbl 1186.68281Bryant, Randal E.; Kroening, Daniel; Ouaknine, Joël; Seshia, Sanjit A.; Strichman, Ofer; Brady, Bryan 15 2007 A first step towards a unified proof checker for QBF. Zbl 1214.68334Jussila, Toni; Biere, Armin; Sinz, Carsten; Kröning, Daniel; Wintersteiger, Christoph M. 13 2007 Verification of Boolean programs with unbounded thread creation. Zbl 1143.68043Cook, Byron; Kroening, Daniel; Sharygina, Natasha 5 2007 Verification of SpecC using predicate abstraction. Zbl 1117.68046Clarke, Edmund; Jain, Himanshu; Kroening, Daniel 4 2007 An algebraic algorithm for the identification of glass networks with periodic orbits along cyclic attractors. Zbl 1127.92004Zinovik, Igor; Kroening, Daniel; Chebiryak, Yury 2 2007 Approximating predicate images for bit-vector logic. Zbl 1180.68175Kroening, Daniel; Sharygina, Natasha 4 2006 Computing over-approximations with bounded model checking. Zbl 1272.68264Kroening, Daniel 3 2006 SATABS: SAT-based predicate abstraction for ANSI-C. Zbl 1087.68586Clarke, Edmund; Kroening, Daniel; Sharygina, Natasha; Yorav, Karen 20 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 Making the most of BMC counterexamples. Zbl 1272.68252Groce, Alex; Kroening, Daniel 3 2005 A tool for checking ANSI-C programs. Zbl 1126.68470Clarke, Edmund; Kroening, Daniel; Lerda, Flavio 73 2004 Completeness and complexity of bounded model checking. Zbl 1202.68244Clarke, Edmund; Kroening, Daniel; Ouaknine, Joël; Strichman, Ofer 16 2004 Predicate abstraction of ANSI-C programs using SAT. Zbl 1090.68022Clarke, Edmund; Kroening, Daniel; Sharygina, Natasha; Yorav, Karen 16 2004 Understanding counterexamples with explain. Zbl 1103.68620Groce, Alex; Kroening, Daniel; Lerda, Flavio 6 2004 Abstraction-based satisfiability solving of Presburger arithmetic. Zbl 1103.68626Kroening, Daniel; Ouaknine, Joël; Seshia, Sanjit A.; Strichman, Ofer 5 2004 Efficient computation of recurrence diameters. Zbl 1022.68579Kroening, Daniel; Strichman, Ofer 9 2003 Instantiating uninterpreted functional units and memory system: Functional verification of the VAMP. Zbl 1179.68009Beyer, 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 969 Authors 33 Kröning, Daniel 11 Abate, Alessandro 11 Rümmer, Philipp 11 Sharygina, Natasha 8 Wahl, Thomas 7 Barrett, Clark W. 7 Biere, Armin 7 Bruttomesso, Roberto 7 Cimatti, Alessandro 7 Davenport, James Harold 7 Griggio, Alberto 7 Sebastiani, Roberto 7 Wintersteiger, Christoph M. 6 Ábrahám, Erika 6 England, Matthew 6 Frohn, Florian 6 Veith, Helmut 5 Atig, Mohamed Faouzi 5 Bonacina, Maria Paola 5 Giesl, Jürgen 5 Podelski, Andreas 5 Seshia, Sanjit Arunkumar 5 Strichman, Ofer 5 Tinelli, Cesare 5 Weissenbacher, Georg 4 Abdulla, Parosh Aziz 4 Bouajjani, Ahmed 4 Brain, Martin 4 Clarke, Edmund Melson jun. 4 D’silva, Vijay 4 Fisman, Dana 4 Ganesh, Vijay 4 Ghilardi, Silvio 4 Gurfinkel, Arie 4 Hensel, Jera 4 Henzinger, Thomas A. 4 Hoenicke, Jochen 4 Hyvärinen, Antti E. J. 4 King, Andy 4 Niemetz, Aina 4 Polgreen, Elizabeth 4 Preiner, Mathias 4 Ranise, Silvio 4 Reynolds, Andrew 4 Sturm, Thomas 4 Tsitovich, Aliaksei 4 Wehrheim, Heike 4 Wies, Thomas 3 Asadi, Sepideh 3 Becker, Bernd 3 Bozzano, Marco 3 Brauer, Jörg 3 Bright, Curtis 3 Brillout, Angelo 3 Brockschmidt, Marc 3 Chaki, Sagar 3 Chakraborty, Supratik 3 Chen, Mingshuai 3 Dasgupta, Pallab 3 Donaldson, Alastair F. 3 Fedyukovich, Grigory 3 Fujita, Masahiro 3 Gupta, Aarti 3 Haller, Leopold 3 Heule, Marijn J. H. 3 Johansson, Moa 3 Kapur, Deepak 3 Konnov, Igor V. 3 Kotsireas, Ilias S. 3 Kupferman, Orna 3 Monniaux, David P. 3 Rakamarić, Zvonimir 3 Rossi, Matteo A. C. 3 Schrammel, Peter 3 Strejček, Jan 3 Ströder, Thomas 3 Tonetta, Stefano 3 Trentin, Patrick 3 Wang, Bow-Yaw 3 Zaikin, Oleg Sergeevich 3 Zeljić, Aleksandar 3 Zhang, Lijun 2 Abbott, John A. 2 Ahmed, Daniele 2 Al-Bataineh, Omar 2 Angluin, Dana 2 Bagnara, Roberto 2 Balasubramanian, A. R. 2 Bardin, Sébastien 2 Bersani, Marcello Maria 2 Bigatti, Anna Maria 2 Blicha, Martin 2 Bloem, Roderick 2 Brown, Christopher W. 2 Brunet, Paul 2 Buchberger, Bruno 2 Byrnes, Kevin M. 2 Cattaruzza, Dario 2 Chatterjee, Krishnendu 2 Chen, Yu-Fang ...and 869 more Authors all top 5 Cited in 65 Serials 50 Formal Methods in System Design 36 Journal of Automated Reasoning 18 Formal Aspects of Computing 10 Journal of Logical and Algebraic Methods in Programming 9 Acta Informatica 9 Theoretical Computer Science 9 Logical Methods in Computer Science 6 Journal of Symbolic Computation 6 Information and Computation 5 Artificial Intelligence 4 Annals of Mathematics and Artificial Intelligence 4 Fundamenta Informaticae 4 Mathematics in Computer Science 3 Information Processing Letters 3 Automatica 3 Programming and Computer Software 3 Science of Computer Programming 3 The Journal of Artificial Intelligence Research (JAIR) 3 Theory of Computing Systems 2 Discrete Applied Mathematics 2 Journal of Computer and System Sciences 2 Journal of Computer Science and Technology 2 International Journal of Parallel Programming 2 AI Communications 2 Machine Learning 2 Discrete Event Dynamic Systems 2 Designs, Codes and Cryptography 2 The Electronic Journal of Combinatorics 2 Constraints 2 International Journal of Applied Mathematics and Computer Science 2 The Journal of Logic and Algebraic Programming 2 Theory and Practice of Logic 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 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 International Journal of Bifurcation and Chaos in Applied Sciences and Engineering 1 Cybernetics and Systems Analysis 1 INFORMS Journal on Computing 1 Optimization Methods & Software 1 Journal of Combinatorial Optimization 1 Journal of the ACM 1 Informatica (Vilnius) 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 SN Operations Research Forum all top 5 Cited in 23 Fields 407 Computer science (68-XX) 91 Mathematical logic and foundations (03-XX) 18 Information and communication theory, circuits (94-XX) 16 Combinatorics (05-XX) 14 Operations research, mathematical programming (90-XX) 12 Systems theory; control (93-XX) 9 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 5 General and overarching topics; collections (00-XX) 5 Order, lattices, ordered algebraic structures (06-XX) 5 Numerical analysis (65-XX) 5 Biology and other natural sciences (92-XX) 4 Statistics (62-XX) 3 Number theory (11-XX) 3 Ordinary differential equations (34-XX) 3 Probability theory and stochastic processes (60-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 Commutative algebra (13-XX) 1 Dynamical systems and ergodic theory (37-XX) 1 General topology (54-XX) 1 Fluid mechanics (76-XX) Citations by Year