| 2026 | AAAI | Symbolic Task Inference in Deep Reinforcement Learning (Abstract Reprint). | Hosein Hasanbeig, Natasha Yogananda Jeppu, Alessandro Abate, Tom Melham, Daniel Kroening |
| 2026 | SP | The Secrets Must Not Flow: Scaling Security Verification to Large Codebases. | Linard Arquint, Samarth Kishor, Jason R. Koenig, Joey Dodds, Daniel Kroening, Peter Mller |
| 2025 | ECAI | Multiple Different Black Box Explanations for Image Classifiers. | Hana Chockler, David A. Kelly, Daniel Kroening |
| 2024 | AAAI | Safeguarded Progress in Reinforcement Learning: Safe Bayesian Exploration for Control Policy Synthesis. | Rohan Mitta, Hosein Hasanbeig, Jun Wang, Daniel Kroening, Yiannis Kantaros, Alessandro Abate |
| 2022 | DATE | Active Learning of Abstract System Models from Traces using Model Checking. | Natasha Yogananda Jeppu, Tom Melham, Daniel Kroening |
| 2021 | AAAI | DeepSynth: Automata Synthesis for Automatic Task Segmentation in Deep Reinforcement Learning. | Mohammadhosein Hasanbeig, Natasha Yogananda Jeppu, Alessandro Abate, Tom Melham, Daniel Kroening |
| 2021 | ICCV | Explanations for Occluded Images. | Hana Chockler, Daniel Kroening, Youcheng Sun |
| 2021 | ISSTA | Exposing previously undetectable faults in deep neural networks. | Isaac Dunn, Hadrien Pouget, Daniel Kroening, Tom Melham |
| 2020 | CCS | The Taint Rabbit: Optimizing Generic Taint Analysis with Dynamic Fast Path Generation. | John Galea, Daniel Kroening |
| 2020 | DAC | Learning Concise Models from Long Execution Traces. | Natasha Yogananda Jeppu, Thomas F. Melham, Daniel Kroening, John O'Leary |
| 2020 | ECCV | Explaining Image Classifiers Using Statistical Fault Localization. | Youcheng Sun, Hana Chockler, Xiaowei Huang, Daniel Kroening |
| 2020 | FMCAD | Using model checking tools to triage the severity of security bugs in the Xen hypervisor. | Byron Cook, Bjrn Dbel, Daniel Kroening, Norbert Manthey, Martin Pohlack, Elizabeth Polgreen, Michael Tautschnig, Pawel Wieczorkiewicz |
| 2019 | CCS | Gollum: Modular and Greybox Exploit Generation for Heap Overflows in Interpreters. | Sean Heelan, Tom Melham, Daniel Kroening |
| 2019 | IJCAI | Global Robustness Evaluation of Deep Neural Networks with Provable Guarantees for the Hamming Distance. | Wenjie Ruan, Min Wu, Youcheng Sun, Xiaowei Huang, Daniel Kroening, Marta Kwiatkowska |
| 2019 | ICSE | DeepConcolic: testing and debugging deep neural networks. | Youcheng Sun, Xiaowei Huang, Daniel Kroening, James Sharp, Matthew Hill, Rob Ashmore |
| 2019 | ICSE | Structural test coverage criteria for deep neural networks. | Youcheng Sun, Xiaowei Huang, Daniel Kroening, James Sharp, Matthew Hill, Rob Ashmore |
| 2019 | TACAS | JBMC: Bounded Model Checking for Java Bytecode - (Competition Contribution). | Lucas C. Cordeiro, Daniel Kroening, Peter Schrammel |
| 2018 | CAV | Counterexample Guided Inductive Synthesis Modulo Theories. | Alessandro Abate, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen |
| 2018 | CAV | Model Checking Boot Code from AWS Data Centers. | Byron Cook, Kareem Khazem, Daniel Kroening, Serdar Tasiran, Michael Tautschnig, Mark R. Tuttle |
| 2018 | CAV | JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode. | Lucas C. Cordeiro, Pascal Kesseli, Daniel Kroening, Peter Schrammel, Marek Trtk |
| 2018 | DATE | Efficient verification of multi-property designs (The benefit of wrong assumptions). | Eugene Goldberg, Matthias Gdemann, Daniel Kroening, Rajdeep Mukherjee |
| 2018 | DATE | Verification of tree-based hierarchical read-copy update in the Linux kernel. | Lihao Liang, Paul E. McKenney, Daniel Kroening, Tom Melham |
| 2018 | FASE | Optimising Spectrum Based Fault Localisation for Single Fault Programs Using Specifications. | David Landsberg, Youcheng Sun, Daniel Kroening |
| 2017 | ATVA | Lifting CDCL to Template-Based Abstract Domains for Program Verification. | Rajdeep Mukherjee, Peter Schrammel, Leopold Haller, Daniel Kroening, Tom Melham |
| 2017 | CADE | SC-square: when Satisfiability Checking and Symbolic Computation join forces. | Erika brahm, John Abbott, Bernd Becker, Anna Maria Bigatti, Martin Brain, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Vijay Ganesh, Alberto Griggio, Daniel Kroening, Werner M. Seiler |
| 2017 | CAV | 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 |
| 2017 | CAV | Sound Numerical Computations in Abstract Acceleration. | Dario Cattaruzza, Alessandro Abate, Peter Schrammel, Daniel Kroening |
| 2017 | CAV | Abstract Interpretation with Unfoldings. | Marcelo Sousa, Csar Rodrguez, Vijay Victor D'Silva, Daniel Kroening |
| 2017 | DAC | Formal Techniques for Effective Co-verification of Hardware/Software Co-designs. | Rajdeep Mukherjee, Mitra Purandare, Raphael Polig, Daniel Kroening |
| 2017 | ICECCS | 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 |
| 2017 | ISSTA | Verifying digital systems with MATLAB. | Lennon C. Chaves, Iury Bessa, Lucas C. Cordeiro, Daniel Kroening, Eddie Batista de Lima Filho |
| 2017 | SAS | Modular Demand-Driven Analysis of Semantic Difference for Program Versions. | Anna Trostanetski, Orna Grumberg, Daniel Kroening |
| 2017 | VMCAI | Independence Abstractions and Models of Concurrency. | Vijay Victor D'Silva, Daniel Kroening, Marcelo Sousa |
| 2016 | DATE | Unbounded safety verification for hardware using software analyzers. | Rajdeep Mukherjee, Peter Schrammel, Daniel Kroening, Tom Melham |
| 2016 | FM | Danger Invariants. | Cristina David, Pascal Kesseli, Daniel Kroening, Matt Lewis |
| 2016 | FM | Equivalence Checking of a Floating-Point Unit Against a High-Level C Model. | Rajdeep Mukherjee, Saurabh Joshi, Andreas Griesmayer, Daniel Kroening, Tom Melham |
| 2016 | ISSTA | Towards Automated Bounded Model Checking of API Implementations. | Daniel Neville, Andrew J. Malton, Martin Brain, Daniel Kroening |
| 2016 | MASCOTS | Static Program Analysis for Identifying Energy Bugs in Graphics-Intensive Mobile Apps. | Chang Hwan Peter Kim, Daniel Kroening, Marta Z. Kwiatkowska |
| 2016 | PPoPP | The virtues of conflict: analysing modern concurrency. | Ganesh Narayanaswamy, Saurabh Joshi, Daniel Kroening |
| 2016 | SYNASC | Algebraic Techniques in Software Verification : Challenges and Opportunities. | Martin Brain, Daniel Kroening, Ryan McCleeary |
| 2016 | TACAS | v2c - A Verilog to C Translator. | Rajdeep Mukherjee, Michael Tautschnig, Daniel Kroening |
| 2016 | TACAS | Formalizing and Checking Thread Refinement for Data-Race-Free Execution Models. | Daniel Poetzl, Daniel Kroening |
| 2016 | TACAS | 2LS for Program Analysis - (Competition Contribution). | Peter Schrammel, Daniel Kroening |
| 2016 | VMCAI | Automatic Generation of Propagation Complete SAT Encodings. | Martin Brain, Liana Hadarean, Daniel Kroening, Ruben Martins |
| 2015 | ATVA | Learning the Language of Error. | Martin Chapman, Hana Chockler, Pascal Kesseli, Daniel Kroening, Ofer Strichman, Michael Tautschnig |
| 2015 | CONCUR | Unfolding-based Partial Order Reduction. | Csar Rodrguez, Marcelo Sousa, Subodh Sharma, Daniel Kroening |
| 2015 | DATE | Effective verification of low-level software with nested interrupts. | Daniel Kroening, Lihao Liang, Tom Melham, Peter Schrammel, Michael Tautschnig |
| 2015 | DATE | Verifying synchronous reactive systems using lazy abstraction. | Kumar Madhukar, Mandayam K. Srivas, Bjrn Wachter, Daniel Kroening, Ravindra Metta |
| 2015 | ESOP | Unrestricted Termination and Non-termination Arguments for Bit-Vector Programs. | Cristina David, Daniel Kroening, Matt Lewis |
| 2015 | ESOP | Propositional Reasoning about Safety and Termination of Heap-Manipulating Programs. | Cristina David, Daniel Kroening, Matt Lewis |
| 2015 | FASE | Evaluation of Measures for Statistical Fault Localisation and an Optimising Scheme. | David Landsberg, Hana Chockler, Daniel Kroening, Matt Lewis |
| 2015 | FM | Property-Driven Fence Insertion Using Reorder Bounded Model Checking. | Saurabh Joshi, Daniel Kroening |
| 2015 | FM | Proving Safety with Trace Automata and Bounded Model Checking. | Daniel Kroening, Matt Lewis, Georg Weissenbacher |
| 2015 | FMCAD | Accelerating Invariant Generation. | Kumar Madhukar, Bjrn Wachter, Daniel Kroening, Matt Lewis, Mandayam K. Srivas |
| 2015 | FMICS | Successful Use of Incremental BMC in the Automotive Industry. | Peter Schrammel, Daniel Kroening, Martin Brain, Ruben Martins, Tino Teige, Tom Bienmller |
| 2015 | FORTE | On Partial Order Semantics for SAT/SMT-Based Symbolic Encodings of Weak Memory Concurrency. | Alex Horn, Daniel Kroening |
| 2015 | FORTE | Faster Linearizability Checking via P-Compositionality. | Alex Horn, Daniel Kroening |
| 2015 | LPAR | Using Program Synthesis for Program Analysis. | Cristina David, Daniel Kroening, Matt Lewis |
| 2015 | SAS | Safety Verification and Refutation by k-Invariants and k-Induction. | Martin Brain, Saurabh Joshi, Daniel Kroening, Peter Schrammel |
| 2015 | SAS | Unbounded-Time Analysis of Guarded LTI Systems with Inputs by Abstract Acceleration. | Dario Cattaruzza, Alessandro Abate, Peter Schrammel, Daniel Kroening |
| 2014 | CAV | Don't Sit on the Fence - A Static Analysis Approach to Automatic Fence Insertion. | Jade Alglave, Daniel Kroening, Vincent Nimal, Daniel Poetzl |
| 2014 | CONCUR | Lost in Abstraction: Monotonicity in Multi-threaded Programs. | Alexander Kaiser, Daniel Kroening, Thomas Wahl |
| 2014 | ESOP | Model and Proof Generation for Heap-Manipulating Programs. | Martin Brain, Cristina David, Daniel Kroening, Peter Schrammel |
| 2014 | FM | Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs. | Vojtech Forejt, Daniel Kroening, Ganesh Narayanaswamy, Subodh Sharma |
| 2014 | POPL | Abstract satisfaction. | Vijay Victor D'Silva, Leopold Haller, Daniel Kroening |
| 2014 | TACAS | CBMC - C Bounded Model Checker - (Competition Contribution). | Daniel Kroening, Michael Tautschnig |
| 2013 | CAV | Partial Orders for Efficient Bounded Model Checking of Concurrent Software. | Jade Alglave, Daniel Kroening, Michael Tautschnig |
| 2013 | CAV | Under-Approximating Loops in C Programs for Fast Counterexample Detection. | Daniel Kroening, Matt Lewis, Georg Weissenbacher |
| 2013 | ESOP | Software Verification for Weak Memory via Program Transformation. | Jade Alglave, Daniel Kroening, Vincent Nimal, Michael Tautschnig |
| 2013 | ESOP | Counterexample-Guided Precondition Inference. | Mohamed Nassim Seghir, Daniel Kroening |
| 2013 | FMCAD | Formal co-validation of low-level hardware/software interfaces. | Alex Horn, Michael Tautschnig, Celina G. Val, Lihao Liang, Tom Melham, Jim Grundy, Daniel Kroening |
| 2013 | FMCAD | Verifying multi-threaded software with impact. | Bjrn Wachter, Daniel Kroening, Jol Ouaknine |
| 2013 | ICSE | A visual studio plug-in for CProver. | Mohamed Nassim Seghir, Daniel Kroening |
| 2013 | POPL | Abstract conflict driven learning. | Vijay Victor D'Silva, Leopold Haller, Daniel Kroening |
| 2013 | SAS | Interpolation-Based Verification of Floating-Point Programs with Abstract CDCL. | Martin Brain, Vijay Victor D'Silva, Alberto Griggio, Leopold Haller, Daniel Kroening |
| 2013 | VMCAI | An Abstract Interpretation of DPLL(T). | Martin Brain, Vijay Victor D'Silva, Leopold Haller, Alberto Griggio, Daniel Kroening |
| 2013 | VMCAI | Abstraction of Syntax. | Vijay Victor D'Silva, Daniel Kroening |
| 2012 | CONCUR | Efficient Coverability Analysis by Proof Minimization. | Alexander Kaiser, Daniel Kroening, Thomas Wahl |
| 2012 | FMCAD | Deciding floating-point logic with systematic abstraction. | Leopold Haller, Alberto Griggio, Martin Brain, Daniel Kroening |
| 2012 | SAS | Satisfiability Solvers Are Static Analysers. | Vijay Victor D'Silva, Leopold Haller, Daniel Kroening |
| 2012 | TACAS | satabs: A Bit-Precise Verifier for C Programs - (Competition Contribution). | Grard Basler, Alastair F. Donaldson, Alexander Kaiser, Daniel Kroening, Michael Tautschnig, Thomas Wahl |
| 2012 | TACAS | Numeric Bounds Analysis with Conflict-Driven Learning. | Vijay Victor D'Silva, Leopold Haller, Daniel Kroening, Michael Tautschnig |
| 2012 | TACAS | Proving Reachability Using FShell - (Competition Contribution). | Andreas Holzer, Daniel Kroening, Christian Schallhart, Michael Tautschnig, Helmut Veith |
| 2012 | TACAS | Wolverine: Battling Bugs with Interpolants - (Competition Contribution). | Georg Weissenbacher, Daniel Kroening, Sharad Malik |
| 2011 | APLAS | Soundness of Data Flow Analyses for Weak Memory Models. | Jade Alglave, Daniel Kroening, John Lugton, Vincent Nimal, Michael Tautschnig |
| 2011 | ATVA | Making Software Verification Tools Really Work. | Jade Alglave, Alastair F. Donaldson, Daniel Kroening, Michael Tautschnig |
| 2011 | CAV | Symmetry-Aware Predicate Abstraction for Shared-Variable Concurrent Programs. | Alastair F. Donaldson, Alexander Kaiser, Daniel Kroening, Thomas Wahl |
| 2011 | CAV | Linear Completeness Thresholds for Bounded Model Checking. | Daniel Kroening, Jol Ouaknine, Ofer Strichman, Thomas Wahl, James Worrell |
| 2011 | CAV | Interpolation-Based Software Verification with Wolverine. | Daniel Kroening, Georg Weissenbacher |
| 2011 | DAC | Test-case generation for embedded simulink via formal concept analysis. | Nannan He, Philipp Rmmer, Daniel Kroening |
| 2011 | PPoPP | SCRATCH: a tool for automatic analysis of dma races. | Alastair F. Donaldson, Daniel Kroening, Philipp Rmmer |
| 2011 | SAS | Software Verification Using k-Induction. | Alastair F. Donaldson, Leopold Haller, Daniel Kroening, Philipp Rmmer |
| 2011 | TACAS | Loop Summarization and Termination Analysis. | Aliaksei Tsitovich, Natasha Sharygina, Christoph M. Wintersteiger, Daniel Kroening |
| 2011 | VMCAI | Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic. | Angelo Brillout, Daniel Kroening, Philipp Rmmer, Thomas Wahl |
| 2011 | VMCAI | Strengthening Induction-Based Race Checking with Lightweight Static Analysis. | Alastair F. Donaldson, Leopold Haller, Daniel Kroening |
| 2010 | CADE | An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic. | Angelo Brillout, Daniel Kroening, Philipp Rmmer, Thomas Wahl |
| 2010 | CADE | Program Verification via Craig Interpolation for Presburger Arithmetic with Arrays. | Angelo Brillout, Daniel Kroening, Philipp Rmmer, Thomas Wahl |
| 2010 | CADE | Loopfrog - loop summarization for static analysis. | Daniel Kroening, Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich, Christoph M. Wintersteiger |
| 2010 | CAV | Dynamic Cutoff Detection in Parameterized Concurrent Programs. | Alexander Kaiser, Daniel Kroening, Thomas Wahl |
| 2010 | CAV | Termination Analysis with Compositional Transition Invariants. | Daniel Kroening, Natasha Sharygina, Aliaksei Tsitovich, Christoph M. Wintersteiger |
| 2010 | DAC | Coverage in interpolation-based model checking. | Hana Chockler, Daniel Kroening, Mitra Purandare |
| 2010 | LPAR | Interpolating Quantifier-Free Presburger Arithmetic. | Daniel Kroening, Jrme Leroux, Philipp Rmmer |
| 2010 | TACAS | Boom: Taking Boolean Program Model Checking One Step Further. | Grard Basler, Matthew Hague, Daniel Kroening, C.-H. Luke Ong, Thomas Wahl, Haoxian Zhao |
| 2010 | TACAS | Ranking Function Synthesis for Bit-Vector Relations. | Byron Cook, Daniel Kroening, Philipp Rmmer, Christoph M. Wintersteiger |
| 2010 | TACAS | Automatic Analysis of Scratch-Pad Memory Code for Heterogeneous Multicore Processors. | Alastair F. Donaldson, Daniel Kroening, Philipp Rmmer |
| 2010 | VMCAI | Interpolant Strength. | Vijay Victor D'Silva, Daniel Kroening, Mitra Purandare, Georg Weissenbacher |
| 2009 | CAV | Symbolic Counter Abstraction for Concurrent Software. | Grard Basler, Michele Mazzucchi, Thomas Wahl, Daniel Kroening |
| 2009 | DATE | Fixed points for multi-cycle path detection. | Vijay Victor D'Silva, Daniel Kroening |
| 2009 | DATE | Strengthening properties using abstraction refinement. | Mitra Purandare, Thomas Wahl, Daniel Kroening |
| 2009 | FMCAD | Mixed abstractions for floating-point arithmetic. | Angelo Brillout, Daniel Kroening, Thomas Wahl |
| 2009 | SAT | Finding Lean Induced Cycles in Binary Hypercubes. | Yury Chebiryak, Thomas Wahl, Daniel Kroening, Leopold Haller |
| 2008 | ATVA | Loop Summarization Using Abstract Transformers. | Daniel Kroening, Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich, Christoph M. Wintersteiger |
| 2008 | ICCAD | Race analysis for SystemC using model checking. | Nicolas Blanc, Daniel Kroening |
| 2008 | ICCAD | Embedded software verification: challenges and solutions. | Chao Wang, Malay K. Ganai, Shuvendu K. Lahiri, Daniel Kroening |
| 2008 | TACAS | Scoot: A Tool for the Analysis of SystemC Models. | Nicolas Blanc, Daniel Kroening, Natasha Sharygina |
| 2008 | VMCAI | Approximation Refinement for Interpolation-Based Model Checking. | Vijay Victor D'Silva, Mitra Purandare, Daniel Kroening |
| 2007 | DATE | Interactive presentation: Image computation and predicate refinement for RTL verilog using word level proofs. | Daniel Kroening, Natasha Sharygina |
| 2007 | FMCAD | Lifting Propositional Interpolants to the Word-Level. | Daniel Kroening, Georg Weissenbacher |
| 2007 | ICCAD | Formal verification at higher levels of abstraction. | Daniel Kroening, Sanjit A. Seshia |
| 2007 | TACAS | Deciding Bit-Vector Arithmetic with Abstraction. | Randal E. Bryant, Daniel Kroening, Jol Ouaknine, Sanjit A. Seshia, Ofer Strichman, Bryan A. Brady |
| 2007 | TACAS | VCEGAR: Verilog CounterExample Guided Abstraction Refinement. | Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund M. Clarke |
| 2006 | CAV | Counterexamples with Loops for Predicate Abstraction. | Daniel Kroening, Georg Weissenbacher |
| 2006 | FMCAD | Over-Approximating Boolean Programs with Unbounded Thread Creation. | Byron Cook, Daniel Kroening, Natasha Sharygina |
| 2006 | TACAS | Approximating Predicate Images for Bit-Vector Logic. | Daniel Kroening, Natasha Sharygina |
| 2005 | CAV | Cogent: Accurate Theorem Proving for Program Verification. | Byron Cook, Daniel Kroening, Natasha Sharygina |
| 2005 | DAC | Word level predicate abstraction and refinement for verifying RTL verilog. | Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund M. Clarke |
| 2005 | MEMOCODE | Formal verification of SystemC by automatic hardware/software partitioning. | Daniel Kroening, Natasha Sharygina |
| 2005 | TACAS | SATABS: SAT-Based Predicate Abstraction for ANSI-C. | Edmund M. Clarke, Daniel Kroening, Natasha Sharygina, Karen Yorav |
| 2004 | CAV | Understanding Counterexamples with explain. | Alex Groce, Daniel Kroening, Flavio Lerda |
| 2004 | CAV | Abstraction-Based Satisfiability Solving of Presburger Arithmetic. | Daniel Kroening, Jol Ouaknine, Sanjit A. Seshia, Ofer Strichman |
| 2004 | DAC | A SAT-based algorithm for reparameterization in symbolic simulation. | Pankaj Chauhan, Edmund M. Clarke, Daniel Kroening |
| 2004 | DSN | Fault Tolerance Tradeoffs in Moving from Decentralized to Centralized Embedded Systems. | Jennifer Morris, Daniel Kroening, Philip Koopman |
| 2004 | ICCAD | Checking consistency of C and Verilog using predicate abstraction and induction. | Daniel Kroening, Edmund M. Clarke |
| 2004 | ICFEM | Tutorial: Software Model Checking. | Edmund M. Clarke, Daniel Kroening |
| 2004 | ICFEM | Counterexample Guided Abstraction Refinement Via Program Execution. | Daniel Kroening, Alex Groce, Edmund M. Clarke |
| 2004 | ISoLA | Accurate Theorem Proving for Program Verification. | Byron Cook, Daniel Kroening, Natasha Sharygina |
| 2004 | MEMOCODE | Verification of SpecC using predicate abstraction. | Himanshu Jain, Daniel Kroening, Edmund M. Clarke |
| 2004 | TACAS | A Tool for Checking ANSI-C Programs. | Edmund M. Clarke, Daniel Kroening, Flavio Lerda |
| 2004 | VMCAI | Completeness and Complexity of Bounded Model Checking. | Edmund M. Clarke, Daniel Kroening, Jol Ouaknine, Ofer Strichman |
| 2003 | ASPDAC | Hardware verification using ANSI-C programs as a reference. | Edmund M. Clarke, Daniel Kroening |
| 2003 | DAC | Behavioral consistency of C and verilog programs using bounded model checking. | Edmund M. Clarke, Daniel Kroening, Karen Yorav |
| 2003 | ICCD | Specifying and Verifying Systems with Multiple Clocks. | Edmund M. Clarke, Daniel Kroening, Karen Yorav |
| 2003 | VMCAI | Efficient Computation of Recurrence Diameters. | Daniel Kroening, Ofer Strichman |
| 2001 | DAC | Automated Pipeline Design. | Daniel Kroening, Wolfgang J. Paul |
| 2000 | GI | Proving the Correctness of a Complete Microprocessor. | Christian Jacobi, Daniel Kroening |