Daniel Kroening

Ofer Strichman, Daniel Kroening: Preface to the special issue "SI: Satisfiability Modulo Theories". Formal Methods in System Design 42(1): 1-2 (2013)

Daniel Kroening, Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich, Christoph M. Wintersteiger: Loop summarization using state and transition invariants. Formal Methods in System Design 42(3): 221-261 (2013)

Mohamed Nassim Seghir, Daniel Kroening: Counterexample-Guided Precondition Inference. ESOP 2013: 451-471

Jade Alglave, Daniel Kroening, Vincent Nimal, Michael Tautschnig: Software Verification for Weak Memory via Program Transformation. ESOP 2013: 512-532

Vijay D'Silva, Leopold Haller, Daniel Kroening: Abstract conflict driven learning. POPL 2013: 143-154

Vijay D'Silva, Daniel Kroening: Abstraction of Syntax. VMCAI 2013: 396-413

Martin Brain, Vijay D'Silva, Leopold Haller, Alberto Griggio, Daniel Kroening: An Abstract Interpretation of DPLL(T). VMCAI 2013: 455-475

Jade Alglave, Daniel Kroening, Michael Tautschnig: Partial Orders for Efficient BMC of Concurrent Software. CoRR abs/1301.1629 (2013)

Alastair F. Donaldson, Alexander Kaiser, Daniel Kroening, Michael Tautschnig, Thomas Wahl: Counterexample-guided abstraction refinement for symmetric concurrent programs. Formal Methods in System Design 41(1): 25-44 (2012)

Hana Chockler, Daniel Kroening, Mitra Purandare: Computing Mutation Coverage in Interpolation-Based Model Checking. IEEE Trans. on CAD of Integrated Circuits and Systems 31(5): 765-778 (2012)

Alexander Kaiser, Daniel Kroening, Thomas Wahl: Efficient Coverability Analysis by Proof Minimization. CONCUR 2012: 500-515

Leopold Haller, Alberto Griggio, Martin Brain, Daniel Kroening: Deciding floating-point logic with systematic abstraction. FMCAD 2012: 131-140

Vijay D'Silva, Leopold Haller, Daniel Kroening: Satisfiability Solvers Are Static Analysers. SAS 2012: 317-333

Vijay D'Silva, Leopold Haller, Daniel Kroening, Michael Tautschnig: Numeric Bounds Analysis with Conflict-Driven Learning. TACAS 2012: 48-63

Andreas Holzer, Daniel Kroening, Christian Schallhart, Michael Tautschnig, Helmut Veith: Proving Reachability Using FShell - (Competition Contribution). TACAS 2012: 538-541

Gérard Basler, Alastair F. Donaldson, Alexander Kaiser, Daniel Kroening, Michael Tautschnig, Thomas Wahl: satabs: A Bit-Precise Verifier for C Programs - (Competition Contribution). TACAS 2012: 552-555

Georg Weissenbacher, Daniel Kroening, Sharad Malik: Wolverine: Battling Bugs with Interpolants - (Competition Contribution). TACAS 2012: 556-558

Jade Alglave, Daniel Kroening, Vincent Nimal, Michael Tautschnig: Software Verification for Weak Memory via Program Transformation. CoRR abs/1207.7264 (2012)

Daniel Kroening, Tiziana Margaria, Jim Woodcock: Editorial. Formal Asp. Comput. 23(5): 585-588 (2011)

Alastair F. Donaldson, Daniel Kroening, Philipp Rümmer: Automatic analysis of DMA races using model checking and k-induction. Formal Methods in System Design 39(1): 83-113 (2011)

Angelo Brillout, Daniel Kroening, Philipp Rümmer, Thomas Wahl: An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic. J. Autom. Reasoning 47(4): 341-367 (2011)

Jade Alglave, Daniel Kroening, John Lugton, Vincent Nimal, Michael Tautschnig: Soundness of Data Flow Analyses for Weak Memory Models. APLAS 2011: 272-288

Jade Alglave, Alastair F. Donaldson, Daniel Kroening, Michael Tautschnig: Making Software Verification Tools Really Work. ATVA 2011: 28-42

Alastair F. Donaldson, Alexander Kaiser, Daniel Kroening, Thomas Wahl: Symmetry-Aware Predicate Abstraction for Shared-Variable Concurrent Programs. CAV 2011: 356-371

Daniel Kroening, Joël Ouaknine, Ofer Strichman, Thomas Wahl, James Worrell: Linear Completeness Thresholds for Bounded Model Checking. CAV 2011: 557-572

Daniel Kroening, Georg Weissenbacher: Interpolation-Based Software Verification with Wolverine. CAV 2011: 573-578

Nannan He, Philipp Rümmer, Daniel Kroening: Test-case generation for embedded simulink via formal concept analysis. DAC 2011: 224-229

Alastair F. Donaldson, Daniel Kroening, Philipp Rümmer: SCRATCH: a tool for automatic analysis of dma races. PPOPP 2011: 311-312

Alastair F. Donaldson, Leopold Haller, Daniel Kroening, Philipp Rümmer: Software Verification Using k-Induction. SAS 2011: 351-368

Aliaksei Tsitovich, Natasha Sharygina, Christoph M. Wintersteiger, Daniel Kroening: Loop Summarization and Termination Analysis. TACAS 2011: 81-95

Angelo Brillout, Daniel Kroening, Philipp Rümmer, Thomas Wahl: Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic. VMCAI 2011: 88-102

Alastair F. Donaldson, Leopold Haller, Daniel Kroening: Strengthening Induction-Based Race Checking with Lightweight Static Analysis. VMCAI 2011: 169-183

Sharon Barner, Ian G. Harris, Daniel Kroening, Orna Raz (Eds.): Hardware and Software: Verification and Testing - 6th International Haifa Verification Conference, HVC 2010, Haifa, Israel, October 4-7, 2010. Revised Selected Papers. Lecture Notes in Computer Science 6504, Springer 2011, isbn 978-3-642-19582-2

Alastair F. Donaldson, Alexander Kaiser, Daniel Kroening, Thomas Wahl: Symmetry-Aware Predicate Abstraction for Shared-Variable Concurrent Programs (Extended Technical Report). CoRR abs/1102.2330 (2011)

Daniel Kroening, Georg Weissenbacher: Verification and falsification of programs with loops using predicate abstraction. Formal Asp. Comput. 22(2): 105-128 (2010)

Gérard Basler, Michele Mazzucchi, Thomas Wahl, Daniel Kroening: Context-aware counter abstraction. Formal Methods in System Design 36(3): 223-245 (2010)

Daniel Kroening, Tiziana Margaria: Verified software: theories, tools and experiments. STTT 12(6): 405-408 (2010)

Igor Zinovik, Yury Chebiryak, Daniel Kroening: Periodic orbits and equilibria in glass models for gene regulatory networks. IEEE Transactions on Information Theory 56(2): 805-820 (2010)

Nicolas Blanc, Daniel Kroening: Race analysis for systemc using model checking. ACM Trans. Design Autom. Electr. Syst. 15(3) (2010)

Angelo Brillout, Daniel Kroening, Philipp Rümmer, Thomas Wahl: An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic. IJCAR 2010: 384-399

Daniel Kroening, Natasha Sharygina, Aliaksei Tsitovich, Christoph M. Wintersteiger: Termination Analysis with Compositional Transition Invariants. CAV 2010: 89-103

Alexander Kaiser, Daniel Kroening, Thomas Wahl: Dynamic Cutoff Detection in Parameterized Concurrent Programs. CAV 2010: 645-659

Hana Chockler, Daniel Kroening, Mitra Purandare: Coverage in interpolation-based model checking. DAC 2010: 182-187

Alastair F. Donaldson, Nannan He, Daniel Kroening, Philipp Rümmer: Tightening Test Coverage Metrics: A Case Study in Equivalence Checking Using k-Induction. FMCO 2010: 297-315

Daniel Kroening, Jérôme Leroux, Philipp Rümmer: Interpolating Quantifier-Free Presburger Arithmetic. LPAR (Yogyakarta) 2010: 489-503

Gérard Basler, Matthew Hague, Daniel Kroening, C.-H. Luke Ong, Thomas Wahl, Haoxian Zhao: Boom: Taking Boolean Program Model Checking One Step Further. TACAS 2010: 145-149

Byron Cook, Daniel Kroening, Philipp Rümmer, Christoph M. Wintersteiger: Ranking Function Synthesis for Bit-Vector Relations. TACAS 2010: 236-250

Alastair F. Donaldson, Daniel Kroening, Philipp Rümmer: Automatic Analysis of Scratch-Pad Memory Code for Heterogeneous Multicore Processors. TACAS 2010: 280-295

Vijay D'Silva, Daniel Kroening, Mitra Purandare, Georg Weissenbacher: Interpolant Strength. VMCAI 2010: 129-145

Angelo Brillout, Daniel Kroening, Philipp Rümmer, Thomas Wahl: Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic (Extended Technical Report). CoRR abs/1011.1036 (2010)

Daniel Kroening, Ofer Strichman: A framework for Satisfiability Modulo Theories. Formal Asp. Comput. 21(5): 485-494 (2009)

Randal E. Bryant, Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, Ofer Strichman, Bryan A. Brady: An abstraction-based decision procedure for bit-vector arithmetic. STTT 11(2): 95-104 (2009)

Gérard Basler, Michele Mazzucchi, Thomas Wahl, Daniel Kroening: Symbolic Counter Abstraction for Concurrent Software. CAV 2009: 64-78

Mitra Purandare, Thomas Wahl, Daniel Kroening: Strengthening properties using abstraction refinement. DATE 2009: 1692-1697

Vijay D'Silva, Daniel Kroening: Fixed points for multi-cycle path detection. DATE 2009: 1710-1715

Angelo Brillout, Daniel Kroening, Thomas Wahl: Mixed abstractions for floating-point arithmetic. FMCAD 2009: 69-76

Angelo Brillout, Nannan He, Michele Mazzucchi, Daniel Kroening, Mitra Purandare, Philipp Rümmer, Georg Weissenbacher: Mutation-Based Test Case Generation for Simulink Models. FMCO 2009: 208-227

Daniel Kroening, Georg Weissenbacher: An Interpolating Decision Procedure for Transitive Relations with Uninterpreted Functions. Haifa Verification Conference 2009: 150-168

Daniel Kroening, Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich, Christoph M. Wintersteiger: Loopfrog: A Static Analyzer for ANSI-C Programs. ASE 2009: 668-670

Yury Chebiryak, Thomas Wahl, Daniel Kroening, Leopold Haller: Finding Lean Induced Cycles in Binary Hypercubes. SAT 2009: 18-31

Nicolas Blanc, Daniel Kroening: Speeding Up Simulation of SystemC Using Model Checking. SBMF 2009: 1-16

Daniel Kroening: Software Verification. Handbook of Satisfiability 2009: 505-532

Yury Chebiryak, Daniel Kroening: Towards a Classification of Hamiltonian Cycles in the 6-Cube. JSAT 4(1): 57-74 (2008)

Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund M. Clarke: Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog. IEEE Trans. on CAD of Integrated Circuits and Systems 27(2): 366-379 (2008)

Vijay D'Silva, Daniel Kroening, Georg Weissenbacher: A Survey of Automated Techniques for Formal Software Verification. IEEE Trans. on CAD of Integrated Circuits and Systems 27(7): 1165-1178 (2008)

Igor Zinovik, Daniel Kroening, Yury Chebiryak: Computing Binary Combinatorial Gray Codes Via Exhaustive Search With SAT Solvers. IEEE Transactions on Information Theory 54(4): 1819-1823 (2008)

Daniel Kroening, Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich, Christoph M. Wintersteiger: Loop Summarization Using Abstract Transformers. ATVA 2008: 111-125

Chao Wang, Malay K. Ganai, Shuvendu K. Lahiri, Daniel Kroening: Embedded software verification: challenges and solutions. ICCAD 2008: 5

Nicolas Blanc, Daniel Kroening: Race analysis for SystemC using model checking. ICCAD 2008: 356-363

Nicolas Blanc, Daniel Kroening, Natasha Sharygina: Scoot: A Tool for the Analysis of SystemC Models. TACAS 2008: 467-470

Vijay D'Silva, Mitra Purandare, Daniel Kroening: Approximation Refinement for Interpolation-Based Model Checking. VMCAI 2008: 68-82

Angelo Brillout, Daniel Kroening, Thomas Wahl: Craig Interpolation for Quantifier-Free Presburger Arithmetic. CoRR abs/0811.3521 (2008)

Edmund M. Clarke, Himanshu Jain, Daniel Kroening: Verification of SpecC using predicate abstraction. Formal Methods in System Design 30(1): 5-28 (2007)

Byron Cook, Daniel Kroening, Natasha Sharygina: Verification of Boolean programs with unbounded thread creation. Theor. Comput. Sci. 388(1-3): 227-242 (2007)

Igor Zinovik, Daniel Kroening, Yury Chebiryak: An Algebraic Algorithm for the Identification of Glass Networks with Periodic Orbits Along Cyclic Attractors. AB 2007: 140-154

Daniel Kroening, Natasha Sharygina: Interactive presentation: Image computation and predicate refinement for RTL verilog using word level proofs. DATE 2007: 1325-1330

Daniel Kroening, Georg Weissenbacher: Lifting Propositional Interpolants to the Word-Level. FMCAD 2007: 85-89

Gérard Basler, Daniel Kroening, Georg Weissenbacher: A Complete Bounded Model Checking Algorithm for Pushdown Systems. Haifa Verification Conference 2007: 202-217

Daniel Kroening, Sanjit A. Seshia: Formal verification at higher levels of abstraction. ICCAD 2007: 572-578

Thomas Witkowski, Nicolas Blanc, Daniel Kroening, Georg Weissenbacher: Model checking concurrent linux device drivers. ASE 2007: 501-504

Nicolas Blanc, Alex Groce, Daniel Kroening: Verifying C++ with STL containers via predicate abstraction. ASE 2007: 521-524

Toni Jussila, Armin Biere, Carsten Sinz, Daniel Kröning, Christoph M. Wintersteiger: A First Step Towards a Unified Proof Checker for QBF. SAT 2007: 201-214

Gérard Basler, Daniel Kroening, Georg Weissenbacher: SAT-Based Summarization for Boolean Programs. SPIN 2007: 131-148

Natasha Sharygina, Daniel Kröning: Model Checking with Abstraction for Web Services. Test and Analysis of Web Services 2007: 121-145

Randal E. Bryant, Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, Ofer Strichman, Bryan A. Brady: Deciding Bit-Vector Arithmetic with Abstraction. TACAS 2007: 358-372

Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund M. Clarke: VCEGAR: Verilog CounterExample Guided Abstraction Refinement. TACAS 2007: 583-586

Daniel Kroening: Computing Over-Approximations with Bounded Model Checking. Electr. Notes Theor. Comput. Sci. 144(1): 79-92 (2006)

Alex Groce, Sagar Chaki, Daniel Kroening, Ofer Strichman: Error explanation with distance metrics. STTT 8(3): 229-247 (2006)

Sven Beyer, Christian Jacobi, Daniel Kröning, Dirk Leinenbach, Wolfgang J. Paul: Putting it all together - Formal verification of the VAMP. STTT 8(4-5): 411-430 (2006)

Daniel Kroening, Georg Weissenbacher: Counterexamples with Loops for Predicate Abstraction. CAV 2006: 152-165

Byron Cook, Daniel Kroening, Natasha Sharygina: Over-Approximating Boolean Programs with Unbounded Thread Creation. FMCAD 2006: 53-59

Sharon Barner, Cindy Eisner, Ziv Glazberg, Daniel Kroening, Ishai Rabinovitz: ExpliSAT: Guiding SAT-Based Software Verification with Explicit States. Haifa Verification Conference 2006: 138-154

Daniel Kroening, Natasha Sharygina: Approximating Predicate Images for Bit-Vector Logic. TACAS 2006: 242-256

Alex Groce, Daniel Kroening: Making the Most of BMC Counterexamples. Electr. Notes Theor. Comput. Sci. 119(2): 67-81 (2005)

Edmund M. Clarke, Daniel Kroening, Joël Ouaknine, Ofer Strichman: Computational challenges in bounded model checking. STTT 7(2): 174-183 (2005)

Byron Cook, Daniel Kroening, Natasha Sharygina: Cogent: Accurate Theorem Proving for Program Verification. CAV 2005: 296-300

Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund M. Clarke: Word level predicate abstraction and refinement for verifying RTL verilog. DAC 2005: 445-450

Daniel Kroening, Natasha Sharygina: Formal verification of SystemC by automatic hardware/software partitioning. MEMOCODE 2005: 101-110

Byron Cook, Daniel Kroening, Natasha Sharygina: Symbolic Model Checking for Asynchronous Boolean Programs. SPIN 2005: 75-90

Edmund M. Clarke, Daniel Kroening, Natasha Sharygina, Karen Yorav: SATABS: SAT-Based Predicate Abstraction for ANSI-C. TACAS 2005: 570-574

Daniel Kroening: Decision Procedures for the Grand Challenge. VSTTE 2005: 428-437

Daniel Kröning: Formal verification of pipelined microprocessors. Saarland University 2004

Edmund M. Clarke, Daniel Kroening, Natasha Sharygina, Karen Yorav: Predicate Abstraction of ANSI-C Programs Using SAT. Formal Methods in System Design 25(2-3): 105-127 (2004)

Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, Ofer Strichman: Abstraction-Based Satisfiability Solving of Presburger Arithmetic. CAV 2004: 308-320

Alex Groce, Daniel Kroening, Flavio Lerda: Understanding Counterexamples with explain. CAV 2004: 453-456

Pankaj Chauhan, Edmund M. Clarke, Daniel Kroening: A SAT-based algorithm for reparameterization in symbolic simulation. DAC 2004: 524-529

Jennifer Morris, Daniel Kroening, Philip Koopman: Fault Tolerance Tradeoffs in Moving from Decentralized to Centralized Embedded Systems. DSN 2004: 377-

Daniel Kroening, Edmund M. Clarke: Checking consistency of C and Verilog using predicate abstraction and induction. ICCAD 2004: 66-72

Edmund M. Clarke, Daniel Kroening: Tutorial: Software Model Checking. ICFEM 2004: 9-10

Daniel Kroening, Alex Groce, Edmund M. Clarke: Counterexample Guided Abstraction Refinement Via Program Execution. ICFEM 2004: 224-238

Byron Cook, Daniel Kroening, Natasha Sharygina: Accurate Theorem Proving for Program Verification. ISoLA 2004: 96-114

Bernd Becker, Markus Behle, Friedrich Eisenbrand, Martin Fränzle, Marc Herbstritt, Christian Herde, Jörg Hoffmann, Daniel Kröning, Bernhard Nebel, Ilia Polian, Ralf Wimmer: Bounded Model Checking and Inductive Verification of Hybrid Discrete-continuous Systems. MBMV 2004: 65-75

Himanshu Jain, Daniel Kroening, Edmund M. Clarke: Verification of SpecC using predicate abstraction. MEMOCODE 2004: 7-16

Edmund M. Clarke, Daniel Kroening, Flavio Lerda: A Tool for Checking ANSI-C Programs. TACAS 2004: 168-176

Edmund M. Clarke, Daniel Kroening, Joël Ouaknine, Ofer Strichman: Completeness and Complexity of Bounded Model Checking. VMCAI 2004: 85-96

Edmund M. Clarke, Daniel Kroening: Hardware verification using ANSI-C programs as a reference. ASP-DAC 2003: 308-311

Sven Beyer, Christian Jacobi, Daniel Kroening, Dirk Leinenbach, Wolfgang J. Paul: Instantiating Uninterpreted Functional Units and Memory System: Functional Verification of the VAMP. CHARME 2003: 51-65

Edmund M. Clarke, Daniel Kroening, Karen Yorav: Behavioral consistency of C and verilog programs using bounded model checking. DAC 2003: 368-371

Edmund M. Clarke, Daniel Kroening, Karen Yorav: Specifying and Verifying Systems with Multiple Clocks. ICCD 2003: 48-

Daniel Kroening, Ofer Strichman: Efficient Computation of Recurrence Diameters. VMCAI 2003: 298-309

Daniel Kröning: Formal verification of pipelined microprocessors. Universität Saarbrücken 2001, pp. I-XIV, 1-348

Daniel Kroening, Wolfgang J. Paul: Automated Pipeline Design. DAC 2001: 810-815

Daniel Kröning, Wolfgang J. Paul, Silvia M. Müller: Proving the Correctness of Pipelined Micro-Architectures. MBMV 2000: 89-98

Silvia M. Müller, Holger W. Leister, Peter Dell, Nikolaus Gerteis, Daniel Kroening: The Impact of Hardware Scheduling Mechanismus on the Performance and Cost of Processor Designs. ARCS 1999: 65-73