×
Compute Distance To:
Author ID: kroning.daniel Recent zbMATH articles by "Kröning, Daniel"
Published as: Kroening, Daniel; Kröning, Daniel; Kroening, D.
External Links: ORCID
all top 5

Co-Authors

1 single-authored
11 Strichman, Ofer
11 Wahl, Thomas
9 D’silva, Vijay
9 Sharygina, Natasha
8 Rümmer, Philipp
7 Brain, Martin
7 Haller, Leopold
6 Clarke, Edmund Melson jun.
6 Cook, Byron
6 David, Cristina
6 Wintersteiger, Christoph M.
5 Abate, Alessandro
5 Chebiryak, Yury
5 Tautschnig, Michael
5 Weissenbacher, Georg
4 Brillout, Angelo
4 Griggio, Alberto
4 Kaiser, Alexander D.
4 Kesseli, Pascal
4 Ouaknine, Joel O.
4 Schrammel, Peter
3 Bessa, Iury
3 Cattaruzza, Dario
3 Cordeiro, Lucas
3 Donaldson, Alastair F.
3 Mazzucchi, Michele
3 Purandare, Mitra
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 Seiler, Werner M.
2 Seshia, Sanjit Arunkumar
2 Sousa, Marcelo S.
2 Sturm, Thomas
2 Tonetta, Stefano
2 Yorav, Karen
1 Alglave, Jade
1 Barner, Sharon
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, Mohammadhosein
1 He, Nannan
1 Horn, Alex
1 Huang, Xiaowei
1 Jacobi, Chris
1 Jain, Himanshu
1 Jussila, Toni
1 Khazem, Kareem
1 Kugler, Hillel
1 Leinenbach, Dirk C.
1 Leroux, Jérôme
1 Margaria, Tiziana
1 Müller, Silvia Melitta
1 Nimal, Vincent
1 Peled, Doron A.
1 Poetzl, Daniel
1 Polgreen, Elizabeth
1 Raz, Orna
1 Rodríguez, César
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 Tasiran, Serdar
1 Teige, Tino
1 Thamo, Emese
1 Trostanetski, Anna
1 Tuttle, Mark R.
1 Veith, Helmut
1 Woodcock, James C. P.
1 Worrell, James B.
...and 1 more Co-Authors

Publications by Year

Citations contained in zbMATH Open

62 Publications have been cited 476 times in 318 Documents Cited by Year
A tool for checking ANSI-C programs. Zbl 1126.68470
Clarke, Edmund; Kroening, Daniel; Lerda, Flavio
61
2004
Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant. Zbl 1149.68071
Kroening, Daniel; Strichman, Ofer
46
2008
Model checking. 2nd expanded and updated edition. Zbl 1423.68002
Clarke, Edmund M. jun.; Grumberg, Orna; Kroening, Daniel; Peled, Doron; Veith, Helmut
28
2018
SATABS: SAT-based predicate abstraction for ANSI-C. Zbl 1087.68586
Clarke, Edmund; Kroening, Daniel; Sharygina, Natasha; Yorav, Karen
21
2005
Interpolant strength. Zbl 1273.68225
D’Silva, Vijay; Kroening, Daniel; Purandare, Mitra; Weissenbacher, Georg
19
2010
Software verification for weak memory via program transformation. Zbl 1381.68143
Alglave, Jade; Kroening, Daniel; Nimal, Vincent; Tautschnig, Michael
16
2013
Completeness and complexity of bounded model checking. Zbl 1202.68244
Clarke, Edmund; Kroening, Daniel; Ouaknine, Joël; Strichman, Ofer
15
2004
An interpolating sequent calculus for quantifier-free Presburger arithmetic. Zbl 1291.03112
Brillout, Angelo; Kroening, Daniel; Rümmer, Philipp; Wahl, Thomas
13
2010
Predicate abstraction of ANSI-C programs using SAT. Zbl 1090.68022
Clarke, Edmund; Kroening, Daniel; Sharygina, Natasha; Yorav, Karen
13
2004
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.
12
2007
Deciding bit-vector arithmetic with abstraction. Zbl 1186.68281
Bryant, Randal E.; Kroening, Daniel; Ouaknine, Joël; Seshia, Sanjit A.; Strichman, Ofer; Brady, Bryan
12
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
11
2016
Ranking function synthesis for bit-vector relations. Zbl 1284.68172
Cook, Byron; Kroening, Daniel; Rümmer, Philipp; Wintersteiger, Christoph M.
11
2010
Beyond quantifier-free interpolation in extensions of Presburger arithmetic. Zbl 1318.03045
Brillout, Angelo; Kroening, Daniel; Rümmer, Philipp; Wahl, Thomas
10
2011
Decision procedures. An algorithmic point of view. 2nd edition. Zbl 1358.68002
Kroening, Daniel; Strichman, Ofer
10
2016
Deciding floating-point logic with abstract conflict driven clause learning. Zbl 1317.68110
Brain, Martin; D’Silva, Vijay; Griggio, Alberto; Haller, Leopold; Kroening, Daniel
9
2014
Efficient computation of recurrence diameters. Zbl 1022.68579
Kroening, Daniel; Strichman, Ofer
9
2003
Learning the language of error. Zbl 1471.68101
Chapman, Martin; Chockler, Hana; Kesseli, Pascal; Kroening, Daniel; Strichman, Ofer; Tautschnig, Michael
8
2015
Symbolic counter abstraction for concurrent software. Zbl 1242.68055
Basler, Gérard; Mazzucchi, Michele; Wahl, Thomas; Kroening, Daniel
8
2009
Numeric bounds analysis with conflict-driven learning. Zbl 1352.68060
D’Silva, Vijay; Haller, Leopold; Kroening, Daniel; Tautschnig, Michael
7
2012
An interpolating sequent calculus for quantifier-free Presburger arithmetic. Zbl 1259.03043
Brillout, Angelo; Kroening, Daniel; Rümmer, Philipp; Wahl, Thomas
7
2011
Abstract conflict driven learning. Zbl 1301.68156
D’Silva, Vijay; Haller, Leopold; Kroening, Daniel
6
2013
Linear completeness thresholds for bounded model checking. Zbl 1360.68592
Kroening, Daniel; Ouaknine, Joël; Strichman, Ofer; Wahl, Thomas; Worrell, James
6
2011
Computing binary combinatorial Gray codes via exhaustive search with SAT solvers. Zbl 1328.94095
Zinovik, Igor; Kroening, Daniel; Chebiryak, Yury
6
2008
Towards a classification of Hamiltonian cycles in the 6-cube. Zbl 1147.68703
Chebiryak, Yury; Kroening, Daniel
6
2008
Loop summarization and termination analysis. Zbl 1315.68106
Tsitovich, Aliaksei; Sharygina, Natasha; Wintersteiger, Christoph M.; Kroening, Daniel
5
2011
Interpolating quantifier-free Presburger arithmetic. Zbl 1306.68148
Kroening, Daniel; Leroux, Jérôme; Rümmer, Philipp
5
2010
Verification of Boolean programs with unbounded thread creation. Zbl 1143.68043
Cook, Byron; Kroening, Daniel; Sharygina, Natasha
5
2007
Understanding counterexamples with explain. Zbl 1103.68620
Groce, Alex; Kroening, Daniel; Lerda, Flavio
5
2004
Symbolic model checking for asynchronous Boolean programs. Zbl 1151.68367
Cook, Byron; Kroening, Daniel; Sharygina, Natasha
5
2005
Unfolding-based partial order reduction. Zbl 1374.68342
Rodríguez, César; Sousa, Marcelo; Sharma, Subodh; Kroening, Daniel
4
2015
Periodic orbits and equilibria in Glass models for gene regulatory networks. Zbl 1366.92052
Zinovik, Igor; Chebiryak, Yury; Kroening, Daniel
4
2010
Ranking function synthesis for bit-vector relations. Zbl 1291.68138
Cook, Byron; Kroening, Daniel; Rümmer, Philipp; Wintersteiger, Christoph M.
4
2013
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
Abstraction-based satisfiability solving of Presburger arithmetic. Zbl 1103.68626
Kroening, Daniel; Ouaknine, Joël; Seshia, Sanjit A.; Strichman, Ofer
4
2004
Approximating predicate images for bit-vector logic. Zbl 1180.68175
Kroening, Daniel; Sharygina, Natasha
4
2006
Loop summarization using abstract transformers. Zbl 1183.68377
Kroening, Daniel; Sharygina, Natasha; Tonetta, Stefano; Tsitovich, Aliaksei; Wintersteiger, Christoph M.
4
2008
Under-approximating loops in C programs for fast counterexample detection. Zbl 1322.68054
Kroening, Daniel; Lewis, Matt; Weissenbacher, Georg
3
2015
Automatic generation of propagation complete SAT encodings. Zbl 1475.68218
Brain, Martin; Hadarean, Liana; Kroening, Daniel; Martins, Ruben
3
2016
Abstract satisfaction. Zbl 1284.68392
D’Silva, Vijay; Haller, Leopold; Kroening, Daniel
3
2014
Unrestricted termination and non-termination arguments for bit-vector programs. Zbl 1335.68050
David, Cristina; Kroening, Daniel; Lewis, Matt
3
2015
An abstract interpretation of DPLL(T). Zbl 1426.68249
Brain, Martin; D’silva, Vijay; Haller, Leopold; Griggio, Alberto; Kroening, Daniel
3
2013
Computing over-approximations with bounded model checking. Zbl 1272.68264
Kroening, Daniel
3
2006
Cogent: Accurate theorem proving for program verification. Zbl 1081.68673
Cook, Byron; Kroening, Daniel; Sharygina, Natasha
3
2005
Verification of SpecC using predicate abstraction. Zbl 1117.68046
Clarke, Edmund; Jain, Himanshu; Kroening, Daniel
3
2007
Efficient coverability analysis by proof minimization. Zbl 1364.68138
Kaiser, Alexander; Kroening, Daniel; Wahl, Thomas
3
2012
SAT-based model checking. Zbl 1392.68232
Biere, Armin; Kröning, Daniel
3
2018
Counterexample-guided abstraction refinement for symmetric concurrent programs. Zbl 1284.68179
Donaldson, Alastair F.; Kaiser, Alexander; Kroening, Daniel; Tautschnig, Michael; Wahl, Thomas
2
2012
Context-aware counter abstraction. Zbl 1213.68362
Basler, Gérard; Mazzucchi, Michele; Wahl, Thomas; Kroening, Daniel
2
2010
Strengthening induction-based race checking with lightweight static analysis. Zbl 1317.68113
Donaldson, Alastair F.; Haller, Leopold; Kroening, Daniel
2
2011
Loop summarization using state and transition invariants. Zbl 1291.68262
Kroening, Daniel; Sharygina, Natasha; Tonetta, Stefano; Tsitovich, Aliaksei; Wintersteiger, Christoph M.
2
2013
Making the most of BMC counterexamples. Zbl 1272.68252
Groce, Alex; Kroening, Daniel
2
2005
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
Approximation refinement for interpolation-based model checking. Zbl 1138.68444
D’Silva, Vijay; Purandare, Mitra; Kroening, Daniel
2
2008
Deep reinforcement learning with temporal logics. Zbl 1455.68190
Hasanbeig, Mohammadhosein; Kroening, Daniel; Abate, Alessandro
2
2020
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
1
2017
Unbounded-time analysis of guarded LTI systems with inputs by abstract acceleration. Zbl 1419.68041
Cattaruzza, Dario; Abate, Alessandro; Schrammel, Peter; Kroening, Daniel
1
2015
Automatic analysis of DMA races using model checking and \(k\)-induction. Zbl 1233.68124
Donaldson, Alastair F.; Kroening, Daniel; Rümmer, Philipp
1
2011
Verification and falsification of programs with loops using predicate abstraction. Zbl 1215.68130
Kroening, Daniel; Weissenbacher, Georg
1
2010
On partial order semantics for SAT/SMT-based symbolic encodings of weak memory concurrency. Zbl 1347.68268
Horn, Alex; Kroening, Daniel
1
2015
Learning the language of software errors. Zbl 1437.68071
Chockler, Hana; Kesseli, Pascal; Kroening, Daniel; Strichman, Ofer
1
2020
Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration. Zbl 07356971
Cattaruzza, Dario; Abate, Alessandro; Schrammel, Peter; Kroening, Daniel
1
2021
Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration. Zbl 07356971
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
2
2020
Learning the language of software errors. Zbl 1437.68071
Chockler, Hana; Kesseli, Pascal; Kroening, Daniel; Strichman, Ofer
1
2020
Model checking. 2nd expanded and updated edition. Zbl 1423.68002
Clarke, Edmund M. jun.; Grumberg, Orna; Kroening, Daniel; Peled, Doron; Veith, Helmut
28
2018
SAT-based model checking. Zbl 1392.68232
Biere, Armin; Kröning, Daniel
3
2018
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
1
2017
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
11
2016
Decision procedures. An algorithmic point of view. 2nd edition. Zbl 1358.68002
Kroening, Daniel; Strichman, Ofer
10
2016
Automatic generation of propagation complete SAT encodings. Zbl 1475.68218
Brain, Martin; Hadarean, Liana; Kroening, Daniel; Martins, Ruben
3
2016
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
4
2015
Under-approximating loops in C programs for fast counterexample detection. Zbl 1322.68054
Kroening, Daniel; Lewis, Matt; Weissenbacher, Georg
3
2015
Unrestricted termination and non-termination arguments for bit-vector programs. Zbl 1335.68050
David, Cristina; Kroening, Daniel; Lewis, Matt
3
2015
Unbounded-time analysis of guarded LTI systems with inputs by abstract acceleration. Zbl 1419.68041
Cattaruzza, Dario; Abate, Alessandro; Schrammel, Peter; Kroening, Daniel
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
9
2014
Abstract satisfaction. Zbl 1284.68392
D’Silva, Vijay; Haller, Leopold; Kroening, Daniel
3
2014
Software verification for weak memory via program transformation. Zbl 1381.68143
Alglave, Jade; Kroening, Daniel; Nimal, Vincent; Tautschnig, Michael
16
2013
Abstract conflict driven learning. Zbl 1301.68156
D’Silva, Vijay; Haller, Leopold; Kroening, Daniel
6
2013
Ranking function synthesis for bit-vector relations. Zbl 1291.68138
Cook, Byron; Kroening, Daniel; Rümmer, Philipp; Wintersteiger, Christoph M.
4
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
Numeric bounds analysis with conflict-driven learning. Zbl 1352.68060
D’Silva, Vijay; Haller, Leopold; Kroening, Daniel; Tautschnig, Michael
7
2012
Efficient coverability analysis by proof minimization. Zbl 1364.68138
Kaiser, Alexander; Kroening, Daniel; Wahl, Thomas
3
2012
Counterexample-guided abstraction refinement for symmetric concurrent programs. Zbl 1284.68179
Donaldson, Alastair F.; Kaiser, Alexander; Kroening, Daniel; Tautschnig, Michael; Wahl, Thomas
2
2012
Beyond quantifier-free interpolation in extensions of Presburger arithmetic. Zbl 1318.03045
Brillout, Angelo; Kroening, Daniel; Rümmer, Philipp; Wahl, Thomas
10
2011
An interpolating sequent calculus for quantifier-free Presburger arithmetic. Zbl 1259.03043
Brillout, Angelo; Kroening, Daniel; Rümmer, Philipp; Wahl, Thomas
7
2011
Linear completeness thresholds for bounded model checking. Zbl 1360.68592
Kroening, Daniel; Ouaknine, Joël; Strichman, Ofer; Wahl, Thomas; Worrell, James
6
2011
Loop summarization and termination analysis. Zbl 1315.68106
Tsitovich, Aliaksei; Sharygina, Natasha; Wintersteiger, Christoph M.; Kroening, Daniel
5
2011
Strengthening induction-based race checking with lightweight static analysis. Zbl 1317.68113
Donaldson, Alastair F.; Haller, Leopold; Kroening, Daniel
2
2011
Automatic analysis of DMA races using model checking and \(k\)-induction. Zbl 1233.68124
Donaldson, Alastair F.; Kroening, Daniel; Rümmer, Philipp
1
2011
Interpolant strength. Zbl 1273.68225
D’Silva, Vijay; Kroening, Daniel; Purandare, Mitra; Weissenbacher, Georg
19
2010
An interpolating sequent calculus for quantifier-free Presburger arithmetic. Zbl 1291.03112
Brillout, Angelo; Kroening, Daniel; Rümmer, Philipp; Wahl, Thomas
13
2010
Ranking function synthesis for bit-vector relations. Zbl 1284.68172
Cook, Byron; Kroening, Daniel; Rümmer, Philipp; Wintersteiger, Christoph M.
11
2010
Interpolating quantifier-free Presburger arithmetic. Zbl 1306.68148
Kroening, Daniel; Leroux, Jérôme; Rümmer, Philipp
5
2010
Periodic orbits and equilibria in Glass models for gene regulatory networks. Zbl 1366.92052
Zinovik, Igor; Chebiryak, Yury; Kroening, Daniel
4
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
1
2010
Symbolic counter abstraction for concurrent software. Zbl 1242.68055
Basler, Gérard; Mazzucchi, Michele; Wahl, Thomas; Kroening, Daniel
8
2009
Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant. Zbl 1149.68071
Kroening, Daniel; Strichman, Ofer
46
2008
Computing binary combinatorial Gray codes via exhaustive search with SAT solvers. Zbl 1328.94095
Zinovik, Igor; Kroening, Daniel; Chebiryak, Yury
6
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.
4
2008
Approximation refinement for interpolation-based model checking. Zbl 1138.68444
D’Silva, Vijay; Purandare, Mitra; Kroening, Daniel
2
2008
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.
12
2007
Deciding bit-vector arithmetic with abstraction. Zbl 1186.68281
Bryant, Randal E.; Kroening, Daniel; Ouaknine, Joël; Seshia, Sanjit A.; Strichman, Ofer; Brady, Bryan
12
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
3
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
4
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
21
2005
Symbolic model checking for asynchronous Boolean programs. Zbl 1151.68367
Cook, Byron; Kroening, Daniel; Sharygina, Natasha
5
2005
Cogent: Accurate theorem proving for program verification. Zbl 1081.68673
Cook, Byron; Kroening, Daniel; Sharygina, Natasha
3
2005
Making the most of BMC counterexamples. Zbl 1272.68252
Groce, Alex; Kroening, Daniel
2
2005
A tool for checking ANSI-C programs. Zbl 1126.68470
Clarke, Edmund; Kroening, Daniel; Lerda, Flavio
61
2004
Completeness and complexity of bounded model checking. Zbl 1202.68244
Clarke, Edmund; Kroening, Daniel; Ouaknine, Joël; Strichman, Ofer
15
2004
Predicate abstraction of ANSI-C programs using SAT. Zbl 1090.68022
Clarke, Edmund; Kroening, Daniel; Sharygina, Natasha; Yorav, Karen
13
2004
Understanding counterexamples with explain. Zbl 1103.68620
Groce, Alex; Kroening, Daniel; Lerda, Flavio
5
2004
Abstraction-based satisfiability solving of Presburger arithmetic. Zbl 1103.68626
Kroening, Daniel; Ouaknine, Joël; Seshia, Sanjit A.; Strichman, Ofer
4
2004
Efficient computation of recurrence diameters. Zbl 1022.68579
Kroening, Daniel; Strichman, Ofer
9
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 top 5

Cited by 724 Authors

30 Kröning, Daniel
11 Rümmer, Philipp
8 Sharygina, Natasha
7 Biere, Armin
7 Davenport, James Harold
7 Wahl, Thomas
7 Wintersteiger, Christoph M.
6 Bruttomesso, Roberto
6 England, Matthew
6 Sebastiani, Roberto
5 Abate, Alessandro
5 Ábrahám, Erika
5 Bonacina, Maria Paola
5 Cimatti, Alessandro
5 Griggio, Alberto
5 Strichman, Ofer
5 Veith, Helmut
4 Atig, Mohamed Faouzi
4 Bouajjani, Ahmed
4 Brain, Martin
4 Clarke, Edmund Melson jun.
4 D’silva, Vijay
4 Frohn, Florian
4 Giesl, Jürgen
4 Hensel, Jera
4 Podelski, Andreas
4 Ranise, Silvio
4 Sturm, Thomas
4 Tsitovich, Aliaksei
4 Weissenbacher, Georg
3 Abdulla, Parosh Aziz
3 Barrett, Clark W.
3 Becker, Bernd
3 Brauer, Jörg
3 Bright, Curtis
3 Brillout, Angelo
3 Brockschmidt, Marc
3 Chaki, Sagar
3 Chakraborty, Supratik
3 Cook, Byron
3 Dasgupta, Pallab
3 Donaldson, Alastair F.
3 Fisman, Dana
3 Ganesh, Vijay
3 Ghilardi, Silvio
3 Gupta, Aarti
3 Gurfinkel, Arie
3 Haller, Leopold
3 Hoenicke, Jochen
3 Johansson, Moa
3 Konnov, Igor V.
3 Kotsireas, Ilias S.
3 Niemetz, Aina
3 Preiner, Mathias
3 Rossi, Matteo A. C.
3 Ströder, Thomas
3 Tinelli, Cesare
3 Wies, Thomas
3 Zeljić, Aleksandar
3 Zhang, Lijun
2 Abbott, John A.
2 Angluin, Dana
2 Bersani, Marcello Maria
2 Bigatti, Anna Maria
2 Bozzano, Marco
2 Brunet, Paul
2 Buchberger, Bruno
2 Byrnes, Kevin M.
2 Chen, Yu-Fang
2 de Moura, Leonardo
2 Dixit, Manoj G.
2 Enea, Constantin
2 Fontaine, Pascal
2 Forrest, Stephen
2 Fox, Anthony C. J.
2 Fujita, Masahiro
2 Ganai, Malay K.
2 Grumberg, Orna
2 Gupta, Ashutosh
2 Hamadi, Youssef
2 Henzinger, Thomas A.
2 Heule, Marijn J. H.
2 Hoos, Holger H.
2 Huang, Chengchao
2 Jain, Himanshu
2 Jonáš, Martin
2 Junttila, Tommi A.
2 Kaiser, Alexander D.
2 Kappé, Tobias
2 King, Andy
2 Kochemazov, Stepan
2 Kremer, Gereon
2 Leino, K. Rustan M.
2 Leyton-Brown, Kevin
2 Liu, Depeng
2 Lonsing, Florian
2 Malik, Sharad
2 Mandrykin, M. U.
2 Mazzucchi, Michele
2 Meseguer Guaita, José
...and 624 more Authors
all top 5

Cited in 55 Serials

44 Formal Methods in System Design
34 Journal of Automated Reasoning
14 Formal Aspects of Computing
10 Journal of Logical and Algebraic Methods in Programming
8 Acta Informatica
8 Theoretical Computer Science
5 Journal of Symbolic Computation
5 Information and Computation
5 Logical Methods in Computer Science
4 Artificial Intelligence
4 Annals of Mathematics and Artificial Intelligence
4 Mathematics in Computer Science
3 Information Processing Letters
3 Programming and Computer Software
3 Science of Computer Programming
3 Theory of Computing Systems
3 Fundamenta Informaticae
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 Designs, Codes and Cryptography
2 The Electronic Journal of Combinatorics
2 The Journal of Artificial Intelligence Research (JAIR)
2 Theory and Practice of Logic Programming
2 Computer Languages, Systems & Structures
2 Journal of Applied Logic
1 ACM Computing Surveys
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 Machine Learning
1 Discrete Event Dynamic Systems
1 International Journal of Bifurcation and Chaos in Applied Sciences and Engineering
1 Cybernetics and Systems Analysis
1 Constraints
1 INFORMS Journal on Computing
1 Journal of Combinatorial Optimization
1 Journal of the ACM
1 Informatica (Vilnius)
1 International Journal of Applied Mathematics and Computer Science
1 The Journal of Logic and Algebraic Programming
1 Journal of Applied Mathematics
1 ACM Transactions on Computational Logic
1 ACM Journal of Experimental Algorithmics
1 Journal of Zhejiang University. Science A
1 Journal of Satisfiability, Boolean Modeling and Computation
1 ACM Communications in Computer Algebra
1 Diskretnyĭ Analiz i Issledovanie Operatsiĭ
1 Central European Journal of Computer Science
1 SN Operations Research Forum

Citations by Year