Daniel Kroening

344 papers A* 41A 46B 44C 11Journal 138Unranked 49

Year	Rank	Type	Title / Venue / Authors
2026	A*	`conf`	Symbolic Task Inference in Deep Reinforcement Learning (Abstract Reprint). AAAI Hosein Hasanbeig, Natasha Yogananda Jeppu, Alessandro Abate, Tom Melham, Daniel Kroening
2026	J	`jnl`	Validated Code Translation for Projects with External Libraries. CoRR Hanliang Zhang, Arindam Sharma, Cristina David, Meng Wang, Brandon Paulsen, Daniel Kroening, Wenjia Ye, Taro Sekiyama
2025	J	`jnl`	Automated Cloud Infrastructure-as-Code Reconciliation with AI Agents. CoRR Zhenning Yang, Hui Guan, Victor Nicolet, Brandon Paulsen, Joey Dodds, Daniel Kroening, Ang Chen
2025	J	`jnl`	Hypergraph-Guided Regex Filter Synthesis for Event-Based Anomaly Detection. CoRR Margarida Ferreira, Victor Nicolet, Luan Pham, Joey Dodds, Daniel Kroening, Inês Lynce, Ruben Martins
2025	J	`jnl`	Large Lemma Miners: Can LLMs do Induction Proofs for Hardware? CoRR Romy Peled, Daniel Kroening, Michael Tautschnig, Yakir Vizel
2025	J	`jnl`	MatchFixAgent: Language-Agnostic Autonomous Repository-Level Code Translation Validation and Repair. CoRR Ali Reza Ibrahimzada, Brandon Paulsen, Reyhaneh Jabbarvand, Joey Dodds, Daniel Kroening
2025	A	`conf`	Multiple Different Black Box Explanations for Image Classifiers. ECAI Hana Chockler, David A. Kelly, Daniel Kroening
2025	J	`jnl`	Program Synthesis From Partial Traces. CoRR Margarida Ferreira, Victor Nicolet, Joey Dodds, Daniel Kroening
2025	J	`jnl`	Program Synthesis from Partial Traces. Proc. ACM Program. Lang. Margarida Ferreira, Victor Nicolet, Joey Dodds, Daniel Kroening
2025	—	`conf`	Quantifying the benefits of code hints for refactoring deprecated Java APIs. SIGSOFT FSE Companion Cristina David, Pascal Kesseli, Daniel Kroening, Hanliang Zhang
2025	J	`jnl`	Scalable, Validated Code Translation of Entire Projects using Large Language Models. Proc. ACM Program. Lang. Hanliang Zhang, Cristina David, Meng Wang, Brandon Paulsen, Daniel Kroening
2025	J	`jnl`	The Secrets Must Not Flow: Scaling Security Verification to Large Codebases (extended version). CoRR Linard Arquint, Samarth Kishor, Jason R. Koenig, Joey Dodds, Daniel Kroening, Peter Müller
2025	A*	`conf`	VERT: Polyglot Verified Equivalent Rust Transpilation with Large Language Models. ASE Aidan Z. H. Yang, Yoshiki Takashima, Brandon Paulsen, Josiah Dodds, Daniel Kroening
2024	J	`jnl`	Causal Explanations for Image Classifiers. CoRR Hana Chockler, David A. Kelly, Daniel Kroening, Youcheng Sun
2024	A*	`conf`	Neural Model Checking. NeurIPS Mirco Giacobbe, Daniel Kroening, Abhinandan Pal, Michael Tautschnig
2024	J	`jnl`	Neural Model Checking. CoRR Mirco Giacobbe, Daniel Kroening, Abhinandan Pal, Michael Tautschnig
2024	J	`jnl`	Quantifying the benefits of code hints for refactoring deprecated Java APIs. CoRR Cristina David, Pascal Kesseli, Daniel Kroening, Hanliang Zhang
2024	A*	`conf`	Safeguarded Progress in Reinforcement Learning: Safe Bayesian Exploration for Control Policy Synthesis. AAAI Rohan Mitta, Hosein Hasanbeig, Jun Wang, Daniel Kroening, Yiannis Kantaros, Alessandro Abate
2024	J	`jnl`	Scalable, Validated Code Translation of Entire Projects using Large Language Models. CoRR Hanliang Zhang, Cristina David, Meng Wang, Brandon Paulsen, Daniel Kroening
2024	J	`jnl`	Symbolic Task Inference in Deep Reinforcement Learning. J. Artif. Intell. Res. Hosein Hasanbeig, Natasha Yogananda Jeppu, Alessandro Abate, Tom Melham, Daniel Kroening
2024	J	`jnl`	Towards Translating Real-World Code with LLMs: A Study of Translating to Rust. CoRR Hasan Ferit Eniser, Hanliang Zhang, Cristina David, Meng Wang, Maria Christakis, Brandon Paulsen, Joey Dodds, Daniel Kroening
2024	J	`jnl`	VERT: Verified Equivalent Rust Transpilation with Few-Shot Learning. CoRR Aidan Z. H. Yang, Yoshiki Takashima, Brandon Paulsen, Josiah Dodds, Daniel Kroening
2023	J	`jnl`	2LS for Program Analysis. CoRR Daniel Kroening, Viktor Malík, Peter Schrammel, Tomás Vojnar
2023	J	`jnl`	CBMC: The C Bounded Model Checker. CoRR Daniel Kroening, Peter Schrammel, Michael Tautschnig
2023	J	`jnl`	Certified reinforcement learning with logic guidance. Artif. Intell. Hosein Hasanbeig, Daniel Kroening, Alessandro Abate
2023	J	`jnl`	JBMC: A Bounded Model Checking Tool for Java Bytecode. CoRR Romain Brenguier, Lucas C. Cordeiro, Daniel Kroening, Peter Schrammel
2023	J	`jnl`	Multiple Different Explanations for Image Classifiers. CoRR Hana Chockler, David A. Kelly, Daniel Kroening
2023	J	`jnl`	Safeguarded Progress in Reinforcement Learning: Safe Bayesian Exploration for Control Policy Synthesis. CoRR Rohan Mitta, Hosein Hasanbeig, Jun Wang, Daniel Kroening, Yiannis Kantaros, Alessandro Abate
2023	J	`jnl`	Synthesising Programs with Non-trivial Constants. J. Autom. Reason. Alessandro Abate, Haniel Barbosa, Clark W. Barrett, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen, Andrew Reynolds, Cesare Tinelli
2023	J	`jnl`	You Only Explain Once. CoRR David A. Kelly, Hana Chockler, Daniel Kroening, Nathan Blake, Aditi Ramaswamy, Melane Navaratnarajah, Aaditya Shivakumar
2022	A	`conf`	Active Learning of Abstract System Models from Traces using Model Checking. DATE Natasha Yogananda Jeppu, Tom Melham, Daniel Kroening
2022	J	`jnl`	Enhancing active model learning with equivalence checking using simulation relations. Formal Methods Syst. Des. Natasha Yogananda Jeppu, Tom Melham, Daniel Kroening
2022	—	`conf`	LCRL: Certified Policy Synthesis via Logically-Constrained Reinforcement Learning. QEST Mohammadhosein Hasanbeig, Daniel Kroening, Alessandro Abate
2022	J	`jnl`	LCRL: Certified Policy Synthesis via Logically-Constrained Reinforcement Learning. CoRR Hosein Hasanbeig, Daniel Kroening, Alessandro Abate
2022	—	`conf`	Neural termination analysis. ESEC/SIGSOFT FSE Mirco Giacobbe, Daniel Kroening, Julian Parsert
2021	J	`jnl`	Active Learning of Abstract System Models from Traces using Model Checking [Extended]. CoRR Natasha Yogananda Jeppu, Tom Melham, Daniel Kroening
2021	J	`jnl`	Compositional Explanations for Image Classifiers. CoRR Hana Chockler, Daniel Kroening, Youcheng Sun
2021	A*	`conf`	DeepSynth: Automata Synthesis for Automatic Task Segmentation in Deep Reinforcement Learning. AAAI Mohammadhosein Hasanbeig, Natasha Yogananda Jeppu, Alessandro Abate, Tom Melham, Daniel Kroening
2021	A*	`conf`	Explanations for Occluded Images. ICCV Hana Chockler, Daniel Kroening, Youcheng Sun
2021	J	`jnl`	Exposing Previously Undetectable Faults in Deep Neural Networks. CoRR Isaac Dunn, Hadrien Pouget, Daniel Kroening, Tom Melham
2021	A	`conf`	Exposing previously undetectable faults in deep neural networks. ISSTA Isaac Dunn, Hadrien Pouget, Daniel Kroening, Tom Melham
2021	J	`jnl`	Model checking boot code from AWS data centers. Formal Methods Syst. Des. Byron Cook, Kareem Khazem, Daniel Kroening, Serdar Tasiran, Michael Tautschnig, Mark R. Tuttle
2021	J	`jnl`	Neural Termination Analysis. CoRR Mirco Giacobbe, Daniel Kroening, Julian Parsert
2021	A*	`conf`	Ranking Policy Decisions. NeurIPS Hadrien Pouget, Hana Chockler, Youcheng Sun, Daniel Kroening
2021	A	`conf`	Shielding Atari Games with Bounded Prescience. AAMAS Mirco Giacobbe, Mohammadhosein Hasanbeig, Daniel Kroening, Hjalmar Wijk
2021	J	`jnl`	Shielding Atari Games with Bounded Prescience. CoRR Mirco Giacobbe, Mohammadhosein Hasanbeig, Daniel Kroening, Hjalmar Wijk
2021	—	`ch.`	Software Verification. Handbook of Satisfiability Daniel Kroening
2021	J	`jnl`	Unbounded-Time Safety Verification of Guarded LTI Models with Inputs by Abstract Acceleration. J. Autom. Reason. Dario Cattaruzza, Alessandro Abate, Peter Schrammel, Daniel Kroening
2020	J	`jnl`	A survey of safety and trustworthiness of deep neural networks: Verification, testing, adversarial attack and defence, and interpretability. Comput. Sci. Rev. Xiaowei Huang, Daniel Kroening, Wenjie Ruan, James Sharp, Youcheng Sun, Emese Thamo, Min Wu, Xinping Yi
2020	J	`jnl`	Automated formal synthesis of provably safe digital controllers for continuous plants. Acta Informatica Alessandro Abate, Iury Bessa, Lucas C. Cordeiro, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen
2020	A	`conf`	Cautious Reinforcement Learning with Logical Constraints. AAMAS Mohammadhosein Hasanbeig, Alessandro Abate, Daniel Kroening
2020	J	`jnl`	Cautious Reinforcement Learning with Logical Constraints. CoRR Mohammadhosein Hasanbeig, Alessandro Abate, Daniel Kroening
2020	J	`jnl`	CounterExample Guided Neural Synthesis. CoRR Elizabeth Polgreen, Ralph Abboud, Daniel Kroening
2020	—	`conf`	Deep Reinforcement Learning with Temporal Logics. FORMATS Mohammadhosein Hasanbeig, Daniel Kroening, Alessandro Abate
2020	—	`conf`	Explaining Image Classifiers Using Statistical Fault Localization. ECCV (28) Youcheng Sun, Hana Chockler, Xiaowei Huang, Daniel Kroening
2020	J	`jnl`	Hardware/Software Co-verification Using Path-based Symbolic Execution. CoRR Rajdeep Mukherjee, Saurabh Joshi, John O'Leary, Daniel Kroening, Tom Melham
2020	A*	`conf`	Learning Concise Models from Long Execution Traces. DAC Natasha Yogananda Jeppu, Thomas F. Melham, Daniel Kroening, John O'Leary
2020	J	`jnl`	Learning Concise Models from Long Execution Traces. CoRR Natasha Yogananda Jeppu, Tom Melham, Daniel Kroening, John O'Leary
2020	J	`jnl`	Learning the Language of Software Errors. J. Artif. Intell. Res. Hana Chockler, Pascal Kesseli, Daniel Kroening, Ofer Strichman
2020	J	`jnl`	Ranking Policy Decisions. CoRR Hadrien Pouget, Hana Chockler, Youcheng Sun, Daniel Kroening
2020	J	`jnl`	Semantic Adversarial Perturbations using Learnt Representations. CoRR Isaac Dunn, Tom Melham, Daniel Kroening
2020	A	`conf`	The Taint Rabbit: Optimizing Generic Taint Analysis with Dynamic Fast Path Generation. AsiaCCS John Galea, Daniel Kroening
2020	J	`jnl`	The Taint Rabbit: Optimizing Generic Taint Analysis with Dynamic Fast Path Generation. CoRR John Galea, Daniel Kroening
2020	B	`conf`	Using model checking tools to triage the severity of security bugs in the Xen hypervisor. FMCAD Byron Cook, Björn Döbel, Daniel Kroening, Norbert Manthey, Martin Pohlack, Elizabeth Polgreen, Michael Tautschnig, Pawel Wieczorkiewicz
2019	J	`jnl`	CREST: Hardware Formal Verification with ANSI-C Reference Specifications. CoRR Andreas Tiemeyer, Tom Melham, Daniel Kroening, John O'Leary
2019	J	`jnl`	Certified Reinforcement Learning with Logic Guidance. CoRR Mohammadhosein Hasanbeig, Alessandro Abate, Daniel Kroening
2019	—	`conf`	DeepConcolic: testing and debugging deep neural networks. ICSE (Companion Volume) Youcheng Sun, Xiaowei Huang, Daniel Kroening, James Sharp, Matthew Hill, Rob Ashmore
2019	J	`jnl`	DeepSynth: Program Synthesis for Automatic Task Segmentation in Deep Reinforcement Learning. CoRR Mohammadhosein Hasanbeig, Natasha Yogananda Jeppu, Alessandro Abate, Tom Melham, Daniel Kroening
2019	J	`jnl`	Explaining Deep Neural Networks Using Spectrum-Based Fault Localization. CoRR Youcheng Sun, Hana Chockler, Xiaowei Huang, Daniel Kroening
2019	J	`jnl`	Generating Realistic Unrestricted Adversarial Inputs using Dual-Objective GAN Training. CoRR Isaac Dunn, Tom Melham, Daniel Kroening
2019	A*	`conf`	Global Robustness Evaluation of Deep Neural Networks with Provable Guarantees for the Hamming Distance. IJCAI Wenjie Ruan, Min Wu, Youcheng Sun, Xiaowei Huang, Daniel Kroening, Marta Kwiatkowska
2019	A*	`conf`	Gollum: Modular and Greybox Exploit Generation for Heap Overflows in Interpreters. CCS Sean Heelan, Tom Melham, Daniel Kroening
2019	—	`conf`	JBMC: Bounded Model Checking for Java Bytecode - (Competition Contribution). TACAS (3) Lucas C. Cordeiro, Daniel Kroening, Peter Schrammel
2019	A	`conf`	Logically-Constrained Neural Fitted Q-iteration. AAMAS Mohammadhosein Hasanbeig, Alessandro Abate, Daniel Kroening
2019	J	`jnl`	Modular Deep Reinforcement Learning with Temporal Logic Specifications. CoRR Lim Zun Yuan, Mohammadhosein Hasanbeig, Alessandro Abate, Daniel Kroening
2019	—	`conf`	Reinforcement Learning for Temporal Logic Control Synthesis with Probabilistic Satisfaction Guarantees. CDC Mohammadhosein Hasanbeig, Yiannis Kantaros, Alessandro Abate, Daniel Kroening, George J. Pappas, Insup Lee
2019	J	`jnl`	Reinforcement Learning for Temporal Logic Control Synthesis with Probabilistic Satisfaction Guarantees. CoRR Mohammadhosein Hasanbeig, Yiannis Kantaros, Alessandro Abate, Daniel Kroening, George J. Pappas, Insup Lee
2019	J	`jnl`	Structural Test Coverage Criteria for Deep Neural Networks. ACM Trans. Embed. Comput. Syst. Youcheng Sun, Xiaowei Huang, Daniel Kroening, James Sharp, Matthew Hill, Rob Ashmore
2019	—	`conf`	Structural test coverage criteria for deep neural networks. ICSE (Companion Volume) Youcheng Sun, Xiaowei Huang, Daniel Kroening, James Sharp, Matthew Hill, Rob Ashmore
2019	—	`conf`	Towards Verifiable and Safe Model-Free Reinforcement Learning. OVERLAY@AI*IA Mohammadhosein Hasanbeig, Daniel Kroening, Alessandro Abate
2018	A*	`conf`	Automatic Heap Layout Manipulation for Exploitation. USENIX Security Symposium Sean Heelan, Tom Melham, Daniel Kroening
2018	J	`jnl`	Automatic Heap Layout Manipulation for Exploitation. CoRR Sean Heelan, Tom Melham, Daniel Kroening
2018	J	`jnl`	Benchmarking of Java Verification Tools at the Software Verification Competition (SV-COMP). CoRR Lucas C. Cordeiro, Daniel Kroening, Peter Schrammel
2018	J	`jnl`	Benchmarking of Java Verification Tools at the Software Verification Competition (SV-COMP). ACM SIGSOFT Softw. Eng. Notes Lucas C. Cordeiro, Daniel Kroening, Peter Schrammel
2018	J	`jnl`	Bit-Precise Procedure-Modular Termination Analysis. ACM Trans. Program. Lang. Syst. Hong-Yi Chen, Cristina David, Daniel Kroening, Peter Schrammel, Björn Wachter
2018	J	`jnl`	Concolic Testing for Deep Neural Networks. CoRR Youcheng Sun, Min Wu, Wenjie Ruan, Xiaowei Huang, Marta Kwiatkowska, Daniel Kroening
2018	A*	`conf`	Concolic testing for deep neural networks. ASE Youcheng Sun, Min Wu, Wenjie Ruan, Xiaowei Huang, Marta Kwiatkowska, Daniel Kroening
2018	—	`conf`	Counterexample Guided Inductive Synthesis Modulo Theories. CAV (1) Alessandro Abate, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen
2018	—	`conf`	DSValidator: An Automated Counterexample Reproducibility Tool for Digital Systems. HSCC Lennon C. Chaves, Iury Bessa, Lucas C. Cordeiro, Daniel Kroening
2018	J	`jnl`	Effective Verification for Low-Level Software with Competing Interrupts. ACM Trans. Embed. Comput. Syst. Lihao Liang, Tom Melham, Daniel Kroening, Peter Schrammel, Michael Tautschnig
2018	A	`conf`	Efficient verification of multi-property designs (The benefit of wrong assumptions). DATE Eugene Goldberg, Matthias Güdemann, Daniel Kroening, Rajdeep Mukherjee
2018	J	`jnl`	Evaluating Manual Intervention to Address the Challenges of Bug Finding with KLEE. CoRR John Galea, Sean Heelan, Daniel Neville, Daniel Kroening
2018	J	`jnl`	Global Robustness Evaluation of Deep Neural Networks with Provable Guarantees for L0 Norm. CoRR Wenjie Ruan, Min Wu, Youcheng Sun, Xiaowei Huang, Daniel Kroening, Marta Kwiatkowska
2018	—	`conf`	JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode. CAV (1) Lucas C. Cordeiro, Pascal Kesseli, Daniel Kroening, Peter Schrammel, Marek Trtík
2018	J	`jnl`	Logically-Constrained Neural Fitted Q-Iteration. CoRR Mohammadhosein Hasanbeig, Alessandro Abate, Daniel Kroening
2018	J	`jnl`	Logically-Correct Reinforcement Learning. CoRR Mohammadhosein Hasanbeig, Alessandro Abate, Daniel Kroening
2018	—	`conf`	Model Checking Boot Code from AWS Data Centers. CAV (2) Byron Cook, Kareem Khazem, Daniel Kroening, Serdar Tasiran, Michael Tautschnig, Mark R. Tuttle
2018	—	`book`	Model checking, 2nd Edition. Edmund M. Clarke, Orna Grumberg, Daniel Kroening, Doron A. Peled, Helmut Veith
2018	B	`conf`	Optimising Spectrum Based Fault Localisation for Single Fault Programs Using Specifications. FASE David Landsberg, Youcheng Sun, Daniel Kroening
2018	J	`jnl`	Program Synthesis for Program Analysis. ACM Trans. Program. Lang. Syst. Cristina David, Pascal Kesseli, Daniel Kroening, Matt Lewis
2018	J	`jnl`	Testing Deep Neural Networks. CoRR Youcheng Sun, Xiaowei Huang, Daniel Kroening
2018	A	`conf`	Verification of tree-based hierarchical read-copy update in the Linux kernel. DATE Lihao Liang, Paul E. McKenney, Daniel Kroening, Tom Melham
2017	—	`conf`	Abstract Interpretation with Unfoldings. CAV (2) Marcelo Sousa, César Rodríguez, Vijay Victor D'Silva, Daniel Kroening
2017	J	`jnl`	Abstract Interpretation with Unfoldings. CoRR Marcelo Sousa, César Rodríguez, Vijay Victor D'Silva, Daniel Kroening
2017	—	`conf`	Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants. CAV (1) Alessandro Abate, Iury Bessa, Dario Cattaruzza, Lucas C. Cordeiro, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen
2017	J	`jnl`	Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants. CoRR Alessandro Abate, Iury Bessa, Dario Cattaruzza, Lucas C. Cordeiro, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen
2017	A*	`conf`	DSSynth: an automated digital controller synthesis tool for physical plants. ASE Alessandro Abate, Iury Bessa, Dario Cattaruzza, Lennon C. Chaves, Lucas C. Cordeiro, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen
2017	J	`jnl`	Don't Sit on the Fence: A Static Analysis Approach to Automatic Fence Insertion. ACM Trans. Program. Lang. Syst. Jade Alglave, Daniel Kroening, Vincent Nimal, Daniel Poetzl
2017	J	`jnl`	Efficient Verification of Multi-Property Designs (The Benefit of Wrong Assumptions) (Extended Version). CoRR Eugene Goldberg, Matthias Güdemann, Daniel Kroening, Rajdeep Mukherjee
2017	A*	`conf`	Formal Techniques for Effective Co-verification of Hardware/Software Co-designs. DAC Rajdeep Mukherjee, Mitra Purandare, Raphael Polig, Daniel Kroening
2017	B	`conf`	Functional Requirements-Based Automated Testing for Avionics. ICECCS Youcheng Sun, Martin Brain, Daniel Kroening, Andrew Hawthorn, Thomas Wilson, Florian Schanda, Francisco Javier Guzman Jimenez, Simon Daniel, Chris Bryan, Ian Broster
2017	J	`jnl`	Functional Requirements-Based Automated Testing for Avionics. CoRR Youcheng Sun, Martin Brain, Daniel Kroening, Andrew Hawthorn, Thomas Wilson, Florian Schanda, Francisco Javier Guzman Jimenez, Simon Daniel, Chris Bryan, Ian Broster
2017	J	`jnl`	Incremental bounded model checking for embedded software. Formal Aspects Comput. Peter Schrammel, Daniel Kroening, Martin Brain, Ruben Martins, Tino Teige, Tom Bienmüller
2017	B	`conf`	Independence Abstractions and Models of Concurrency. VMCAI Vijay Victor D'Silva, Daniel Kroening, Marcelo Sousa
2017	J	`jnl`	Kayak: Safe Semantic Refactoring to Java Streams. CoRR Cristina David, Pascal Kesseli, Daniel Kroening
2017	B	`conf`	Lifting CDCL to Template-Based Abstract Domains for Program Verification. ATVA Rajdeep Mukherjee, Peter Schrammel, Leopold Haller, Daniel Kroening, Tom Melham
2017	J	`jnl`	Lifting CDCL to Template-based Abstract Domains for Program Verification. CoRR Rajdeep Mukherjee, Peter Schrammel, Leopold Haller, Daniel Kroening, Tom Melham
2017	J	`jnl`	Lost in abstraction: Monotonicity in multi-threaded programs. Inf. Comput. Alexander Kaiser, Daniel Kroening, Thomas Wahl
2017	B	`conf`	Modular Demand-Driven Analysis of Semantic Difference for Program Versions. SAS Anna Trostanetski, Orna Grumberg, Daniel Kroening
2017	J	`jnl`	Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs. ACM Trans. Program. Lang. Syst. Vojtech Forejt, Saurabh Joshi, Daniel Kroening, Ganesh Narayanaswamy, Subodh Sharma
2017	—	`conf`	SC-square: when Satisfiability Checking and Symbolic Computation join forces. ARCADE@CADE Erika Ábrahám, 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	—	`conf`	Sound Numerical Computations in Abstract Acceleration. NSV@CAV Dario Cattaruzza, Alessandro Abate, Peter Schrammel, Daniel Kroening
2017	—	`conf`	Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants. HSCC Alessandro Abate, Iury Bessa, Dario Cattaruzza, Lucas C. Cordeiro, Cristina David, Pascal Kesseli, Daniel Kroening
2017	J	`jnl`	Verifying Digital Systems with MATLAB. CoRR Lennon C. Chaves, Iury Bessa, Lucas C. Cordeiro, Daniel Kroening, Eddie Batista de Lima Filho
2017	A	`conf`	Verifying digital systems with MATLAB. ISSTA Lennon C. Chaves, Iury Bessa, Lucas C. Cordeiro, Daniel Kroening, Eddie Batista de Lima Filho
2016	A	`conf`	2LS for Program Analysis - (Competition Contribution). TACAS Peter Schrammel, Daniel Kroening
2016	—	`conf`	Algebraic Techniques in Software Verification : Challenges and Opportunities. SC²@SYNASC Martin Brain, Daniel Kroening, Ryan McCleeary
2016	—	`conf`	Assisted Coverage Closure. NFM Adam Nellis, Pascal Kesseli, Philippa Ryan Conmy, Daniel Kroening, Peter Schrammel, Michael Tautschnig
2016	B	`conf`	Automatic Generation of Propagation Complete SAT Encodings. VMCAI Martin Brain, Liana Hadarean, Daniel Kroening, Ruben Martins
2016	B	`conf`	Danger Invariants. FM Cristina David, Pascal Kesseli, Daniel Kroening, Matt Lewis
2016	—	`book`	Decision Procedures - An Algorithmic Point of View, Second Edition Daniel Kroening, Ofer Strichman
2016	J	`jnl`	Equivalence Checking a Floating-point Unit against a High-level C Model (Extended Version). CoRR Rajdeep Mukherjee, Saurabh Joshi, Andreas Griesmayer, Daniel Kroening, Tom Melham
2016	B	`conf`	Equivalence Checking of a Floating-Point Unit Against a High-Level C Model. FM Rajdeep Mukherjee, Saurabh Joshi, Andreas Griesmayer, Daniel Kroening, Tom Melham
2016	A	`conf`	Formalizing and Checking Thread Refinement for Data-Race-Free Execution Models. TACAS Daniel Poetzl, Daniel Kroening
2016	J	`jnl`	Generating test case chains for reactive systems. Int. J. Softw. Tools Technol. Transf. Peter Schrammel, Tom Melham, Daniel Kroening
2016	J	`jnl`	Preface: Special Issue on Interpolation. J. Autom. Reason. Daniel Kroening, Andrey Rybalchenko
2016	—	`conf`	Probabilistic Fault Localisation. Haifa Verification Conference David Landsberg, Hana Chockler, Daniel Kroening
2016	C	`conf`	SC CICM Erika Ábrahám, John Abbott, Bernd Becker, Anna Maria Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner M. Seiler, Thomas Sturm
2016	J	`jnl`	Satisfiability Checking and Symbolic Computation. CoRR Erika Ábrahám, John Abbott, Bernd Becker, Anna Maria Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner M. Seiler, Thomas Sturm
2016	J	`jnl`	Satisfiability Checking meets Symbolic Computation (Project Paper). CoRR Erika Ábrahám, John Abbott, Bernd Becker, Anna Maria Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner M. Seiler, Thomas Sturm
2016	J	`jnl`	Satisfiability checking and symbolic computation. ACM Commun. Comput. Algebra Erika Ábrahám, John Abbott, Bernd Becker, Anna Maria Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner M. Seiler, Thomas Sturm
2016	J	`jnl`	Sound Static Deadlock Analysis for C/Pthreads (Extended Version). CoRR Daniel Kroening, Daniel Poetzl, Peter Schrammel, Björn Wachter
2016	J	`jnl`	Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants. CoRR Alessandro Abate, Iury Bessa, Dario Cattaruzza, Lucas C. Cordeiro, Cristina David, Pascal Kesseli, Daniel Kroening
2016	A*	`conf`	Sound static deadlock analysis for C/Pthreads. ASE Daniel Kroening, Daniel Poetzl, Peter Schrammel, Björn Wachter
2016	B	`conf`	Static Program Analysis for Identifying Energy Bugs in Graphics-Intensive Mobile Apps. MASCOTS Chang Hwan Peter Kim, Daniel Kroening, Marta Z. Kwiatkowska
2016	J	`jnl`	The Virtues of Conflict: Analyzing Modern Concurrency. CoRR Ganesh Narayanaswamy, Saurabh Joshi, Daniel Kroening
2016	B	`conf`	The virtues of conflict: analysing modern concurrency. PPoPP Ganesh Narayanaswamy, Saurabh Joshi, Daniel Kroening
2016	—	`conf`	Towards Automated Bounded Model Checking of API Implementations. CSTVA@ISSTA Daniel Neville, Andrew J. Malton, Martin Brain, Daniel Kroening
2016	A	`conf`	Unbounded safety verification for hardware using software analyzers. DATE Rajdeep Mukherjee, Peter Schrammel, Daniel Kroening, Tom Melham
2016	—	`ch.`	Verification of Concurrent Software. Dependable Software Systems Engineering Daniel Kroening
2016	J	`jnl`	Verification of the Tree-Based Hierarchical Read-Copy Update in the Linux Kernel. CoRR Lihao Liang, Paul E. McKenney, Daniel Kroening, Tom Melham
2016	A	`conf`	v2c - A Verilog to C Translator. TACAS Rajdeep Mukherjee, Michael Tautschnig, Daniel Kroening
2015	B	`conf`	Accelerating Invariant Generation. FMCAD Kumar Madhukar, Björn Wachter, Daniel Kroening, Matt Lewis, Mandayam K. Srivas
2015	J	`jnl`	Assisted Coverage Closure. CoRR Adam Nellis, Pascal Kesseli, Philippa Ryan Conmy, Daniel Kroening, Peter Schrammel, Michael Tautschnig
2015	—	`ch.`	Challenges of Existing Technology. Validation of Evolving Software Hana Chockler, Daniel Kroening, Leonardo Mariani, Natasha Sharygina
2015	—	`ch.`	Complementarities Among the Technologies Presented in the Book. Validation of Evolving Software Hana Chockler, Daniel Kroening, Leonardo Mariani, Natasha Sharygina
2015	—	`ed.`	Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I CAV (1) Daniel Kroening, Corina S. Pasareanu
2015	—	`ed.`	Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II CAV (2) Daniel Kroening, Corina S. Pasareanu
2015	J	`jnl`	Danger Invariants. CoRR Cristina David, Daniel Kroening, Matt Lewis
2015	A	`conf`	Effective verification of low-level software with nested interrupts. DATE Daniel Kroening, Lihao Liang, Tom Melham, Peter Schrammel, Michael Tautschnig
2015	—	`conf`	Equivalence Checking Using Trace Partitioning. ISVLSI Rajdeep Mukherjee, Daniel Kroening, Tom Melham, Mandayam K. Srivas
2015	B	`conf`	Evaluation of Measures for Statistical Fault Localisation and an Optimising Scheme. FASE David Landsberg, Hana Chockler, Daniel Kroening, Matt Lewis
2015	C	`conf`	Faster Linearizability Checking via P-Compositionality. FORTE Alex Horn, Daniel Kroening
2015	J	`jnl`	Faster linearizability checking via $P$-compositionality. CoRR Alex Horn, Daniel Kroening
2015	J	`jnl`	Formalizing and Checking Thread Refinement for Data-Race-Free Execution Models (Extended Version). CoRR Daniel Poetzl, Daniel Kroening
2015	—	`conf`	From AgentSpeak to C for Safety Considerations in Unmanned Aerial Vehicles. TAROS Samuel Bucheli, Daniel Kroening, Ruben Martins, Ashutosh Natraj
2015	—	`conf`	Hardware Verification Using Software Analyzers. ISVLSI Rajdeep Mukherjee, Daniel Kroening, Tom Melham
2015	—	`ch.`	Introduction. Validation of Evolving Software Hana Chockler, Daniel Kroening, Leonardo Mariani, Natasha Sharygina
2015	B	`conf`	Learning the Language of Error. ATVA Martin Chapman, Hana Chockler, Pascal Kesseli, Daniel Kroening, Ofer Strichman, Michael Tautschnig
2015	—	`ch.`	Measuring Change Impact on Program Behaviour. Validation of Evolving Software Ajitha Rajan, Daniel Kroening
2015	C	`conf`	On Partial Order Semantics for SAT/SMT-Based Symbolic Encodings of Weak Memory Concurrency. FORTE Alex Horn, Daniel Kroening
2015	J	`jnl`	On partial order semantics for SAT/SMT-based symbolic encodings of weak memory concurrency. CoRR Alex Horn, Daniel Kroening
2015	B	`conf`	Property-Driven Fence Insertion Using Reorder Bounded Model Checking. FM Saurabh Joshi, Daniel Kroening
2015	A	`conf`	Propositional Reasoning about Safety and Termination of Heap-Manipulating Programs. ESOP Cristina David, Daniel Kroening, Matt Lewis
2015	B	`conf`	Proving Safety with Trace Automata and Bounded Model Checking. FM Daniel Kroening, Matt Lewis, Georg Weissenbacher
2015	B	`conf`	Safety Verification and Refutation by k-Invariants and k-Induction. SAS Martin Brain, Saurabh Joshi, Daniel Kroening, Peter Schrammel
2015	J	`jnl`	Safety Verification and Refutation by k-invariants and k-induction (extended version). CoRR Martin Brain, Saurabh Joshi, Daniel Kroening, Peter Schrammel
2015	C	`conf`	Successful Use of Incremental BMC in the Automotive Industry. FMICS Peter Schrammel, Daniel Kroening, Martin Brain, Ruben Martins, Tino Teige, Tom Bienmüller
2015	A*	`conf`	Synthesising Interprocedural Bit-Precise Termination Proofs (T). ASE Hong-Yi Chen, Cristina David, Daniel Kroening, Peter Schrammel, Björn Wachter
2015	J	`jnl`	Synthesising Interprocedural Bit-Precise Termination Proofs (extended version). CoRR Hong-Yi Chen, Cristina David, Daniel Kroening, Peter Schrammel, Björn Wachter
2015	J	`jnl`	Unbounded-Time Analysis of Guarded LTI Systems with Inputs by Abstract Acceleration (extended version). CoRR Dario Cattaruzza, Alessandro Abate, Peter Schrammel, Daniel Kroening
2015	B	`conf`	Unbounded-Time Analysis of Guarded LTI Systems with Inputs by Abstract Acceleration. SAS Dario Cattaruzza, Alessandro Abate, Peter Schrammel, Daniel Kroening
2015	J	`jnl`	Under-approximating loops in C programs for fast counterexample detection. Formal Methods Syst. Des. Daniel Kroening, Matt Lewis, Georg Weissenbacher
2015	B	`conf`	Unfolding-based Partial Order Reduction. CONCUR César Rodríguez, Marcelo Sousa, Subodh Sharma, Daniel Kroening
2015	J	`jnl`	Unfolding-based Partial Order Reduction. CoRR César Rodríguez, Marcelo Sousa, Subodh Sharma, Daniel Kroening
2015	A	`conf`	Unrestricted Termination and Non-termination Arguments for Bit-Vector Programs. ESOP Cristina David, Daniel Kroening, Matt Lewis
2015	B	`conf`	Using Program Synthesis for Program Analysis. LPAR Cristina David, Daniel Kroening, Matt Lewis
2015	J	`jnl`	Using Program Synthesis for Program Analysis. CoRR Cristina David, Daniel Kroening, Matt Lewis
2015	—	`book`	Validation of Evolving Software Hana Chockler, Daniel Kroening, Leonardo Mariani, Natasha Sharygina
2015	A	`conf`	Verifying synchronous reactive systems using lazy abstraction. DATE Kumar Madhukar, Mandayam K. Srivas, Björn Wachter, Daniel Kroening, Ravindra Metta
2014	J	`jnl`	A Widening Approach to Multithreaded Program Verification. ACM Trans. Program. Lang. Syst. Alexander Kaiser, Daniel Kroening, Thomas Wahl
2014	J	`jnl`	AbPress: Flexing Partial-Order Reduction and Abstraction. CoRR Daniel Kroening, Subodh Sharma, Björn Wachter
2014	A*	`conf`	Abstract satisfaction. POPL Vijay Victor D'Silva, Leopold Haller, Daniel Kroening
2014	A*	`conf`	Accelerated test execution using GPUs. ASE Ajitha Rajan, Subodh Sharma, Peter Schrammel, Daniel Kroening
2014	—	`conf`	Automating Software Analysis at Large Scale. MEMICS Daniel Kroening, Michael Tautschnig
2014	A	`conf`	CBMC - C Bounded Model Checker - (Competition Contribution). TACAS Daniel Kroening, Michael Tautschnig
2014	—	`conf`	Camera-laser projector stereo system based anti-collision system for robotic wheelchair users with cognitive impairment. MFI Ashutosh Natraj, Shailendra Natraj, Sonia Waharte, Daniel Kroening
2014	J	`jnl`	Deciding floating-point logic with abstract conflict driven clause learning. Formal Methods Syst. Des. Martin Brain, Vijay Victor D'Silva, Alberto Griggio, Leopold Haller, Daniel Kroening
2014	J	`jnl`	Decision Procedures and Abstract Interpretation (Dagstuhl Seminar 14351). Dagstuhl Reports Daniel Kroening, Thomas W. Reps, Sanjit A. Seshia, Aditya V. Thakur
2014	A*	`conf`	Don't Sit on the Fence - A Static Analysis Approach to Automatic Fence Insertion. CAV Jade Alglave, Daniel Kroening, Vincent Nimal, Daniel Poetzl
2014	J	`jnl`	Incremental Bounded Model Checking for Embedded Software (extended version). CoRR Peter Schrammel, Daniel Kroening, Martin Brain, Ruben Martins, Tino Teige, Tom Bienmüller
2014	J	`jnl`	Lost in Abstraction: Monotonicity in Multi-Threaded Programs (Extended Technical Report). CoRR Alexander Kaiser, Daniel Kroening, Thomas Wahl
2014	B	`conf`	Lost in Abstraction: Monotonicity in Multi-threaded Programs. CONCUR Alexander Kaiser, Daniel Kroening, Thomas Wahl
2014	A	`conf`	Model and Proof Generation for Heap-Manipulating Programs. ESOP Martin Brain, Cristina David, Daniel Kroening, Peter Schrammel
2014	J	`jnl`	Next Generation Static Software Analysis Tools (Dagstuhl Seminar 14352). Dagstuhl Reports Patrick Cousot, Daniel Kroening, Carsten Sinz
2014	B	`conf`	Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs. FM Vojtech Forejt, Daniel Kroening, Ganesh Narayanaswamy, Subodh Sharma
2014	J	`jnl`	Property-Driven Fence Insertion using Reorder Bounded Model Checking. CoRR Saurabh Joshi, Daniel Kroening
2014	J	`jnl`	Propositional Reasoning about Safety and Termination of Heap-Manipulating Programs. CoRR Cristina David, Daniel Kroening, Matt Lewis
2014	J	`jnl`	Proving Safety with Trace Automata and Bounded Model Checking. CoRR Daniel Kroening, Matt Lewis, Georg Weissenbacher
2014	J	`jnl`	Second-Order SAT Solving using Program Synthesis. CoRR Daniel Kroening, Matt Lewis
2014	J	`jnl`	Unrestricted Termination and Non-Termination Arguments for Bit-Vector Programs. CoRR Cristina David, Daniel Kroening, Matt Lewis
2014	—	`ed.`	Verified Software: Theories, Tools and Experiments - 6th International Conference, VSTTE 2014, Vienna, Austria, July 17-18, 2014, Revised Selected Papers VSTTE Dimitra Giannakopoulou, Daniel Kroening
2013	—	`conf`	A visual studio plug-in for CProver. TOPI@ICSE Mohamed Nassim Seghir, Daniel Kroening
2013	A*	`conf`	Abstract conflict driven learning. POPL Vijay Victor D'Silva, Leopold Haller, Daniel Kroening
2013	B	`conf`	Abstraction of Syntax. VMCAI Vijay Victor D'Silva, Daniel Kroening
2013	B	`conf`	An Abstract Interpretation of DPLL(T). VMCAI Martin Brain, Vijay Victor D'Silva, Leopold Haller, Alberto Griggio, Daniel Kroening
2013	—	`conf`	Automated Verification of Concurrent Software. RP Daniel Kroening
2013	J	`jnl`	Chaining Test Cases for Reactive System Testing (extended version). CoRR Peter Schrammel, Tom Melham, Daniel Kroening
2013	C	`conf`	Chaining Test Cases for Reactive System Testing. ICTSS Peter Schrammel, Tom Melham, Daniel Kroening
2013	A	`conf`	Counterexample-Guided Precondition Inference. ESOP Mohamed Nassim Seghir, Daniel Kroening
2013	J	`jnl`	Don't sit on the fence: A static analysis approach to automatic fence insertion. CoRR Jade Alglave, Daniel Kroening, Vincent Nimal, Daniel Poetzl
2013	B	`conf`	Formal co-validation of low-level hardware/software interfaces. FMCAD Alex Horn, Michael Tautschnig, Celina G. Val, Lihao Liang, Tom Melham, Jim Grundy, Daniel Kroening
2013	B	`conf`	Interpolation-Based Verification of Floating-Point Programs with Abstract CDCL. SAS Martin Brain, Vijay Victor D'Silva, Alberto Griggio, Leopold Haller, Daniel Kroening
2013	J	`jnl`	Loop summarization using state and transition invariants. Formal Methods Syst. Des. Daniel Kroening, Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich, Christoph M. Wintersteiger
2013	J	`jnl`	Partial Orders for Efficient BMC of Concurrent Software CoRR Jade Alglave, Daniel Kroening, Michael Tautschnig
2013	A*	`conf`	Partial Orders for Efficient Bounded Model Checking of Concurrent Software. CAV Jade Alglave, Daniel Kroening, Michael Tautschnig
2013	J	`jnl`	Preface to the special issue "SI: Satisfiability Modulo Theories". Formal Methods Syst. Des. Ofer Strichman, Daniel Kroening
2013	J	`jnl`	Ranking function synthesis for bit-vector relations. Formal Methods Syst. Des. Byron Cook, Daniel Kroening, Philipp Rümmer, Christoph M. Wintersteiger
2013	A	`conf`	Software Verification for Weak Memory via Program Transformation. ESOP Jade Alglave, Daniel Kroening, Vincent Nimal, Michael Tautschnig
2013	A*	`conf`	Under-Approximating Loops in C Programs for Fast Counterexample Detection. CAV Daniel Kroening, Matt Lewis, Georg Weissenbacher
2013	B	`conf`	Verifying multi-threaded software with impact. FMCAD Björn Wachter, Daniel Kroening, Joël Ouaknine
2012	J	`jnl`	Computing Mutation Coverage in Interpolation-Based Model Checking. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Hana Chockler, Daniel Kroening, Mitra Purandare
2012	J	`jnl`	Counterexample-guided abstraction refinement for symmetric concurrent programs. Formal Methods Syst. Des. Alastair F. Donaldson, Alexander Kaiser, Daniel Kroening, Michael Tautschnig, Thomas Wahl
2012	B	`conf`	Deciding floating-point logic with systematic abstraction. FMCAD Leopold Haller, Alberto Griggio, Martin Brain, Daniel Kroening
2012	B	`conf`	Efficient Coverability Analysis by Proof Minimization. CONCUR Alexander Kaiser, Daniel Kroening, Thomas Wahl
2012	A	`conf`	Numeric Bounds Analysis with Conflict-Driven Learning. TACAS Vijay Victor D'Silva, Leopold Haller, Daniel Kroening, Michael Tautschnig
2012	A	`conf`	Proving Reachability Using FShell - (Competition Contribution). TACAS Andreas Holzer, Daniel Kroening, Christian Schallhart, Michael Tautschnig, Helmut Veith
2012	B	`conf`	Satisfiability Solvers Are Static Analysers. SAS Vijay Victor D'Silva, Leopold Haller, Daniel Kroening
2012	J	`jnl`	Software Verification for Weak Memory via Program Transformation CoRR Jade Alglave, Daniel Kroening, Vincent Nimal, Michael Tautschnig
2012	A	`conf`	Wolverine: Battling Bugs with Interpolants - (Competition Contribution). TACAS Georg Weissenbacher, Daniel Kroening, Sharad Malik
2012	A	`conf`	satabs: A Bit-Precise Verifier for C Programs - (Competition Contribution). TACAS Gérard Basler, Alastair F. Donaldson, Alexander Kaiser, Daniel Kroening, Michael Tautschnig, Thomas Wahl
2011	J	`jnl`	An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic. J. Autom. Reason. Angelo Brillout, Daniel Kroening, Philipp Rümmer, Thomas Wahl
2011	J	`jnl`	Automatic analysis of DMA races using model checking and Formal Methods Syst. Des. Alastair F. Donaldson, Daniel Kroening, Philipp Rümmer
2011	B	`conf`	Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic. VMCAI Angelo Brillout, Daniel Kroening, Philipp Rümmer, Thomas Wahl
2011	J	`jnl`	Editorial. Formal Aspects Comput. Daniel Kroening, Tiziana Margaria, Jim Woodcock
2011	—	`ed.`	Hardware and Software: Verification and Testing - 6th International Haifa Verification Conference, HVC 2010, Haifa, Israel, October 4-7, 2010. Revised Selected Papers Haifa Verification Conference Sharon Barner, Ian G. Harris, Daniel Kroening, Orna Raz
2011	A*	`conf`	Interpolation-Based Software Verification with Wolverine. CAV Daniel Kroening, Georg Weissenbacher
2011	A*	`conf`	Linear Completeness Thresholds for Bounded Model Checking. CAV Daniel Kroening, Joël Ouaknine, Ofer Strichman, Thomas Wahl, James Worrell
2011	A	`conf`	Loop Summarization and Termination Analysis. TACAS Aliaksei Tsitovich, Natasha Sharygina, Christoph M. Wintersteiger, Daniel Kroening
2011	B	`conf`	Making Software Verification Tools Really Work. ATVA Jade Alglave, Alastair F. Donaldson, Daniel Kroening, Michael Tautschnig
2011	B	`conf`	SCRATCH: a tool for automatic analysis of dma races. PPoPP Alastair F. Donaldson, Daniel Kroening, Philipp Rümmer
2011	B	`conf`	Software Verification Using k-Induction. SAS Alastair F. Donaldson, Leopold Haller, Daniel Kroening, Philipp Rümmer
2011	B	`conf`	Soundness of Data Flow Analyses for Weak Memory Models. APLAS Jade Alglave, Daniel Kroening, John Lugton, Vincent Nimal, Michael Tautschnig
2011	B	`conf`	Strengthening Induction-Based Race Checking with Lightweight Static Analysis. VMCAI Alastair F. Donaldson, Leopold Haller, Daniel Kroening
2011	J	`jnl`	Symmetry-Aware Predicate Abstraction for Shared-Variable Concurrent Programs (Extended Technical Report) CoRR Alastair F. Donaldson, Alexander Kaiser, Daniel Kroening, Thomas Wahl
2011	A*	`conf`	Symmetry-Aware Predicate Abstraction for Shared-Variable Concurrent Programs. CAV Alastair F. Donaldson, Alexander Kaiser, Daniel Kroening, Thomas Wahl
2011	A*	`conf`	Test-case generation for embedded simulink via formal concept analysis. DAC Nannan He, Philipp Rümmer, Daniel Kroening
2010	A	`conf`	An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic. IJCAR Angelo Brillout, Daniel Kroening, Philipp Rümmer, Thomas Wahl
2010	A	`conf`	Automatic Analysis of Scratch-Pad Memory Code for Heterogeneous Multicore Processors. TACAS Alastair F. Donaldson, Daniel Kroening, Philipp Rümmer
2010	J	`jnl`	Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic (Extended Technical Report) CoRR Angelo Brillout, Daniel Kroening, Philipp Rümmer, Thomas Wahl
2010	A	`conf`	Boom: Taking Boolean Program Model Checking One Step Further. TACAS Gérard Basler, Matthew Hague, Daniel Kroening, C.-H. Luke Ong, Thomas Wahl, Haoxian Zhao
2010	J	`jnl`	Context-aware counter abstraction. Formal Methods Syst. Des. Gérard Basler, Michele Mazzucchi, Thomas Wahl, Daniel Kroening
2010	A*	`conf`	Coverage in interpolation-based model checking. DAC Hana Chockler, Daniel Kroening, Mitra Purandare
2010	A*	`conf`	Dynamic Cutoff Detection in Parameterized Concurrent Programs. CAV Alexander Kaiser, Daniel Kroening, Thomas Wahl
2010	B	`conf`	Interpolant Strength. VMCAI Vijay Victor D'Silva, Daniel Kroening, Mitra Purandare, Georg Weissenbacher
2010	—	`conf`	Interpolating Quantifier-Free Presburger Arithmetic. LPAR (Yogyakarta) Daniel Kroening, Jérôme Leroux, Philipp Rümmer
2010	—	`conf`	Loopfrog - loop summarization for static analysis. WING@ETAPS/IJCAR Daniel Kroening, Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich, Christoph M. Wintersteiger
2010	J	`jnl`	Periodic orbits and equilibria in glass models for gene regulatory networks. IEEE Trans. Inf. Theory Igor Zinovik, Yury Chebiryak, Daniel Kroening
2010	—	`conf`	Program Verification via Craig Interpolation for Presburger Arithmetic with Arrays. VERIFY@IJCAR Angelo Brillout, Daniel Kroening, Philipp Rümmer, Thomas Wahl
2010	J	`jnl`	Race analysis for systemc using model checking. ACM Trans. Design Autom. Electr. Syst. Nicolas Blanc, Daniel Kroening
2010	A	`conf`	Ranking Function Synthesis for Bit-Vector Relations. TACAS Byron Cook, Daniel Kroening, Philipp Rümmer, Christoph M. Wintersteiger
2010	A*	`conf`	Termination Analysis with Compositional Transition Invariants. CAV Daniel Kroening, Natasha Sharygina, Aliaksei Tsitovich, Christoph M. Wintersteiger
2010	—	`conf`	Tightening Test Coverage Metrics: A Case Study in Equivalence Checking Using k-Induction. FMCO Alastair F. Donaldson, Nannan He, Daniel Kroening, Philipp Rümmer
2010	J	`jnl`	Verification and falsification of programs with loops using predicate abstraction. Formal Aspects Comput. Daniel Kroening, Georg Weissenbacher
2010	J	`jnl`	Verified software: theories, tools and experiments. Int. J. Softw. Tools Technol. Transf. Daniel Kroening, Tiziana Margaria
2009	J	`jnl`	A framework for Satisfiability Modulo Theories. Formal Aspects Comput. Daniel Kroening, Ofer Strichman
2009	—	`conf`	An Interpolating Decision Procedure for Transitive Relations with Uninterpreted Functions. Haifa Verification Conference Daniel Kroening, Georg Weissenbacher
2009	J	`jnl`	An abstraction-based decision procedure for bit-vector arithmetic. Int. J. Softw. Tools Technol. Transf. Randal E. Bryant, Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, Ofer Strichman, Bryan A. Brady
2009	A	`conf`	Finding Lean Induced Cycles in Binary Hypercubes. SAT Yury Chebiryak, Thomas Wahl, Daniel Kroening, Leopold Haller
2009	A	`conf`	Fixed points for multi-cycle path detection. DATE Vijay Victor D'Silva, Daniel Kroening
2009	A*	`conf`	Loopfrog: A Static Analyzer for ANSI-C Programs. ASE Daniel Kroening, Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich, Christoph M. Wintersteiger
2009	B	`conf`	Mixed abstractions for floating-point arithmetic. FMCAD Angelo Brillout, Daniel Kroening, Thomas Wahl
2009	—	`conf`	Mutation-Based Test Case Generation for Simulink Models. FMCO Angelo Brillout, Nannan He, Michele Mazzucchi, Daniel Kroening, Mitra Purandare, Philipp Rümmer, Georg Weissenbacher
2009	—	`ch.`	Software Verification. Handbook of Satisfiability Daniel Kroening
2009	—	`conf`	Speeding Up Simulation of SystemC Using Model Checking. SBMF Nicolas Blanc, Daniel Kroening
2009	A	`conf`	Strengthening properties using abstraction refinement. DATE Mitra Purandare, Thomas Wahl, Daniel Kroening
2009	A*	`conf`	Symbolic Counter Abstraction for Concurrent Software. CAV Gérard Basler, Michele Mazzucchi, Thomas Wahl, Daniel Kroening
2008	J	`jnl`	A Survey of Automated Techniques for Formal Software Verification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Vijay Victor D'Silva, Daniel Kroening, Georg Weissenbacher
2008	B	`conf`	Approximation Refinement for Interpolation-Based Model Checking. VMCAI Vijay Victor D'Silva, Mitra Purandare, Daniel Kroening
2008	J	`jnl`	Computing Binary Combinatorial Gray Codes Via Exhaustive Search With SAT Solvers. IEEE Trans. Inf. Theory Igor Zinovik, Daniel Kroening, Yury Chebiryak
2008	J	`jnl`	Craig Interpolation for Quantifier-Free Presburger Arithmetic CoRR Angelo Brillout, Daniel Kroening, Thomas Wahl
2008	—	`book`	Decision Procedures - An Algorithmic Point of View Daniel Kroening, Ofer Strichman
2008	A	`conf`	Embedded software verification: challenges and solutions. ICCAD Chao Wang, Malay K. Ganai, Shuvendu K. Lahiri, Daniel Kroening
2008	B	`conf`	Loop Summarization Using Abstract Transformers. ATVA Daniel Kroening, Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich, Christoph M. Wintersteiger
2008	A	`conf`	Race analysis for SystemC using model checking. ICCAD Nicolas Blanc, Daniel Kroening
2008	A	`conf`	Scoot: A Tool for the Analysis of SystemC Models. TACAS Nicolas Blanc, Daniel Kroening, Natasha Sharygina
2008	J	`jnl`	Towards a Classification of Hamiltonian Cycles in the 6-Cube. J. Satisf. Boolean Model. Comput. Yury Chebiryak, Daniel Kroening
2008	J	`jnl`	Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund M. Clarke
2007	—	`conf`	A Complete Bounded Model Checking Algorithm for Pushdown Systems. Haifa Verification Conference Gérard Basler, Daniel Kroening, Georg Weissenbacher
2007	—	`conf`	An Algebraic Algorithm for the Identification of Glass Networks with Periodic Orbits Along Cyclic Attractors. AB Igor Zinovik, Daniel Kroening, Yury Chebiryak
2007	A	`conf`	Deciding Bit-Vector Arithmetic with Abstraction. TACAS Randal E. Bryant, Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, Ofer Strichman, Bryan A. Brady
2007	A	`conf`	Formal verification at higher levels of abstraction. ICCAD Daniel Kroening, Sanjit A. Seshia
2007	A	`conf`	Interactive presentation: Image computation and predicate refinement for RTL verilog using word level proofs. DATE Daniel Kroening, Natasha Sharygina
2007	B	`conf`	Lifting Propositional Interpolants to the Word-Level. FMCAD Daniel Kroening, Georg Weissenbacher
2007	A*	`conf`	Model checking concurrent linux device drivers. ASE Thomas Witkowski, Nicolas Blanc, Daniel Kroening, Georg Weissenbacher
2007	—	`conf`	SAT-Based Summarization for Boolean Programs. SPIN Gérard Basler, Daniel Kroening, Georg Weissenbacher
2007	A	`conf`	VCEGAR: Verilog CounterExample Guided Abstraction Refinement. TACAS Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund M. Clarke
2007	J	`jnl`	Verification of Boolean programs with unbounded thread creation. Theor. Comput. Sci. Byron Cook, Daniel Kroening, Natasha Sharygina
2007	J	`jnl`	Verification of SpecC using predicate abstraction. Formal Methods Syst. Des. Edmund M. Clarke, Himanshu Jain, Daniel Kroening
2007	A*	`conf`	Verifying C++ with STL containers via predicate abstraction. ASE Nicolas Blanc, Alex Groce, Daniel Kroening
2006	A	`conf`	Approximating Predicate Images for Bit-Vector Logic. TACAS Daniel Kroening, Natasha Sharygina
2006	A*	`conf`	Counterexamples with Loops for Predicate Abstraction. CAV Daniel Kroening, Georg Weissenbacher
2006	J	`jnl`	Error explanation with distance metrics. Int. J. Softw. Tools Technol. Transf. Alex Groce, Sagar Chaki, Daniel Kroening, Ofer Strichman
2006	—	`conf`	ExpliSAT: Guiding SAT-Based Software Verification with Explicit States. Haifa Verification Conference Sharon Barner, Cindy Eisner, Ziv Glazberg, Daniel Kroening, Ishai Rabinovitz
2006	B	`conf`	Over-Approximating Boolean Programs with Unbounded Thread Creation. FMCAD Byron Cook, Daniel Kroening, Natasha Sharygina
2005	A*	`conf`	Cogent: Accurate Theorem Proving for Program Verification. CAV Byron Cook, Daniel Kroening, Natasha Sharygina
2005	J	`jnl`	Computational challenges in bounded model checking. Int. J. Softw. Tools Technol. Transf. Edmund M. Clarke, Daniel Kroening, Joël Ouaknine, Ofer Strichman
2005	—	`conf`	Computing Over-Approximations with Bounded Model Checking. BMC@CAV Daniel Kroening
2005	—	`conf`	Decision Procedures for the Grand Challenge. VSTTE Daniel Kroening
2005	C	`conf`	Formal verification of SystemC by automatic hardware/software partitioning. MEMOCODE Daniel Kroening, Natasha Sharygina
2005	A	`conf`	SATABS: SAT-Based Predicate Abstraction for ANSI-C. TACAS Edmund M. Clarke, Daniel Kroening, Natasha Sharygina, Karen Yorav
2005	—	`conf`	Symbolic Model Checking for Asynchronous Boolean Programs. SPIN Byron Cook, Daniel Kroening, Natasha Sharygina
2005	A*	`conf`	Word level predicate abstraction and refinement for verifying RTL verilog. DAC Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund M. Clarke
2004	A*	`conf`	A SAT-based algorithm for reparameterization in symbolic simulation. DAC Pankaj Chauhan, Edmund M. Clarke, Daniel Kroening
2004	A	`conf`	A Tool for Checking ANSI-C Programs. TACAS Edmund M. Clarke, Daniel Kroening, Flavio Lerda
2004	A*	`conf`	Abstraction-Based Satisfiability Solving of Presburger Arithmetic. CAV Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, Ofer Strichman
2004	C	`conf`	Accurate Theorem Proving for Program Verification. ISoLA Byron Cook, Daniel Kroening, Natasha Sharygina
2004	A	`conf`	Checking consistency of C and Verilog using predicate abstraction and induction. ICCAD Daniel Kroening, Edmund M. Clarke
2004	B	`conf`	Completeness and Complexity of Bounded Model Checking. VMCAI Edmund M. Clarke, Daniel Kroening, Joël Ouaknine, Ofer Strichman
2004	C	`conf`	Counterexample Guided Abstraction Refinement Via Program Execution. ICFEM Daniel Kroening, Alex Groce, Edmund M. Clarke
2004	A	`conf`	Fault Tolerance Tradeoffs in Moving from Decentralized to Centralized Embedded Systems. DSN Jennifer Morris, Daniel Kroening, Philip Koopman
2004	—	`conf`	Making the Most of BMC Counterexamples. BMC@CAV Alex Groce, Daniel Kroening
2004	J	`jnl`	Predicate Abstraction of ANSI-C Programs Using SAT. Formal Methods Syst. Des. Edmund M. Clarke, Daniel Kroening, Natasha Sharygina, Karen Yorav
2004	C	`conf`	Tutorial: Software Model Checking. ICFEM Edmund M. Clarke, Daniel Kroening
2004	A*	`conf`	Understanding Counterexamples with explain. CAV Alex Groce, Daniel Kroening, Flavio Lerda
2004	C	`conf`	Verification of SpecC using predicate abstraction. MEMOCODE Himanshu Jain, Daniel Kroening, Edmund M. Clarke
2003	A*	`conf`	Behavioral consistency of C and verilog programs using bounded model checking. DAC Edmund M. Clarke, Daniel Kroening, Karen Yorav
2003	B	`conf`	Efficient Computation of Recurrence Diameters. VMCAI Daniel Kroening, Ofer Strichman
2003	—	`conf`	Hardware verification using ANSI-C programs as a reference. ASP-DAC Edmund M. Clarke, Daniel Kroening
2003	—	`conf`	Instantiating Uninterpreted Functional Units and Memory System: Functional Verification of the VAMP. CHARME Sven Beyer, Christian Jacobi, Daniel Kroening, Dirk Leinenbach, Wolfgang J. Paul
2003	C	`conf`	Specifying and Verifying Systems with Multiple Clocks. ICCD Edmund M. Clarke, Daniel Kroening, Karen Yorav
2001	A*	`conf`	Automated Pipeline Design. DAC Daniel Kroening, Wolfgang J. Paul
2000	—	`conf`	Proving the Correctness of a Complete Microprocessor. GI Jahrestagung Christian Jacobi, Daniel Kroening
1999	—	`conf`	The Impact of Hardware Scheduling Mechanismus on the Performance and Cost of Processor Designs. ARCS Silvia M. Müller, Holger W. Leister, Peter Dell, Nikolaus Gerteis, Daniel Kroening