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

Proving the Correctness of a Complete Microprocessor. - Christian Jacobi 002; Daniel Kroening (GI Jahrestagung, 2000)

Proving the Correctness of Pipelined Micro-Architectures. - Daniel Kröning; Wolfgang J. Paul; Silvia M. Müller (MBMV, 2000)

Formal verification of pipelined microprocessors. - Daniel Kröning (2001)

Automated Pipeline Design. - Daniel Kroening; Wolfgang J. Paul (DAC, 2001)

Formal verification of pipelined microprocessors. - Daniel Kröning (Ausgezeichnete Informatikdissertationen, 2001)

Hardware verification using ANSI-C programs as a reference. - Edmund M. Clarke; Daniel Kroening (ASP-DAC, 2003)

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

Behavioral consistency of C and verilog programs using bounded model checking. - Edmund M. Clarke; Daniel Kroening; Karen Yorav (DAC, 2003)

Specifying and Verifying Systems with Multiple Clocks. - Edmund M. Clarke; Daniel Kroening; Karen Yorav (ICCD, 2003)

Efficient Computation of Recurrence Diameters. - Daniel Kroening; Ofer Strichman (VMCAI, 2003)

Understanding Counterexamples with explain. - Alex Groce; Daniel Kroening; Flavio Lerda (CAV, 2004)

Abstraction-Based Satisfiability Solving of Presburger Arithmetic. - Daniel Kroening; Joël Ouaknine; Sanjit A. Seshia; Ofer Strichman (CAV, 2004)

A SAT-based algorithm for reparameterization in symbolic simulation. - Pankaj Chauhan; Edmund M. Clarke; Daniel Kroening (DAC, 2004)

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

Checking consistency of C and Verilog using predicate abstraction and induction. - Daniel Kroening; Edmund M. Clarke (ICCAD, 2004)

Tutorial: Software Model Checking. - Edmund M. Clarke; Daniel Kroening (ICFEM, 2004)

Counterexample Guided Abstraction Refinement Via Program Execution. - Daniel Kroening; Alex Groce; Edmund M. Clarke (ICFEM, 2004)

Accurate Theorem Proving for Program Verification. - Byron Cook; Daniel Kroening; Natasha Sharygina (ISoLA, 2004)

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

A Tool for Checking ANSI-C Programs. - Edmund M. Clarke; Daniel Kroening; Flavio Lerda (TACAS, 2004)

Completeness and Complexity of Bounded Model Checking. - Edmund M. Clarke; Daniel Kroening; Joël Ouaknine; Ofer Strichman (VMCAI, 2004)

Making the Most of BMC Counterexamples. - Alex Groce; Daniel Kroening (BMC@CAV, 2004)

Predicate Abstraction of ANSI-C Programs Using SAT. - Edmund M. Clarke; Daniel Kroening; Natasha Sharygina; Karen Yorav (Formal Methods Syst. Des., 2004)

Cogent: Accurate Theorem Proving for Program Verification. - Byron Cook; Daniel Kroening; Natasha Sharygina (CAV, 2005)

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

Formal verification of SystemC by automatic hardware/software partitioning. - Daniel Kroening; Natasha Sharygina (MEMOCODE, 2005)

Symbolic Model Checking for Asynchronous Boolean Programs. - Byron Cook; Daniel Kroening; Natasha Sharygina (SPIN, 2005)

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

Decision Procedures for the Grand Challenge. - Daniel Kroening (VSTTE, 2005)

Computing Over-Approximations with Bounded Model Checking. - Daniel Kroening (BMC@CAV, 2005)

Computational challenges in bounded model checking. - Edmund M. Clarke; Daniel Kroening; Joël Ouaknine; Ofer Strichman (Int. J. Softw. Tools Technol. Transf., 2005)

Counterexamples with Loops for Predicate Abstraction. - Daniel Kroening; Georg Weissenbacher (CAV, 2006)

Over-Approximating Boolean Programs with Unbounded Thread Creation. - Byron Cook; Daniel Kroening; Natasha Sharygina (FMCAD, 2006)

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

Approximating Predicate Images for Bit-Vector Logic. - Daniel Kroening; Natasha Sharygina (TACAS, 2006)

Putting it all together - Formal verification of the VAMP. - Sven Beyer; Christian Jacobi 002; Daniel Kröning; Dirk Leinenbach; Wolfgang J. Paul (Int. J. Softw. Tools Technol. Transf., 2006)

Error explanation with distance metrics. - Alex Groce; Sagar Chaki; Daniel Kroening; Ofer Strichman (Int. J. Softw. Tools Technol. Transf., 2006)

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

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

Lifting Propositional Interpolants to the Word-Level. - Daniel Kroening; Georg Weissenbacher (FMCAD, 2007)

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

Formal verification at higher levels of abstraction. - Daniel Kroening; Sanjit A. Seshia (ICCAD, 2007)

Verifying C++ with STL containers via predicate abstraction. - Nicolas Blanc; Alex Groce; Daniel Kroening (ASE, 2007)

Model checking concurrent linux device drivers. - Thomas Witkowski; Nicolas Blanc; Daniel Kroening; Georg Weissenbacher (ASE, 2007)

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

SAT-Based Summarization for Boolean Programs. - Gérard Basler; Daniel Kroening; Georg Weissenbacher (SPIN, 2007)

Model Checking with Abstraction for Web Services. - Natasha Sharygina; Daniel Kröning (Test and Analysis of Web Services, 2007)

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

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

Verification of SpecC using predicate abstraction. - Edmund M. Clarke; Himanshu Jain; Daniel Kroening (Formal Methods Syst. Des., 2007)

Verification of Boolean programs with unbounded thread creation. - Byron Cook; Daniel Kroening; Natasha Sharygina (Theor. Comput. Sci., 2007)

Loop Summarization Using Abstract Transformers. - Daniel Kroening; Natasha Sharygina; Stefano Tonetta; Aliaksei Tsitovich; Christoph M. Wintersteiger (ATVA, 2008)

Embedded software verification: challenges and solutions. - Chao Wang 001; Malay K. Ganai; Shuvendu K. Lahiri; Daniel Kroening (ICCAD, 2008)

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

Approximation Refinement for Interpolation-Based Model Checking. - Vijay Victor D'Silva; Mitra Purandare; Daniel Kroening (VMCAI, 2008)

Craig Interpolation for Quantifier-Free Presburger Arithmetic - Angelo Brillout; Daniel Kroening; Thomas Wahl (CoRR, 2008)

Towards a Classification of Hamiltonian Cycles in the 6-Cube. - Yury Chebiryak; Daniel Kroening (J. Satisf. Boolean Model. Comput., 2008)

A Survey of Automated Techniques for Formal Software Verification. - Vijay Victor D'Silva; Daniel Kroening; Georg Weissenbacher (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2008)

Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog. - Himanshu Jain; Daniel Kroening; Natasha Sharygina; Edmund M. Clarke (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2008)

Computing Binary Combinatorial Gray Codes Via Exhaustive Search With SAT Solvers. - Igor Zinovik; Daniel Kroening; Yury Chebiryak (IEEE Trans. Inf. Theory, 2008)

Decision Procedures - An Algorithmic Point of View - Daniel Kroening; Ofer Strichman (Springer, 2008)

Symbolic Counter Abstraction for Concurrent Software. - Gérard Basler; Michele Mazzucchi; Thomas Wahl; Daniel Kroening (CAV, 2009)

Fixed points for multi-cycle path detection. - Vijay Victor D'Silva; Daniel Kroening (DATE, 2009)

Strengthening properties using abstraction refinement. - Mitra Purandare; Thomas Wahl; Daniel Kroening (DATE, 2009)

Mixed abstractions for floating-point arithmetic. - Angelo Brillout; Daniel Kroening; Thomas Wahl (FMCAD, 2009)

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

An Interpolating Decision Procedure for Transitive Relations with Uninterpreted Functions. - Daniel Kroening; Georg Weissenbacher (Haifa Verification Conference, 2009)

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

Finding Lean Induced Cycles in Binary Hypercubes. - Yury Chebiryak; Thomas Wahl; Daniel Kroening; Leopold Haller (SAT, 2009)

Speeding Up Simulation of SystemC Using Model Checking. - Nicolas Blanc; Daniel Kroening (SBMF, 2009)

A framework for Satisfiability Modulo Theories. - Daniel Kroening; Ofer Strichman (Formal Aspects Comput., 2009)

An abstraction-based decision procedure for bit-vector arithmetic. - Randal E. Bryant; Daniel Kroening; Joël Ouaknine; Sanjit A. Seshia; Ofer Strichman; Bryan A. Brady (Int. J. Softw. Tools Technol. Transf., 2009)

Software Verification. - Daniel Kroening (Handbook of Satisfiability, 2009)

Program Verification via Craig Interpolation for Presburger Arithmetic with Arrays. - Angelo Brillout; Daniel Kroening; Philipp Rümmer; Thomas Wahl (VERIFY@IJCAR, 2010)

Loopfrog - loop summarization for static analysis. - Daniel Kroening; Natasha Sharygina; Stefano Tonetta; Aliaksei Tsitovich; Christoph M. Wintersteiger (WING@ETAPS/IJCAR, 2010)

Dynamic Cutoff Detection in Parameterized Concurrent Programs. - Alexander Kaiser 001; Daniel Kroening; Thomas Wahl (CAV, 2010)

Termination Analysis with Compositional Transition Invariants. - Daniel Kroening; Natasha Sharygina; Aliaksei Tsitovich; Christoph M. Wintersteiger (CAV, 2010)

Coverage in interpolation-based model checking. - Hana Chockler; Daniel Kroening; Mitra Purandare (DAC, 2010)

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

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

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

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

Interpolant Strength. - Vijay Victor D'Silva; Daniel Kroening; Mitra Purandare; Georg Weissenbacher (VMCAI, 2010)

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

Verification and falsification of programs with loops using predicate abstraction. - Daniel Kroening; Georg Weissenbacher (Formal Aspects Comput., 2010)

Context-aware counter abstraction. - Gérard Basler; Michele Mazzucchi; Thomas Wahl; Daniel Kroening (Formal Methods Syst. Des., 2010)

Verified software: theories, tools and experiments. - Daniel Kroening; Tiziana Margaria (Int. J. Softw. Tools Technol. Transf., 2010)

Periodic orbits and equilibria in glass models for gene regulatory networks. - Igor Zinovik; Yury Chebiryak; Daniel Kroening (IEEE Trans. Inf. Theory, 2010)

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

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

Making Software Verification Tools Really Work. - Jade Alglave; Alastair F. Donaldson; Daniel Kroening; Michael Tautschnig (ATVA, 2011)

Symmetry-Aware Predicate Abstraction for Shared-Variable Concurrent Programs. - Alastair F. Donaldson; Alexander Kaiser 001; Daniel Kroening; Thomas Wahl (CAV, 2011)

Linear Completeness Thresholds for Bounded Model Checking. - Daniel Kroening; Joël Ouaknine; Ofer Strichman; Thomas Wahl; James Worrell 001 (CAV, 2011)

Interpolation-Based Software Verification with Wolverine. - Daniel Kroening; Georg Weissenbacher (CAV, 2011)

Test-case generation for embedded simulink via formal concept analysis. - Nannan He; Philipp Rümmer; Daniel Kroening (DAC, 2011)

SCRATCH: a tool for automatic analysis of dma races. - Alastair F. Donaldson; Daniel Kroening; Philipp Rümmer (PPoPP, 2011)

Software Verification Using k-Induction. - Alastair F. Donaldson; Leopold Haller; Daniel Kroening; Philipp Rümmer (SAS, 2011)

Loop Summarization and Termination Analysis. - Aliaksei Tsitovich; Natasha Sharygina; Christoph M. Wintersteiger; Daniel Kroening (TACAS, 2011)

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

Strengthening Induction-Based Race Checking with Lightweight Static Analysis. - Alastair F. Donaldson; Leopold Haller; Daniel Kroening (VMCAI, 2011)

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

Editorial. - Daniel Kroening; Tiziana Margaria; Jim Woodcock 001 (Formal Aspects Comput., 2011)

Automatic analysis of DMA races using model checking and k-induction. - Alastair F. Donaldson; Daniel Kroening; Philipp Rümmer (Formal Methods Syst. Des., 2011)

An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic. - Angelo Brillout; Daniel Kroening; Philipp Rümmer; Thomas Wahl (J. Autom. Reason., 2011)

Efficient Coverability Analysis by Proof Minimization. - Alexander Kaiser 001; Daniel Kroening; Thomas Wahl (CONCUR, 2012)

Deciding floating-point logic with systematic abstraction. - Leopold Haller; Alberto Griggio; Martin Brain; Daniel Kroening (FMCAD, 2012)

Satisfiability Solvers Are Static Analysers. - Vijay Victor D'Silva; Leopold Haller; Daniel Kroening (SAS, 2012)

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

Numeric Bounds Analysis with Conflict-Driven Learning. - Vijay Victor D'Silva; Leopold Haller; Daniel Kroening; Michael Tautschnig (TACAS, 2012)

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

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

Counterexample-guided abstraction refinement for symmetric concurrent programs. - Alastair F. Donaldson; Alexander Kaiser 001; Daniel Kroening; Michael Tautschnig; Thomas Wahl (Formal Methods Syst. Des., 2012)

Computing Mutation Coverage in Interpolation-Based Model Checking. - Hana Chockler; Daniel Kroening; Mitra Purandare (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2012)

Partial Orders for Efficient Bounded Model Checking of Concurrent Software. - Jade Alglave; Daniel Kroening; Michael Tautschnig (CAV, 2013)

Software Verification for Weak Memory via Program Transformation. - Jade Alglave; Daniel Kroening; Vincent Nimal; Michael Tautschnig (ESOP, 2013)

Counterexample-Guided Precondition Inference. - Mohamed Nassim Seghir; Daniel Kroening (ESOP, 2013)

Formal co-validation of low-level hardware/software interfaces. - Alex Horn; Michael Tautschnig; Celina G. Val; Lihao Liang; Tom Melham; Jim Grundy; Daniel Kroening (FMCAD, 2013)

Verifying multi-threaded software with impact. - Björn Wachter; Daniel Kroening; Joël Ouaknine (FMCAD, 2013)

A visual studio plug-in for CProver. - Mohamed Nassim Seghir; Daniel Kroening (TOPI@ICSE, 2013)

Abstract conflict driven learning. - Vijay Victor D'Silva; Leopold Haller; Daniel Kroening (POPL, 2013)

Chaining Test Cases for Reactive System Testing. - Peter Schrammel; Tom Melham; Daniel Kroening (ICTSS, 2013)

Automated Verification of Concurrent Software. - Daniel Kroening (RP, 2013)

Interpolation-Based Verification of Floating-Point Programs with Abstract CDCL. - Martin Brain; Vijay Victor D'Silva; Alberto Griggio; Leopold Haller; Daniel Kroening (SAS, 2013)

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

Abstraction of Syntax. - Vijay Victor D'Silva; Daniel Kroening (VMCAI, 2013)

Chaining Test Cases for Reactive System Testing (extended version). - Peter Schrammel; Tom Melham; Daniel Kroening (CoRR, 2013)

Partial Orders for Efficient BMC of Concurrent Software - Jade Alglave; Daniel Kroening; Michael Tautschnig (CoRR, 2013)

Ranking function synthesis for bit-vector relations. - Byron Cook; Daniel Kroening; Philipp Rümmer; Christoph M. Wintersteiger (Formal Methods Syst. Des., 2013)

Loop summarization using state and transition invariants. - Daniel Kroening; Natasha Sharygina; Stefano Tonetta; Aliaksei Tsitovich; Christoph M. Wintersteiger (Formal Methods Syst. Des., 2013)

Preface to the special issue "SI: Satisfiability Modulo Theories". - Ofer Strichman; Daniel Kroening (Formal Methods Syst. Des., 2013)

Model and Proof Generation for Heap-Manipulating Programs. - Martin Brain; Cristina David; Daniel Kroening; Peter Schrammel (ESOP, 2014)

Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs. - Vojtech Forejt; Daniel Kroening; Ganesh Narayanaswamy; Subodh Sharma 001 (FM, 2014)

Accelerated test execution using GPUs. - Ajitha Rajan; Subodh Sharma 001; Peter Schrammel; Daniel Kroening (ASE, 2014)

Automating Software Analysis at Large Scale. - Daniel Kroening; Michael Tautschnig (MEMICS, 2014)

Camera-laser projector stereo system based anti-collision system for robotic wheelchair users with cognitive impairment. - Ashutosh Natraj; Shailendra Natraj; Sonia Waharte; Daniel Kroening (MFI, 2014)

Abstract satisfaction. - Vijay Victor D'Silva; Leopold Haller; Daniel Kroening (POPL, 2014)

CBMC - C Bounded Model Checker - (Competition Contribution). - Daniel Kroening; Michael Tautschnig (TACAS, 2014)

Lost in Abstraction: Monotonicity in Multi-Threaded Programs (Extended Technical Report). - Alexander Kaiser 001; Daniel Kroening; Thomas Wahl (CoRR, 2014)

Second-Order SAT Solving using Program Synthesis. - Daniel Kroening; Matt Lewis (CoRR, 2014)

AbPress: Flexing Partial-Order Reduction and Abstraction. - Daniel Kroening; Subodh Sharma 001; Björn Wachter (CoRR, 2014)

Incremental Bounded Model Checking for Embedded Software (extended version). - Peter Schrammel; Daniel Kroening; Martin Brain; Ruben Martins; Tino Teige; Tom Bienmüller (CoRR, 2014)

Next Generation Static Software Analysis Tools (Dagstuhl Seminar 14352). - Patrick Cousot; Daniel Kroening; Carsten Sinz (Dagstuhl Reports, 2014)

Decision Procedures and Abstract Interpretation (Dagstuhl Seminar 14351). - Daniel Kroening; Thomas W. Reps; Sanjit A. Seshia; Aditya V. Thakur (Dagstuhl Reports, 2014)

Deciding floating-point logic with abstract conflict driven clause learning. - Martin Brain; Vijay Victor D'Silva; Alberto Griggio; Leopold Haller; Daniel Kroening (Formal Methods Syst. Des., 2014)

A Widening Approach to Multithreaded Program Verification. - Alexander Kaiser 001; Daniel Kroening; Thomas Wahl (ACM Trans. Program. Lang. Syst., 2014)

Introduction. - Hana Chockler; Daniel Kroening; Leonardo Mariani; Natasha Sharygina (Validation of Evolving Software, 2015)

Challenges of Existing Technology. - Hana Chockler; Daniel Kroening; Leonardo Mariani; Natasha Sharygina (Validation of Evolving Software, 2015)

Complementarities Among the Technologies Presented in the Book. - Hana Chockler; Daniel Kroening; Leonardo Mariani; Natasha Sharygina (Validation of Evolving Software, 2015)

Measuring Change Impact on Program Behaviour. - Ajitha Rajan; Daniel Kroening (Validation of Evolving Software, 2015)

Learning the Language of Error. - Martin Chapman; Hana Chockler; Pascal Kesseli; Daniel Kroening; Ofer Strichman; Michael Tautschnig (ATVA, 2015)

Unfolding-based Partial Order Reduction. - César Rodríguez; Marcelo Sousa; Subodh Sharma 001; Daniel Kroening (CONCUR, 2015)

Effective verification of low-level software with nested interrupts. - Daniel Kroening; Lihao Liang; Tom Melham; Peter Schrammel; Michael Tautschnig (DATE, 2015)

Verifying synchronous reactive systems using lazy abstraction. - Kumar Madhukar; Mandayam K. Srivas; Björn Wachter; Daniel Kroening; Ravindra Metta (DATE, 2015)

Unrestricted Termination and Non-termination Arguments for Bit-Vector Programs. - Cristina David; Daniel Kroening; Matt Lewis (ESOP, 2015)

Propositional Reasoning about Safety and Termination of Heap-Manipulating Programs. - Cristina David; Daniel Kroening; Matt Lewis (ESOP, 2015)

Evaluation of Measures for Statistical Fault Localisation and an Optimising Scheme. - David Landsberg; Hana Chockler; Daniel Kroening; Matt Lewis (FASE, 2015)

Property-Driven Fence Insertion Using Reorder Bounded Model Checking. - Saurabh Joshi 001; Daniel Kroening (FM, 2015)

Proving Safety with Trace Automata and Bounded Model Checking. - Daniel Kroening; Matt Lewis; Georg Weissenbacher (FM, 2015)

Accelerating Invariant Generation. - Kumar Madhukar; Björn Wachter; Daniel Kroening; Matt Lewis; Mandayam K. Srivas (FMCAD, 2015)

Successful Use of Incremental BMC in the Automotive Industry. - Peter Schrammel; Daniel Kroening; Martin Brain; Ruben Martins; Tino Teige; Tom Bienmüller (FMICS, 2015)

On Partial Order Semantics for SAT/SMT-Based Symbolic Encodings of Weak Memory Concurrency. - Alex Horn; Daniel Kroening (FORTE, 2015)

Faster Linearizability Checking via P-Compositionality. - Alex Horn; Daniel Kroening (FORTE, 2015)

Hardware Verification Using Software Analyzers. - Rajdeep Mukherjee; Daniel Kroening; Tom Melham (ISVLSI, 2015)

Equivalence Checking Using Trace Partitioning. - Rajdeep Mukherjee; Daniel Kroening; Tom Melham; Mandayam K. Srivas (ISVLSI, 2015)

Synthesising Interprocedural Bit-Precise Termination Proofs (T). - Hong-Yi Chen; Cristina David; Daniel Kroening; Peter Schrammel; Björn Wachter (ASE, 2015)

Using Program Synthesis for Program Analysis. - Cristina David; Daniel Kroening; Matt Lewis (LPAR, 2015)

Safety Verification and Refutation by k-Invariants and k-Induction. - Martin Brain; Saurabh Joshi 001; Daniel Kroening; Peter Schrammel (SAS, 2015)

Unbounded-Time Analysis of Guarded LTI Systems with Inputs by Abstract Acceleration. - Dario Cattaruzza; Alessandro Abate; Peter Schrammel; Daniel Kroening (SAS, 2015)

From AgentSpeak to C for Safety Considerations in Unmanned Aerial Vehicles. - Samuel Bucheli; Daniel Kroening; Ruben Martins; Ashutosh Natraj (TAROS, 2015)

Safety Verification and Refutation by k-invariants and k-induction (extended version). - Martin Brain; Saurabh Joshi 001; Daniel Kroening; Peter Schrammel (CoRR, 2015)

Unbounded-Time Analysis of Guarded LTI Systems with Inputs by Abstract Acceleration (extended version). - Dario Cattaruzza; Alessandro Abate; Peter Schrammel; Daniel Kroening (CoRR, 2015)

Synthesising Interprocedural Bit-Precise Termination Proofs (extended version). - Hong-Yi Chen; Cristina David; Daniel Kroening; Peter Schrammel; Björn Wachter (CoRR, 2015)

Danger Invariants. - Cristina David; Daniel Kroening; Matt Lewis (CoRR, 2015)

Formalizing and Checking Thread Refinement for Data-Race-Free Execution Models (Extended Version). - Daniel Poetzl; Daniel Kroening (CoRR, 2015)

Under-approximating loops in C programs for fast counterexample detection. - Daniel Kroening; Matt Lewis; Georg Weissenbacher (Formal Methods Syst. Des., 2015)

Unbounded safety verification for hardware using software analyzers. - Rajdeep Mukherjee; Peter Schrammel; Daniel Kroening; Tom Melham (DATE, 2016)

Danger Invariants. - Cristina David; Pascal Kesseli; Daniel Kroening; Matt Lewis (FM, 2016)

Equivalence Checking of a Floating-Point Unit Against a High-Level C Model. - Rajdeep Mukherjee; Saurabh Joshi 001; Andreas Griesmayer; Daniel Kroening; Tom Melham (FM, 2016)

Probabilistic Fault Localisation. - David Landsberg; Hana Chockler; Daniel Kroening (Haifa Verification Conference, 2016)

Towards Automated Bounded Model Checking of API Implementations. - Daniel Neville; Andrew J. Malton; Martin Brain; Daniel Kroening (CSTVA@ISSTA, 2016)

Sound static deadlock analysis for C/Pthreads. - Daniel Kroening; Daniel Poetzl; Peter Schrammel; Björn Wachter (ASE, 2016)

Static Program Analysis for Identifying Energy Bugs in Graphics-Intensive Mobile Apps. - Chang Hwan Peter Kim; Daniel Kroening; Marta Z. Kwiatkowska (MASCOTS, 2016)

SC2: Satisfiability Checking Meets Symbolic Computation - (Project Paper). - Erika Ábrahám; John Abbott; Bernd Becker 001; Anna Maria Bigatti; Martin Brain; Bruno Buchberger; Alessandro Cimatti; James H. Davenport; Matthew England 001; Pascal Fontaine; Stephen Forrest; Alberto Griggio; et al. (CICM, 2016)

Assisted Coverage Closure. - Adam Nellis; Pascal Kesseli; Philippa Ryan Conmy; Daniel Kroening; Peter Schrammel; Michael Tautschnig (NFM, 2016)

The virtues of conflict: analysing modern concurrency. - Ganesh Narayanaswamy; Saurabh Joshi 001; Daniel Kroening (PPoPP, 2016)

Algebraic Techniques in Software Verification : Challenges and Opportunities. - Martin Brain; Daniel Kroening; Ryan McCleeary (SC²@SYNASC, 2016)

v2c - A Verilog to C Translator. - Rajdeep Mukherjee; Michael Tautschnig; Daniel Kroening (TACAS, 2016)

Formalizing and Checking Thread Refinement for Data-Race-Free Execution Models. - Daniel Poetzl; Daniel Kroening (TACAS, 2016)

2LS for Program Analysis - (Competition Contribution). - Peter Schrammel; Daniel Kroening (TACAS, 2016)

Automatic Generation of Propagation Complete SAT Encodings. - Martin Brain; Liana Hadarean; Daniel Kroening; Ruben Martins (VMCAI, 2016)

Satisfiability checking and symbolic computation. - Erika Ábrahám; John Abbott; Bernd Becker 001; Anna Maria Bigatti; Martin Brain; Bruno Buchberger; Alessandro Cimatti; James H. Davenport; Matthew England 001; Pascal Fontaine; Stephen Forrest; Alberto Griggio; et al. (ACM Commun. Comput. Algebra, 2016)

Satisfiability Checking meets Symbolic Computation (Project Paper). - Erika Ábrahám; John Abbott; Bernd Becker 001; Anna Maria Bigatti; Martin Brain; Bruno Buchberger; Alessandro Cimatti; James H. Davenport; Matthew England 001; Pascal Fontaine; Stephen Forrest; Alberto Griggio; et al. (CoRR, 2016)

Sound Static Deadlock Analysis for C/Pthreads (Extended Version). - Daniel Kroening; Daniel Poetzl; Peter Schrammel; Björn Wachter (CoRR, 2016)

Equivalence Checking a Floating-point Unit against a High-level C Model (Extended Version). - Rajdeep Mukherjee; Saurabh Joshi 001; Andreas Griesmayer; Daniel Kroening; Tom Melham (CoRR, 2016)

The Virtues of Conflict: Analyzing Modern Concurrency. - Ganesh Narayanaswamy; Saurabh Joshi 001; Daniel Kroening (CoRR, 2016)

Preface: Special Issue on Interpolation. - Daniel Kroening; Andrey Rybalchenko (J. Autom. Reason., 2016)

Generating test case chains for reactive systems. - Peter Schrammel; Tom Melham; Daniel Kroening (Int. J. Softw. Tools Technol. Transf., 2016)

Verification of Concurrent Software. - Daniel Kroening (Dependable Software Systems Engineering, 2016)

Decision Procedures - An Algorithmic Point of View, Second Edition - Daniel Kroening; Ofer Strichman (Springer, 2016)

Lifting CDCL to Template-Based Abstract Domains for Program Verification. - Rajdeep Mukherjee; Peter Schrammel; Leopold Haller; Daniel Kroening; Tom Melham (ATVA, 2017)

SC-square: when Satisfiability Checking and Symbolic Computation join forces. - Erika Ábrahám; John Abbott; Bernd Becker 001; Anna Maria Bigatti; Martin Brain; Alessandro Cimatti; James H. Davenport; Matthew England 001; Pascal Fontaine; Stephen Forrest; Vijay Ganesh 001; Alberto Griggio; et al. (ARCADE@CADE, 2017)

Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants. - Alessandro Abate; Iury Bessa; Dario Cattaruzza; Lucas C. Cordeiro; Cristina David; Pascal Kesseli; Daniel Kroening; Elizabeth Polgreen (CAV (1), 2017)

Sound Numerical Computations in Abstract Acceleration. - Dario Cattaruzza; Alessandro Abate; Peter Schrammel; Daniel Kroening (NSV@CAV, 2017)

Abstract Interpretation with Unfoldings. - Marcelo Sousa; César Rodríguez; Vijay Victor D'Silva; Daniel Kroening (CAV (2), 2017)

Formal Techniques for Effective Co-verification of Hardware/Software Co-designs. - Rajdeep Mukherjee; Mitra Purandare; Raphael Polig; Daniel Kroening (DAC, 2017)

Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants. - Alessandro Abate; Iury Bessa; Dario Cattaruzza; Lucas C. Cordeiro; Cristina David; Pascal Kesseli; Daniel Kroening (HSCC, 2017)

Functional Requirements-Based Automated Testing for Avionics. - Youcheng Sun; Martin Brain; Daniel Kroening; Andrew Hawthorn; Thomas Wilson; Florian Schanda; Francisco Javier Guzman Jimenez; Simon Daniel; Chris Bryan; Ian Broster (ICECCS, 2017)

Verifying digital systems with MATLAB. - Lennon C. Chaves; Iury Bessa; Lucas C. Cordeiro; Daniel Kroening; Eddie Batista de Lima Filho (ISSTA, 2017)

DSSynth: an automated digital controller synthesis tool for physical plants. - Alessandro Abate; Iury Bessa; Dario Cattaruzza; Lennon C. Chaves; Lucas C. Cordeiro; Cristina David; Pascal Kesseli; Daniel Kroening; Elizabeth Polgreen (ASE, 2017)

Modular Demand-Driven Analysis of Semantic Difference for Program Versions. - Anna Trostanetski; Orna Grumberg; Daniel Kroening (SAS, 2017)

Independence Abstractions and Models of Concurrency. - Vijay Victor D'Silva; Daniel Kroening; Marcelo Sousa (VMCAI, 2017)

Efficient Verification of Multi-Property Designs (The Benefit of Wrong Assumptions) (Extended Version). - Eugene Goldberg; Matthias Güdemann; Daniel Kroening; Rajdeep Mukherjee (CoRR, 2017)

Kayak: Safe Semantic Refactoring to Java Streams. - Cristina David; Pascal Kesseli; Daniel Kroening (CoRR, 2017)

Incremental bounded model checking for embedded software. - Peter Schrammel; Daniel Kroening; Martin Brain; Ruben Martins; Tino Teige; Tom Bienmüller (Formal Aspects Comput., 2017)

Lost in abstraction: Monotonicity in multi-threaded programs. - Alexander Kaiser 001; Daniel Kroening; Thomas Wahl (Inf. Comput., 2017)

Don't Sit on the Fence: A Static Analysis Approach to Automatic Fence Insertion. - Jade Alglave; Daniel Kroening; Vincent Nimal; Daniel Poetzl (ACM Trans. Program. Lang. Syst., 2017)

Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs. - Vojtech Forejt; Saurabh Joshi 001; Daniel Kroening; Ganesh Narayanaswamy; Subodh Sharma 001 (ACM Trans. Program. Lang. Syst., 2017)

Model checking, 2nd Edition. - Edmund M. Clarke; Orna Grumberg; Daniel Kroening; Doron A. Peled; Helmut Veith (MIT Press, 2018)

Counterexample Guided Inductive Synthesis Modulo Theories. - Alessandro Abate; Cristina David; Pascal Kesseli; Daniel Kroening; Elizabeth Polgreen (CAV (1), 2018)

JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode. - Lucas C. Cordeiro; Pascal Kesseli; Daniel Kroening; Peter Schrammel; Marek Trtík (CAV (1), 2018)

Efficient verification of multi-property designs (The benefit of wrong assumptions). - Eugene Goldberg; Matthias Güdemann; Daniel Kroening; Rajdeep Mukherjee (DATE, 2018)

Verification of tree-based hierarchical read-copy update in the Linux kernel. - Lihao Liang; Paul E. McKenney; Daniel Kroening; Tom Melham (DATE, 2018)

Optimising Spectrum Based Fault Localisation for Single Fault Programs Using Specifications. - David Landsberg; Youcheng Sun; Daniel Kroening (FASE, 2018)

DSValidator: An Automated Counterexample Reproducibility Tool for Digital Systems. - Lennon C. Chaves; Iury Bessa; Lucas C. Cordeiro; Daniel Kroening (HSCC, 2018)

Concolic testing for deep neural networks. - Youcheng Sun; Min Wu 011; Wenjie Ruan; Xiaowei Huang 001; Marta Kwiatkowska; Daniel Kroening (ASE, 2018)

Automatic Heap Layout Manipulation for Exploitation. - Sean Heelan; Tom Melham; Daniel Kroening (USENIX Security Symposium, 2018)

Logically-Correct Reinforcement Learning. - Mohammadhosein Hasanbeig; Alessandro Abate; Daniel Kroening (CoRR, 2018)

Testing Deep Neural Networks. - Youcheng Sun; Xiaowei Huang 001; Daniel Kroening (CoRR, 2018)

Global Robustness Evaluation of Deep Neural Networks with Provable Guarantees for L0 Norm. - Wenjie Ruan; Min Wu 011; Youcheng Sun; Xiaowei Huang 001; Daniel Kroening; Marta Kwiatkowska (CoRR, 2018)

Evaluating Manual Intervention to Address the Challenges of Bug Finding with KLEE. - John Galea; Sean Heelan; Daniel Neville; Daniel Kroening (CoRR, 2018)

Benchmarking of Java Verification Tools at the Software Verification Competition (SV-COMP). - Lucas C. Cordeiro; Daniel Kroening; Peter Schrammel (ACM SIGSOFT Softw. Eng. Notes, 2018)

Effective Verification for Low-Level Software with Competing Interrupts. - Lihao Liang; Tom Melham; Daniel Kroening; Peter Schrammel; Michael Tautschnig (ACM Trans. Embed. Comput. Syst., 2018)

Bit-Precise Procedure-Modular Termination Analysis. - Hong-Yi Chen; Cristina David; Daniel Kroening; Peter Schrammel; Björn Wachter (ACM Trans. Program. Lang. Syst., 2018)

Program Synthesis for Program Analysis. - Cristina David; Pascal Kesseli; Daniel Kroening; Matt Lewis (ACM Trans. Program. Lang. Syst., 2018)

SAT-Based Model Checking. - Armin Biere; Daniel Kröning (Handbook of Model Checking, 2018)

Towards Verifiable and Safe Model-Free Reinforcement Learning. - Mohammadhosein Hasanbeig; Daniel Kroening; Alessandro Abate (OVERLAY@AI*IA, 2019)

Logically-Constrained Neural Fitted Q-iteration. - Mohammadhosein Hasanbeig; Alessandro Abate; Daniel Kroening (AAMAS, 2019)

Gollum: Modular and Greybox Exploit Generation for Heap Overflows in Interpreters. - Sean Heelan; Tom Melham; Daniel Kroening (CCS, 2019)

Reinforcement Learning for Temporal Logic Control Synthesis with Probabilistic Satisfaction Guarantees. - Mohammadhosein Hasanbeig; Yiannis Kantaros; Alessandro Abate; Daniel Kroening; George J. Pappas; Insup Lee 001 (CDC, 2019)

DeepConcolic: testing and debugging deep neural networks. - Youcheng Sun; Xiaowei Huang 001; Daniel Kroening; James Sharp; Matthew Hill; Rob Ashmore (ICSE (Companion Volume), 2019)

Global Robustness Evaluation of Deep Neural Networks with Provable Guarantees for the Hamming Distance. - Wenjie Ruan; Min Wu 011; Youcheng Sun; Xiaowei Huang 001; Daniel Kroening; Marta Kwiatkowska (IJCAI, 2019)

JBMC: Bounded Model Checking for Java Bytecode - (Competition Contribution). - Lucas C. Cordeiro; Daniel Kroening; Peter Schrammel (TACAS (3), 2019)

Certified Reinforcement Learning with Logic Guidance. - Mohammadhosein Hasanbeig; Alessandro Abate; Daniel Kroening (CoRR, 2019)

Generating Realistic Unrestricted Adversarial Inputs using Dual-Objective GAN Training. - Isaac Dunn; Tom Melham; Daniel Kroening (CoRR, 2019)

CREST: Hardware Formal Verification with ANSI-C Reference Specifications. - Andreas Tiemeyer; Tom Melham; Daniel Kroening; John O'Leary (CoRR, 2019)

Explaining Deep Neural Networks Using Spectrum-Based Fault Localization. - Youcheng Sun; Hana Chockler; Xiaowei Huang 001; Daniel Kroening (CoRR, 2019)

Modular Deep Reinforcement Learning with Temporal Logic Specifications. - Lim Zun Yuan; Mohammadhosein Hasanbeig; Alessandro Abate; Daniel Kroening (CoRR, 2019)

DeepSynth: Program Synthesis for Automatic Task Segmentation in Deep Reinforcement Learning. - Mohammadhosein Hasanbeig; Natasha Yogananda Jeppu; Alessandro Abate; Tom Melham; Daniel Kroening (CoRR, 2019)

Structural Test Coverage Criteria for Deep Neural Networks. - Youcheng Sun; Xiaowei Huang 001; Daniel Kroening; James Sharp; Matthew Hill; Rob Ashmore (ACM Trans. Embed. Comput. Syst., 2019)

Cautious Reinforcement Learning with Logical Constraints. - Mohammadhosein Hasanbeig; Alessandro Abate; Daniel Kroening (AAMAS, 2020)

The Taint Rabbit: Optimizing Generic Taint Analysis with Dynamic Fast Path Generation. - John Galea; Daniel Kroening (AsiaCCS, 2020)

Learning Concise Models from Long Execution Traces. - Natasha Yogananda Jeppu; Thomas F. Melham; Daniel Kroening; John O'Leary (DAC, 2020)

Explaining Image Classifiers Using Statistical Fault Localization. - Youcheng Sun; Hana Chockler; Xiaowei Huang 001; Daniel Kroening (ECCV (28), 2020)

Using model checking tools to triage the severity of security bugs in the Xen hypervisor. - Byron Cook; Björn Döbel; Daniel Kroening; Norbert Manthey; Martin Pohlack; Elizabeth Polgreen; Michael Tautschnig; Pawel Wieczorkiewicz (FMCAD, 2020)

Deep Reinforcement Learning with Temporal Logics. - Mohammadhosein Hasanbeig; Daniel Kroening; Alessandro Abate (FORMATS, 2020)

Automated formal synthesis of provably safe digital controllers for continuous plants. - Alessandro Abate; Iury Bessa; Lucas C. Cordeiro; Cristina David; Pascal Kesseli; Daniel Kroening; Elizabeth Polgreen (Acta Informatica, 2020)

Hardware/Software Co-verification Using Path-based Symbolic Execution. - Rajdeep Mukherjee; Saurabh Joshi 001; John O'Leary; Daniel Kroening; Tom Melham (CoRR, 2020)

CounterExample Guided Neural Synthesis. - Elizabeth Polgreen; Ralph Abboud; Daniel Kroening (CoRR, 2020)

Semantic Adversarial Perturbations using Learnt Representations. - Isaac Dunn; Tom Melham; Daniel Kroening (CoRR, 2020)

A survey of safety and trustworthiness of deep neural networks: Verification, testing, adversarial attack and defence, and interpretability. - Xiaowei Huang 001; Daniel Kroening; Wenjie Ruan; James Sharp; Youcheng Sun; Emese Thamo; Min Wu 011; Xinping Yi (Comput. Sci. Rev., 2020)

Learning the Language of Software Errors. - Hana Chockler; Pascal Kesseli; Daniel Kroening; Ofer Strichman (J. Artif. Intell. Res., 2020)

DeepSynth: Automata Synthesis for Automatic Task Segmentation in Deep Reinforcement Learning. - Mohammadhosein Hasanbeig; Natasha Yogananda Jeppu; Alessandro Abate; Tom Melham; Daniel Kroening (AAAI, 2021)

Shielding Atari Games with Bounded Prescience. - Mirco Giacobbe; Mohammadhosein Hasanbeig; Daniel Kroening; Hjalmar Wijk (AAMAS, 2021)

Explanations for Occluded Images. - Hana Chockler; Daniel Kroening; Youcheng Sun (ICCV, 2021)

Exposing previously undetectable faults in deep neural networks. - Isaac Dunn; Hadrien Pouget; Daniel Kroening; Tom Melham (ISSTA, 2021)

Ranking Policy Decisions. - Hadrien Pouget; Hana Chockler; Youcheng Sun; Daniel Kroening (NeurIPS, 2021)

Compositional Explanations for Image Classifiers. - Hana Chockler; Daniel Kroening; Youcheng Sun (CoRR, 2021)

Active Learning of Abstract System Models from Traces using Model Checking [Extended]. - Natasha Yogananda Jeppu; Tom Melham; Daniel Kroening (CoRR, 2021)

Model checking boot code from AWS data centers. - Byron Cook; Kareem Khazem; Daniel Kroening; Serdar Tasiran; Michael Tautschnig; Mark R. Tuttle (Formal Methods Syst. Des., 2021)

Unbounded-Time Safety Verification of Guarded LTI Models with Inputs by Abstract Acceleration. - Dario Cattaruzza; Alessandro Abate; Peter Schrammel; Daniel Kroening (J. Autom. Reason., 2021)

Software Verification. - Daniel Kroening (Handbook of Satisfiability, 2021)

Active Learning of Abstract System Models from Traces using Model Checking. - Natasha Yogananda Jeppu; Tom Melham; Daniel Kroening (DATE, 2022)

LCRL: Certified Policy Synthesis via Logically-Constrained Reinforcement Learning. - Mohammadhosein Hasanbeig; Daniel Kroening; Alessandro Abate (QEST, 2022)

Neural termination analysis. - Mirco Giacobbe; Daniel Kroening; Julian Parsert (ESEC/SIGSOFT FSE, 2022)

LCRL: Certified Policy Synthesis via Logically-Constrained Reinforcement Learning. - Hosein Hasanbeig; Daniel Kroening; Alessandro Abate (CoRR, 2022)

Enhancing active model learning with equivalence checking using simulation relations. - Natasha Yogananda Jeppu; Tom Melham; Daniel Kroening (Formal Methods Syst. Des., 2022)

2LS for Program Analysis. - Daniel Kroening; Viktor Malík; Peter Schrammel; Tomás Vojnar (CoRR, 2023)

JBMC: A Bounded Model Checking Tool for Java Bytecode. - Romain Brenguier; Lucas C. Cordeiro; Daniel Kroening; Peter Schrammel (CoRR, 2023)

CBMC: The C Bounded Model Checker. - Daniel Kroening; Peter Schrammel; Michael Tautschnig (CoRR, 2023)

Multiple Different Explanations for Image Classifiers. - Hana Chockler; David A. Kelly; Daniel Kroening (CoRR, 2023)

You Only Explain Once. - David A. Kelly; Hana Chockler; Daniel Kroening; Nathan Blake; Aditi Ramaswamy; Melane Navaratnarajah; Aaditya Shivakumar (CoRR, 2023)

Synthesising Programs with Non-trivial Constants. - Alessandro Abate; Haniel Barbosa; Clark W. Barrett; Cristina David; Pascal Kesseli; Daniel Kroening; Elizabeth Polgreen; Andrew Reynolds 001; Cesare Tinelli (J. Autom. Reason., 2023)

Certified reinforcement learning with logic guidance. - Hosein Hasanbeig; Daniel Kroening; Alessandro Abate (Artif. Intell., 2023)

Safeguarded Progress in Reinforcement Learning: Safe Bayesian Exploration for Control Policy Synthesis. - Rohan Mitta; Hosein Hasanbeig; Jun Wang 135; Daniel Kroening; Yiannis Kantaros; Alessandro Abate (AAAI, 2024)

Neural Model Checking. - Mirco Giacobbe; Daniel Kroening; Abhinandan Pal; Michael Tautschnig (NeurIPS, 2024)

VERT: Verified Equivalent Rust Transpilation with Few-Shot Learning. - Aidan Z. H. Yang; Yoshiki Takashima; Brandon Paulsen; Josiah Dodds; Daniel Kroening (CoRR, 2024)

Towards Translating Real-World Code with LLMs: A Study of Translating to Rust. - Hasan Ferit Eniser; Hanliang Zhang; Cristina David; Meng Wang 002; Maria Christakis; Brandon Paulsen; Joey Dodds; Daniel Kroening (CoRR, 2024)

Causal Explanations for Image Classifiers. - Hana Chockler; David A. Kelly; Daniel Kroening; Youcheng Sun (CoRR, 2024)

Symbolic Task Inference in Deep Reinforcement Learning. - Hosein Hasanbeig; Natasha Yogananda Jeppu; Alessandro Abate; Tom Melham; Daniel Kroening (J. Artif. Intell. Res., 2024)

Quantifying the benefits of code hints for refactoring deprecated Java APIs. - Cristina David; Pascal Kesseli; Daniel Kroening; Hanliang Zhang (SIGSOFT FSE Companion, 2025)

Program Synthesis from Partial Traces. - Margarida Ferreira; Victor Nicolet; Joey Dodds; Daniel Kroening (Proc. ACM Program. Lang., 2025)

Scalable, Validated Code Translation of Entire Projects using Large Language Models. - Hanliang Zhang; Cristina David; Meng Wang 002; Brandon Paulsen; Daniel Kroening (Proc. ACM Program. Lang., 2025)

The Secrets Must Not Flow: Scaling Security Verification to Large Codebases (extended version). - Linard Arquint; Samarth Kishor; Jason R. Koenig; Joey Dodds; Daniel Kroening; Peter Müller 001 (CoRR, 2025)