Chockler, Hana; Kesseli, Pascal; Kroening, Daniel; Strichman, Ofer Learning the language of software errors. (English) Zbl 1437.68071 J. Artif. Intell. Res. (JAIR) 67, 881-903 (2020). MSC: 68Q32 68N30 68Q45 68Q60 PDFBibTeX XMLCite \textit{H. Chockler} et al., J. Artif. Intell. Res. (JAIR) 67, 881--903 (2020; Zbl 1437.68071) Full Text: DOI
Abate, Alessandro; David, Cristina; Kesseli, Pascal; Kroening, Daniel; Polgreen, Elizabeth Counterexample guided inductive synthesis modulo theories. (English) Zbl 1511.68064 Chockler, Hana (ed.) et al., Computer aided verification. 30th international conference, CAV 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 14–17, 2018. Proceedings. Part I. Cham: Springer Open. Lect. Notes Comput. Sci. 10981, 270-288 (2018). MSC: 68N30 PDFBibTeX XMLCite \textit{A. Abate} et al., Lect. Notes Comput. Sci. 10981, 270--288 (2018; Zbl 1511.68064) Full Text: DOI
Mukherjee, Rajdeep; Schrammel, Peter; Haller, Leopold; Kroening, Daniel; Melham, Tom Lifting CDCL to template-based abstract domains for program verification. (English) Zbl 1495.68139 D’Souza, Deepak (ed.) et al., Automated technology for verification and analysis. 15th international symposium, ATVA 2017, Pune, India, October 3–6, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10482, 307-326 (2017). MSC: 68Q60 68N30 68Q32 68T20 PDFBibTeX XMLCite \textit{R. Mukherjee} et al., Lect. Notes Comput. Sci. 10482, 307--326 (2017; Zbl 1495.68139) Full Text: DOI arXiv Link
Trostanetski, Anna; Grumberg, Orna; Kroening, Daniel Modular demand-driven analysis of semantic difference for program versions. (English) Zbl 1420.68076 Ranzato, Francesco (ed.), Static analysis. 24th international symposium, SAS 2017, New York, NY, USA, August 30 – September 1, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10422, 405-427 (2017). MSC: 68N30 68Q55 PDFBibTeX XMLCite \textit{A. Trostanetski} et al., Lect. Notes Comput. Sci. 10422, 405--427 (2017; Zbl 1420.68076) Full Text: DOI Link
Kaiser, Alexander; Kroening, Daniel; Wahl, Thomas Lost in abstraction: monotonicity in multi-threaded programs. (English) Zbl 1355.68055 Inf. Comput. 252, 30-47 (2017). MSC: 68N30 68Q60 68Q85 PDFBibTeX XMLCite \textit{A. Kaiser} et al., Inf. Comput. 252, 30--47 (2017; Zbl 1355.68055) Full Text: DOI
Poetzl, Daniel; Kroening, Daniel Formalizing and checking thread refinement for data-race-free execution models. (English) Zbl 1420.68072 Chechik, Marsha (ed.) et al., Tools and algorithms for the construction and analysis of systems. 22nd international conference, TACAS 2016, held as part of the European joint conferences on theory and practice of software, ETAPS 2016, Eindhoven, The Netherlands, April 2–8, 2016. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 9636, 515-530 (2016). MSC: 68N30 68N19 68Q85 PDFBibTeX XMLCite \textit{D. Poetzl} and \textit{D. Kroening}, Lect. Notes Comput. Sci. 9636, 515--530 (2016; Zbl 1420.68072) Full Text: DOI arXiv Link
Kroening, Daniel; Lewis, Matt; Weissenbacher, Georg Proving safety with trace automata and bounded model checking. (English) Zbl 1427.68047 Bjørner, Nikolaj (ed.) et al., FM 2015: formal methods. 20th international symposium, Oslo, Norway, June 24–26, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9109, 325-341 (2015). MSC: 68N30 68Q45 68Q60 PDFBibTeX XMLCite \textit{D. Kroening} et al., Lect. Notes Comput. Sci. 9109, 325--341 (2015; Zbl 1427.68047) Full Text: DOI arXiv
David, Cristina; Kroening, Daniel; Lewis, Matt Propositional reasoning about safety and termination of heap-manipulating programs. (English) Zbl 1335.68051 Vitek, Jan (ed.), Programming languages and systems. 24th European symposium on programming, ESOP 2015, held as part of the European joint conferences on theory and practice of software, ETAPS 2015, London, UK, April 11–18, 2015. Proceedings. Berlin: Springer (ISBN 978-3-662-46668-1/pbk; 978-3-662-46669-8/ebook). Lecture Notes in Computer Science 9032, 661-684 (2015). MSC: 68N30 PDFBibTeX XMLCite \textit{C. David} et al., Lect. Notes Comput. Sci. 9032, 661--684 (2015; Zbl 1335.68051) Full Text: DOI arXiv
David, Cristina; Kroening, Daniel; Lewis, Matt Unrestricted termination and non-termination arguments for bit-vector programs. (English) Zbl 1335.68050 Vitek, Jan (ed.), Programming languages and systems. 24th European symposium on programming, ESOP 2015, held as part of the European joint conferences on theory and practice of software, ETAPS 2015, London, UK, April 11–18, 2015. Proceedings. Berlin: Springer (ISBN 978-3-662-46668-1/pbk; 978-3-662-46669-8/ebook). Lecture Notes in Computer Science 9032, 183-204 (2015). MSC: 68N30 PDFBibTeX XMLCite \textit{C. David} et al., Lect. Notes Comput. Sci. 9032, 183--204 (2015; Zbl 1335.68050) Full Text: DOI arXiv
David, Cristina; Kroening, Daniel; Lewis, Matt Using program synthesis for program analysis. (English) Zbl 1471.68056 Davis, Martin (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 20th international conference, LPAR-20 2015, Suva, Fiji, November 24–28, 2015. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 9450, 483-498 (2015). MSC: 68N30 03B70 PDFBibTeX XMLCite \textit{C. David} et al., Lect. Notes Comput. Sci. 9450, 483--498 (2015; Zbl 1471.68056) Full Text: DOI arXiv
Chapman, Martin; Chockler, Hana; Kesseli, Pascal; Kroening, Daniel; Strichman, Ofer; Tautschnig, Michael Learning the language of error. (English) Zbl 1471.68101 Finkbeiner, Bernd (ed.) et al., Automated technology for verification and analysis. 13th international symposium, ATVA 2015, Shanghai, China, October 12–15, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9364, 114-130 (2015). MSC: 68Q32 68N30 68Q45 PDFBibTeX XMLCite \textit{M. Chapman} et al., Lect. Notes Comput. Sci. 9364, 114--130 (2015; Zbl 1471.68101) Full Text: DOI
Kroening, Daniel; Lewis, Matt; Weissenbacher, Georg Under-approximating loops in C programs for fast counterexample detection. (English) Zbl 1322.68054 Form. Methods Syst. Des. 47, No. 1, 75-92 (2015). MSC: 68N30 68Q60 PDFBibTeX XMLCite \textit{D. Kroening} et al., Form. Methods Syst. Des. 47, No. 1, 75--92 (2015; Zbl 1322.68054) Full Text: DOI
Brain, Martin; David, Cristina; Kroening, Daniel; Schrammel, Peter Model and proof generation for heap-manipulating programs. (English) Zbl 1405.68072 Shao, Zhong (ed.), Programming languages and systems. 23rd European symposium on programming, ESOP 2014, held as part of the European joint conferences on theory and practice of software, ETAPS 2014, Grenoble, France, April 5–13, 2014. Proceedings. Berlin: Springer (ISBN 978-3-642-54832-1/pbk). Lecture Notes in Computer Science 8410, 432-452 (2014). MSC: 68N30 68P05 PDFBibTeX XMLCite \textit{M. Brain} et al., Lect. Notes Comput. Sci. 8410, 432--452 (2014; Zbl 1405.68072) Full Text: DOI
D’Silva, Vijay; Haller, Leopold; Kroening, Daniel Abstract conflict driven learning. (English) Zbl 1301.68156 Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’13, Rome, Italy, January 23–25, 2013. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-1832-7). 143-154 (2013). MSC: 68Q25 06B99 68N30 68Q60 68T05 PDFBibTeX XMLCite \textit{V. D'Silva} et al., in: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL '13, Rome, Italy, January 23--25, 2013. New York, NY: Association for Computing Machinery (ACM). 143--154 (2013; Zbl 1301.68156) Full Text: DOI
D’Silva, Vijay; Kroening, Daniel Abstraction of syntax. (English) Zbl 1426.68157 Giacobazzi, Roberto (ed.) et al., Verification, model checking, and abstract interpretation. 14th international conference, VMCAI 2013, Rome, Italy, January 20–22, 2013. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 7737, 396-413 (2013). MSC: 68Q55 68N30 PDFBibTeX XMLCite \textit{V. D'Silva} and \textit{D. Kroening}, Lect. Notes Comput. Sci. 7737, 396--413 (2013; Zbl 1426.68157) Full Text: DOI
Cook, Byron; Kroening, Daniel; Rümmer, Philipp; Wintersteiger, Christoph M. Ranking function synthesis for bit-vector relations. (English) Zbl 1291.68138 Form. Methods Syst. Des. 43, No. 1, 93-120 (2013). MSC: 68N30 68T20 PDFBibTeX XMLCite \textit{B. Cook} et al., Form. Methods Syst. Des. 43, No. 1, 93--120 (2013; Zbl 1291.68138) Full Text: DOI
Kroening, Daniel; Sharygina, Natasha; Tonetta, Stefano; Tsitovich, Aliaksei; Wintersteiger, Christoph M. Loop summarization using state and transition invariants. (English) Zbl 1291.68262 Form. Methods Syst. Des. 42, No. 3, 221-261 (2013). MSC: 68Q60 68N30 PDFBibTeX XMLCite \textit{D. Kroening} et al., Form. Methods Syst. Des. 42, No. 3, 221--261 (2013; Zbl 1291.68262) Full Text: DOI Link
Seghir, Mohamed Nassim; Kroening, Daniel Counterexample-guided precondition inference. (English) Zbl 1381.68180 Felleisen, Matthias (ed.) et al., Programming languages and systems. 22nd European symposium on programming, ESOP 2013, held as part of the European joint conferences on theory and practice of software, ETAPS 2013, Rome, Italy, March 16–24, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-37035-9/pbk). Lecture Notes in Computer Science 7792, 451-471 (2013). MSC: 68Q60 68N30 PDFBibTeX XMLCite \textit{M. N. Seghir} and \textit{D. Kroening}, Lect. Notes Comput. Sci. 7792, 451--471 (2013; Zbl 1381.68180) Full Text: DOI
Donaldson, Alastair F.; Kaiser, Alexander; Kroening, Daniel; Tautschnig, Michael; Wahl, Thomas Counterexample-guided abstraction refinement for symmetric concurrent programs. (English) Zbl 1284.68179 Form. Methods Syst. Des. 41, No. 1, 25-44 (2012). MSC: 68N30 68Q60 68N19 68Q85 PDFBibTeX XMLCite \textit{A. F. Donaldson} et al., Form. Methods Syst. Des. 41, No. 1, 25--44 (2012; Zbl 1284.68179) Full Text: DOI Link
Kaiser, Alexander; Kroening, Daniel; Wahl, Thomas Efficient coverability analysis by proof minimization. (English) Zbl 1364.68138 Koutny, Maciej (ed.) et al., CONCUR 2012 – concurrency theory. 23rd international conference, CONCUR 2012, Newcastle upon Tyne, UK, September 4–7, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-32939-5/pbk). Lecture Notes in Computer Science 7454, 500-515 (2012). MSC: 68N30 68Q60 68Q85 PDFBibTeX XMLCite \textit{A. Kaiser} et al., Lect. Notes Comput. Sci. 7454, 500--515 (2012; Zbl 1364.68138) Full Text: DOI
D’Silva, Vijay; Haller, Leopold; Kroening, Daniel; Tautschnig, Michael Numeric bounds analysis with conflict-driven learning. (English) Zbl 1352.68060 Flanagan, Cormac (ed.) et al., Tools and algorithms for the construction and analysis of systems. 18th international conference, TACAS 2012, held as part of the European joint conferences on theory and practice of software, ETAPS 2012, Tallinn, Estonia, March 24 – April 1, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-28755-8/pbk). Lecture Notes in Computer Science 7214, 48-63 (2012). MSC: 68N30 65G40 PDFBibTeX XMLCite \textit{V. D'Silva} et al., Lect. Notes Comput. Sci. 7214, 48--63 (2012; Zbl 1352.68060) Full Text: DOI
Donaldson, Alastair F.; Kroening, Daniel; Rümmer, Philipp Automatic analysis of DMA races using model checking and \(k\)-induction. (English) Zbl 1233.68124 Form. Methods Syst. Des. 39, No. 1, 83-113 (2011). MSC: 68N30 68Q60 68N19 PDFBibTeX XMLCite \textit{A. F. Donaldson} et al., Form. Methods Syst. Des. 39, No. 1, 83--113 (2011; Zbl 1233.68124) Full Text: DOI
Kroening, Daniel (ed.); Margaria, Tiziana (ed.); Woodcock, Jim (ed.) Special issue: Workshop on tools at VSTTE 2008. Selected papers based on the presentations at the conference on verified software: theories, tools and experiments, Toronto, Canada, October 6–9, 2008. (English) Zbl 1243.68021 Formal Asp. Comput. 23, No. 5, 585-679 (2011). MSC: 68-06 68Q60 68N30 00B25 PDFBibTeX XML
Tsitovich, Aliaksei; Sharygina, Natasha; Wintersteiger, Christoph M.; Kroening, Daniel Loop summarization and termination analysis. (English) Zbl 1315.68106 Abdulla, Parosh Aziz (ed.) et al., Tools and algorithms for the construction and analysis of systems. 17th international conference, TACAS 2011, held as part of the joint European conferences on theory and practice of software, ETAPS 2011, Saarbrücken, Germany, March 26 – April 3, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-19834-2/pbk). Lecture Notes in Computer Science 6605, 81-95 (2011). MSC: 68N30 PDFBibTeX XMLCite \textit{A. Tsitovich} et al., Lect. Notes Comput. Sci. 6605, 81--95 (2011; Zbl 1315.68106) Full Text: DOI
Barner, Sharon (ed.); Harris, Ian (ed.); Kroening, Daniel (ed.); Raz, Orna (ed.) Hardware and software: verification and testing. 6th international Haifa verification conference, HVC 2010, Haifa, Israel, October 4–7, 2010. Revised selected papers. (English) Zbl 1209.68002 Lecture Notes in Computer Science 6504. Berlin: Springer (ISBN 978-3-642-19582-2/pbk). x, 197 p. (2011). MSC: 68-06 68N30 68Q60 00B25 PDFBibTeX XMLCite \textit{S. Barner} (ed.) et al., Hardware and software: verification and testing. 6th international Haifa verification conference, HVC 2010, Haifa, Israel, October 4--7, 2010. Revised selected papers. Berlin: Springer (2011; Zbl 1209.68002) Full Text: DOI
Brillout, Angelo; He, Nannan; Mazzucchi, Michele; Kroening, Daniel; Purandare, Mitra; Rümmer, Philipp; Weissenbacher, Georg Mutation-based test case generation for Simulink models. (English) Zbl 1312.68130 de Boer, Frank S. (ed.) et al., Formal methods for components and objects. 8th international symposium, FMCO 2009, Eindhoven, The Netherlands, November 4–6, 2009. Revised selected papers. Berlin: Springer (ISBN 978-3-642-17070-6/pbk). Lecture Notes in Computer Science 6286, 208-227 (2010). MSC: 68Q60 68N99 PDFBibTeX XMLCite \textit{A. Brillout} et al., Lect. Notes Comput. Sci. 6286, 208--227 (2010; Zbl 1312.68130) Full Text: DOI
Cook, Byron; Kroening, Daniel; Rümmer, Philipp; Wintersteiger, Christoph M. Ranking function synthesis for bit-vector relations. (English) Zbl 1284.68172 Esparza, Javier (ed.) et al., Tools and algorithms for the construction and analysis of systems. 16th international conference, TACAS 2010, held as part of the joint European conferences on theory and practice of software, ETAPS 2010, Paphos, Cyprus, March 20–28, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-12001-5/pbk). Lecture Notes in Computer Science 6015, 236-250 (2010). MSC: 68N30 03B70 PDFBibTeX XMLCite \textit{B. Cook} et al., Lect. Notes Comput. Sci. 6015, 236--250 (2010; Zbl 1284.68172) Full Text: DOI
Cook, Byron; Kroening, Daniel; Sharygina, Natasha Verification of Boolean programs with unbounded thread creation. (English) Zbl 1143.68043 Theor. Comput. Sci. 388, No. 1-3, 227-242 (2007). MSC: 68Q60 68N30 68Q55 PDFBibTeX XMLCite \textit{B. Cook} et al., Theor. Comput. Sci. 388, No. 1--3, 227--242 (2007; Zbl 1143.68043) Full Text: DOI
Kroening, Daniel; Sharygina, Natasha Approximating predicate images for bit-vector logic. (English) Zbl 1180.68175 Hermanns, Holger (ed.) et al., Tools and algorithms for the construction and analysis of systems. 12th international conference, TACAS 2006, held as part of the joint European conferences on theory and practice of software, ETAPS 2006, Vienna, Austria, March 25 – April 2, 2006. Proceedings. Berlin: Springer (ISBN 3-540-33056-9/pbk). Lecture Notes in Computer Science 3920, 242-256 (2006). MSC: 68Q60 03B70 68N30 PDFBibTeX XMLCite \textit{D. Kroening} and \textit{N. Sharygina}, Lect. Notes Comput. Sci. 3920, 242--256 (2006; Zbl 1180.68175) Full Text: DOI
Cook, Byron; Kroening, Daniel; Sharygina, Natasha Symbolic model checking for asynchronous Boolean programs. (English) Zbl 1151.68367 Godefroid, Patrice (ed.), Model checking software. 12th international SPIN workshop, San Francisco, CA, USA, August 22–24, 2005. Proceedings. Berlin: Springer (ISBN 3-540-28195-9/pbk). Lecture Notes in Computer Science 3639, 75-90 (2005). MSC: 68N30 68Q60 PDFBibTeX XMLCite \textit{B. Cook} et al., Lect. Notes Comput. Sci. 3639, 75--90 (2005; Zbl 1151.68367) Full Text: DOI
Cook, Byron; Kroening, Daniel; Sharygina, Natasha Cogent: Accurate theorem proving for program verification. (English) Zbl 1081.68673 Etessami, Kousha (ed.) et al., Computer aided verification. 17th international conference, CAV 2005, Edinburgh, Scotland, UK, July 6–10, 2005. Proceedings. Berlin: Springer (ISBN 3-540-27231-3/pbk). Lecture Notes in Computer Science 3576, 296-300 (2005). MSC: 68T15 68N99 68Q60 PDFBibTeX XMLCite \textit{B. Cook} et al., Lect. Notes Comput. Sci. 3576, 296--300 (2005; Zbl 1081.68673) Full Text: DOI
Clarke, Edmund; Kroening, Daniel; Sharygina, Natasha; Yorav, Karen Predicate abstraction of ANSI-C programs using SAT. (English) Zbl 1090.68022 Form. Methods Syst. Des. 25, No. 2-3, 105-127 (2004). MSC: 68N30 68Q60 PDFBibTeX XMLCite \textit{E. Clarke} et al., Form. Methods Syst. Des. 25, No. 2--3, 105--127 (2004; Zbl 1090.68022) Full Text: DOI
Mueller, Silvia M.; Paul, Wolfgang J.; Kroening, Daniel Proving the correctness of processors with delayed branch using delayed PC. (English) Zbl 0956.68520 Althöfer, Ingo (ed.) et al., Numbers, information and complexity. Dedicated to Rudolf Ahlswede on the occasion of his 60th birthday. Dordrecht: Kluwer Academic Publishers. 579-588 (2000). MSC: 68Q60 68N99 PDFBibTeX XMLCite \textit{S. M. Mueller} et al., in: Numbers, information and complexity. Dedicated to Rudolf Ahlswede on the occasion of his 60th birthday. Dordrecht: Kluwer Academic Publishers. 579--588 (2000; Zbl 0956.68520)