Daniel Kroening

Orcid: 0000-0002-6681-5283

Affiliations:
  • Amazon, USA


According to our database1, Daniel Kroening authored at least 289 papers between 1999 and 2024.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
Symbolic Task Inference in Deep Reinforcement Learning.
J. Artif. Intell. Res., 2024

Neural Model Checking.
CoRR, 2024

Towards Translating Real-World Code with LLMs: A Study of Translating to Rust.
CoRR, 2024

VERT: Verified Equivalent Rust Transpilation with Few-Shot Learning.
CoRR, 2024

Safeguarded Progress in Reinforcement Learning: Safe Bayesian Exploration for Control Policy Synthesis.
Proceedings of the Thirty-Eighth AAAI Conference on Artificial Intelligence, 2024

2023
Certified reinforcement learning with logic guidance.
Artif. Intell., September, 2023

Synthesising Programs with Non-trivial Constants.
J. Autom. Reason., June, 2023

You Only Explain Once.
CoRR, 2023

Multiple Different Explanations for Image Classifiers.
CoRR, 2023

CBMC: The C Bounded Model Checker.
CoRR, 2023

JBMC: A Bounded Model Checking Tool for Java Bytecode.
CoRR, 2023

2LS for Program Analysis.
CoRR, 2023

2022
Enhancing active model learning with equivalence checking using simulation relations.
Formal Methods Syst. Des., December, 2022

LCRL: Certified Policy Synthesis via Logically-Constrained Reinforcement Learning.
CoRR, 2022

Neural termination analysis.
Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2022

LCRL: Certified Policy Synthesis via Logically-Constrained Reinforcement Learning.
Proceedings of the Quantitative Evaluation of Systems - 19th International Conference, 2022

Active Learning of Abstract System Models from Traces using Model Checking.
Proceedings of the 2022 Design, Automation & Test in Europe Conference & Exhibition, 2022

2021
Software Verification.
Proceedings of the Handbook of Satisfiability - Second Edition, 2021

Unbounded-Time Safety Verification of Guarded LTI Models with Inputs by Abstract Acceleration.
J. Autom. Reason., 2021

Model checking boot code from AWS data centers.
Formal Methods Syst. Des., 2021

Active Learning of Abstract System Models from Traces using Model Checking [Extended].
CoRR, 2021

Compositional Explanations for Image Classifiers.
CoRR, 2021

Ranking Policy Decisions.
Proceedings of the Advances in Neural Information Processing Systems 34: Annual Conference on Neural Information Processing Systems 2021, 2021

Exposing previously undetectable faults in deep neural networks.
Proceedings of the ISSTA '21: 30th ACM SIGSOFT International Symposium on Software Testing and Analysis, 2021

Explanations for Occluded Images.
Proceedings of the 2021 IEEE/CVF International Conference on Computer Vision, 2021

Shielding Atari Games with Bounded Prescience.
Proceedings of the AAMAS '21: 20th International Conference on Autonomous Agents and Multiagent Systems, 2021

DeepSynth: Automata Synthesis for Automatic Task Segmentation in Deep Reinforcement Learning.
Proceedings of the Thirty-Fifth AAAI Conference on Artificial Intelligence, 2021

2020
Learning the Language of Software Errors.
J. Artif. Intell. Res., 2020

A survey of safety and trustworthiness of deep neural networks: Verification, testing, adversarial attack and defence, and interpretability.
Comput. Sci. Rev., 2020

Semantic Adversarial Perturbations using Learnt Representations.
CoRR, 2020

CounterExample Guided Neural Synthesis.
CoRR, 2020

Hardware/Software Co-verification Using Path-based Symbolic Execution.
CoRR, 2020

Automated formal synthesis of provably safe digital controllers for continuous plants.
Acta Informatica, 2020

Deep Reinforcement Learning with Temporal Logics.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2020

Using model checking tools to triage the severity of security bugs in the Xen hypervisor.
Proceedings of the 2020 Formal Methods in Computer Aided Design, 2020

Explaining Image Classifiers Using Statistical Fault Localization.
Proceedings of the Computer Vision - ECCV 2020, 2020

Learning Concise Models from Long Execution Traces.
Proceedings of the 57th ACM/IEEE Design Automation Conference, 2020

The Taint Rabbit: Optimizing Generic Taint Analysis with Dynamic Fast Path Generation.
Proceedings of the ASIA CCS '20: The 15th ACM Asia Conference on Computer and Communications Security, 2020

Cautious Reinforcement Learning with Logical Constraints.
Proceedings of the 19th International Conference on Autonomous Agents and Multiagent Systems, 2020

2019
Structural Test Coverage Criteria for Deep Neural Networks.
ACM Trans. Embed. Comput. Syst., 2019

DeepSynth: Program Synthesis for Automatic Task Segmentation in Deep Reinforcement Learning.
CoRR, 2019

Modular Deep Reinforcement Learning with Temporal Logic Specifications.
CoRR, 2019

Explaining Deep Neural Networks Using Spectrum-Based Fault Localization.
CoRR, 2019

CREST: Hardware Formal Verification with ANSI-C Reference Specifications.
CoRR, 2019

Generating Realistic Unrestricted Adversarial Inputs using Dual-Objective GAN Training.
CoRR, 2019

Certified Reinforcement Learning with Logic Guidance.
CoRR, 2019

JBMC: Bounded Model Checking for Java Bytecode - (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2019

Global Robustness Evaluation of Deep Neural Networks with Provable Guarantees for the Hamming Distance.
Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, 2019

DeepConcolic: testing and debugging deep neural networks.
Proceedings of the 41st International Conference on Software Engineering: Companion Proceedings, 2019

Reinforcement Learning for Temporal Logic Control Synthesis with Probabilistic Satisfaction Guarantees.
Proceedings of the 58th IEEE Conference on Decision and Control, 2019

Gollum: Modular and Greybox Exploit Generation for Heap Overflows in Interpreters.
Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, 2019

Logically-Constrained Neural Fitted Q-iteration.
Proceedings of the 18th International Conference on Autonomous Agents and MultiAgent Systems, 2019

Towards Verifiable and Safe Model-Free Reinforcement Learning.
Proceedings of the 1st Workshop on Artificial Intelligence and Formal Verification, 2019

2018
SAT-Based Model Checking.
Proceedings of the Handbook of Model Checking., 2018

Program Synthesis for Program Analysis.
ACM Trans. Program. Lang. Syst., 2018

Bit-Precise Procedure-Modular Termination Analysis.
ACM Trans. Program. Lang. Syst., 2018

Effective Verification for Low-Level Software with Competing Interrupts.
ACM Trans. Embed. Comput. Syst., 2018

Benchmarking of Java Verification Tools at the Software Verification Competition (SV-COMP).
ACM SIGSOFT Softw. Eng. Notes, 2018

Evaluating Manual Intervention to Address the Challenges of Bug Finding with KLEE.
CoRR, 2018

Global Robustness Evaluation of Deep Neural Networks with Provable Guarantees for L0 Norm.
CoRR, 2018

Testing Deep Neural Networks.
CoRR, 2018

Logically-Correct Reinforcement Learning.
CoRR, 2018

Automatic Heap Layout Manipulation for Exploitation.
Proceedings of the 27th USENIX Security Symposium, 2018

Concolic testing for deep neural networks.
Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, 2018

DSValidator: An Automated Counterexample Reproducibility Tool for Digital Systems.
Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week), 2018

Optimising Spectrum Based Fault Localisation for Single Fault Programs Using Specifications.
Proceedings of the Fundamental Approaches to Software Engineering, 2018

Verification of tree-based hierarchical read-copy update in the Linux kernel.
Proceedings of the 2018 Design, Automation & Test in Europe Conference & Exhibition, 2018

Efficient verification of multi-property designs (The benefit of wrong assumptions).
Proceedings of the 2018 Design, Automation & Test in Europe Conference & Exhibition, 2018

JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode.
Proceedings of the Computer Aided Verification - 30th International Conference, 2018

Counterexample Guided Inductive Synthesis Modulo Theories.
Proceedings of the Computer Aided Verification - 30th International Conference, 2018

Model checking, 2nd Edition.
MIT Press, ISBN: 978-0-262-03883-6, 2018

2017
Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs.
ACM Trans. Program. Lang. Syst., 2017

Don't Sit on the Fence: A Static Analysis Approach to Automatic Fence Insertion.
ACM Trans. Program. Lang. Syst., 2017

Lost in abstraction: Monotonicity in multi-threaded programs.
Inf. Comput., 2017

Incremental bounded model checking for embedded software.
Formal Aspects Comput., 2017

Kayak: Safe Semantic Refactoring to Java Streams.
CoRR, 2017

Efficient Verification of Multi-Property Designs (The Benefit of Wrong Assumptions) (Extended Version).
CoRR, 2017

Independence Abstractions and Models of Concurrency.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2017

Modular Demand-Driven Analysis of Semantic Difference for Program Versions.
Proceedings of the Static Analysis - 24th International Symposium, 2017

DSSynth: an automated digital controller synthesis tool for physical plants.
Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering, 2017

Verifying digital systems with MATLAB.
Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis, Santa Barbara, CA, USA, July 10, 2017

Functional Requirements-Based Automated Testing for Avionics.
Proceedings of the 22nd International Conference on Engineering of Complex Computer Systems, 2017

Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants.
Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control, 2017

Formal Techniques for Effective Co-verification of Hardware/Software Co-designs.
Proceedings of the 54th Annual Design Automation Conference, 2017

Abstract Interpretation with Unfoldings.
Proceedings of the Computer Aided Verification - 29th International Conference, 2017

Sound Numerical Computations in Abstract Acceleration.
Proceedings of the Numerical Software Verification - 10th International Workshop, 2017

Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants.
Proceedings of the Computer Aided Verification - 29th International Conference, 2017


Lifting CDCL to Template-Based Abstract Domains for Program Verification.
Proceedings of the Automated Technology for Verification and Analysis, 2017

2016
Decision Procedures - An Algorithmic Point of View, Second Edition
Texts in Theoretical Computer Science. An EATCS Series, Springer, ISBN: 978-3-662-50497-0, 2016

Verification of Concurrent Software.
Proceedings of the Dependable Software Systems Engineering, 2016

Generating test case chains for reactive systems.
Int. J. Softw. Tools Technol. Transf., 2016

Preface: Special Issue on Interpolation.
J. Autom. Reason., 2016

The Virtues of Conflict: Analyzing Modern Concurrency.
CoRR, 2016

Equivalence Checking a Floating-point Unit against a High-level C Model (Extended Version).
CoRR, 2016

Sound Static Deadlock Analysis for C/Pthreads (Extended Version).
CoRR, 2016

Satisfiability Checking meets Symbolic Computation (Project Paper).
CoRR, 2016

Satisfiability checking and symbolic computation.
ACM Commun. Comput. Algebra, 2016

Automatic Generation of Propagation Complete SAT Encodings.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2016

2LS for Program Analysis - (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2016

Formalizing and Checking Thread Refinement for Data-Race-Free Execution Models.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2016

v2c - A Verilog to C Translator.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2016

Algebraic Techniques in Software Verification : Challenges and Opportunities.
Proceedings of the 1st Workshop on Satisfiability Checking and Symbolic Computation co-located with 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2016), 2016

The virtues of conflict: analysing modern concurrency.
Proceedings of the 21st ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 2016

Assisted Coverage Closure.
Proceedings of the NASA Formal Methods - 8th International Symposium, 2016

SC<sup>2</sup>: Satisfiability Checking Meets Symbolic Computation - (Project Paper).
Proceedings of the Intelligent Computer Mathematics - 9th International Conference, 2016

Static Program Analysis for Identifying Energy Bugs in Graphics-Intensive Mobile Apps.
Proceedings of the 24th IEEE International Symposium on Modeling, 2016

Sound static deadlock analysis for C/Pthreads.
Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, 2016

Towards Automated Bounded Model Checking of API Implementations.
Proceedings of the 7th Workshop on Constraint Solvers in Testing, 2016

Probabilistic Fault Localisation.
Proceedings of the Hardware and Software: Verification and Testing, 2016

Equivalence Checking of a Floating-Point Unit Against a High-Level C Model.
Proceedings of the FM 2016: Formal Methods, 2016

Danger Invariants.
Proceedings of the FM 2016: Formal Methods, 2016

Unbounded safety verification for hardware using software analyzers.
Proceedings of the 2016 Design, Automation & Test in Europe Conference & Exhibition, 2016

2015
Under-approximating loops in C programs for fast counterexample detection.
Formal Methods Syst. Des., 2015

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

Danger Invariants.
CoRR, 2015

Synthesising Interprocedural Bit-Precise Termination Proofs (extended version).
CoRR, 2015

Unbounded-Time Analysis of Guarded LTI Systems with Inputs by Abstract Acceleration (extended version).
CoRR, 2015

Safety Verification and Refutation by k-invariants and k-induction (extended version).
CoRR, 2015

From AgentSpeak to C for Safety Considerations in Unmanned Aerial Vehicles.
Proceedings of the Towards Autonomous Robotic Systems - 16th Annual Conference, 2015

Unbounded-Time Analysis of Guarded LTI Systems with Inputs by Abstract Acceleration.
Proceedings of the Static Analysis - 22nd International Symposium, 2015

Safety Verification and Refutation by k-Invariants and k-Induction.
Proceedings of the Static Analysis - 22nd International Symposium, 2015

Using Program Synthesis for Program Analysis.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2015

Synthesising Interprocedural Bit-Precise Termination Proofs (T).
Proceedings of the 30th IEEE/ACM International Conference on Automated Software Engineering, 2015

Equivalence Checking Using Trace Partitioning.
Proceedings of the 2015 IEEE Computer Society Annual Symposium on VLSI, 2015

Hardware Verification Using Software Analyzers.
Proceedings of the 2015 IEEE Computer Society Annual Symposium on VLSI, 2015

Faster Linearizability Checking via P-Compositionality.
Proceedings of the Formal Techniques for Distributed Objects, Components, and Systems, 2015

On Partial Order Semantics for SAT/SMT-Based Symbolic Encodings of Weak Memory Concurrency.
Proceedings of the Formal Techniques for Distributed Objects, Components, and Systems, 2015

Successful Use of Incremental BMC in the Automotive Industry.
Proceedings of the Formal Methods for Industrial Critical Systems, 2015

Accelerating Invariant Generation.
Proceedings of the Formal Methods in Computer-Aided Design, 2015

Proving Safety with Trace Automata and Bounded Model Checking.
Proceedings of the FM 2015: Formal Methods, 2015

Property-Driven Fence Insertion Using Reorder Bounded Model Checking.
Proceedings of the FM 2015: Formal Methods, 2015

Evaluation of Measures for Statistical Fault Localisation and an Optimising Scheme.
Proceedings of the Fundamental Approaches to Software Engineering, 2015

Propositional Reasoning about Safety and Termination of Heap-Manipulating Programs.
Proceedings of the Programming Languages and Systems, 2015

Unrestricted Termination and Non-termination Arguments for Bit-Vector Programs.
Proceedings of the Programming Languages and Systems, 2015

Verifying synchronous reactive systems using lazy abstraction.
Proceedings of the 2015 Design, Automation & Test in Europe Conference & Exhibition, 2015

Effective verification of low-level software with nested interrupts.
Proceedings of the 2015 Design, Automation & Test in Europe Conference & Exhibition, 2015

Unfolding-based Partial Order Reduction.
Proceedings of the 26th International Conference on Concurrency Theory, 2015

Learning the Language of Error.
Proceedings of the Automated Technology for Verification and Analysis, 2015

Measuring Change Impact on Program Behaviour.
Proceedings of the Validation of Evolving Software, 2015

Complementarities Among the Technologies Presented in the Book.
Proceedings of the Validation of Evolving Software, 2015

Challenges of Existing Technology.
Proceedings of the Validation of Evolving Software, 2015

Introduction.
Proceedings of the Validation of Evolving Software, 2015

2014
A Widening Approach to Multithreaded Program Verification.
ACM Trans. Program. Lang. Syst., 2014

Deciding floating-point logic with abstract conflict driven clause learning.
Formal Methods Syst. Des., 2014

Decision Procedures and Abstract Interpretation (Dagstuhl Seminar 14351).
Dagstuhl Reports, 2014

Next Generation Static Software Analysis Tools (Dagstuhl Seminar 14352).
Dagstuhl Reports, 2014

Incremental Bounded Model Checking for Embedded Software (extended version).
CoRR, 2014

AbPress: Flexing Partial-Order Reduction and Abstraction.
CoRR, 2014

Second-Order SAT Solving using Program Synthesis.
CoRR, 2014

Lost in Abstraction: Monotonicity in Multi-Threaded Programs (Extended Technical Report).
CoRR, 2014

CBMC - C Bounded Model Checker - (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2014

Abstract satisfaction.
Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

Camera-laser projector stereo system based anti-collision system for robotic wheelchair users with cognitive impairment.
Proceedings of the International Conference on Multisensor Fusion and Information Integration for Intelligent Systems, 2014

Automating Software Analysis at Large Scale.
Proceedings of the Mathematical and Engineering Methods in Computer Science, 2014

Accelerated test execution using GPUs.
Proceedings of the ACM/IEEE International Conference on Automated Software Engineering, 2014

Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs.
Proceedings of the FM 2014: Formal Methods, 2014

Model and Proof Generation for Heap-Manipulating Programs.
Proceedings of the Programming Languages and Systems, 2014

2013
Preface to the special issue "SI: Satisfiability Modulo Theories".
Formal Methods Syst. Des., 2013

Loop summarization using state and transition invariants.
Formal Methods Syst. Des., 2013

Ranking function synthesis for bit-vector relations.
Formal Methods Syst. Des., 2013

Partial Orders for Efficient BMC of Concurrent Software
CoRR, 2013

Chaining Test Cases for Reactive System Testing (extended version).
CoRR, 2013

Abstraction of Syntax.
Proceedings of the Verification, 2013

An Abstract Interpretation of DPLL(T).
Proceedings of the Verification, 2013

Interpolation-Based Verification of Floating-Point Programs with Abstract CDCL.
Proceedings of the Static Analysis - 20th International Symposium, 2013

Automated Verification of Concurrent Software.
Proceedings of the Reachability Problems - 7th International Workshop, 2013

Chaining Test Cases for Reactive System Testing.
Proceedings of the Testing Software and Systems, 2013

Abstract conflict driven learning.
Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2013

A visual studio plug-in for CProver.
Proceedings of the 3rd International Workshop on Developing Tools as Plug-ins, 2013

Verifying multi-threaded software with impact.
Proceedings of the Formal Methods in Computer-Aided Design, 2013

Formal co-validation of low-level hardware/software interfaces.
Proceedings of the Formal Methods in Computer-Aided Design, 2013

Counterexample-Guided Precondition Inference.
Proceedings of the Programming Languages and Systems, 2013

Software Verification for Weak Memory via Program Transformation.
Proceedings of the Programming Languages and Systems, 2013

Partial Orders for Efficient Bounded Model Checking of Concurrent Software.
Proceedings of the Computer Aided Verification - 25th International Conference, 2013

2012
Computing Mutation Coverage in Interpolation-Based Model Checking.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2012

Counterexample-guided abstraction refinement for symmetric concurrent programs.
Formal Methods Syst. Des., 2012

Wolverine: Battling Bugs with Interpolants - (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2012

Proving Reachability Using FShell - (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2012

Numeric Bounds Analysis with Conflict-Driven Learning.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2012

satabs: A Bit-Precise Verifier for C Programs - (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2012

Satisfiability Solvers Are Static Analysers.
Proceedings of the Static Analysis - 19th International Symposium, 2012

Deciding floating-point logic with systematic abstraction.
Proceedings of the Formal Methods in Computer-Aided Design, 2012

Efficient Coverability Analysis by Proof Minimization.
Proceedings of the CONCUR 2012 - Concurrency Theory - 23rd International Conference, 2012

2011
An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic.
J. Autom. Reason., 2011

Automatic analysis of DMA races using model checking and <i>k</i>-induction.
Formal Methods Syst. Des., 2011

Editorial.
Formal Aspects Comput., 2011

Symmetry-Aware Predicate Abstraction for Shared-Variable Concurrent Programs (Extended Technical Report)
CoRR, 2011

Strengthening Induction-Based Race Checking with Lightweight Static Analysis.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2011

Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2011

Loop Summarization and Termination Analysis.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2011

Software Verification Using k-Induction.
Proceedings of the Static Analysis - 18th International Symposium, 2011

SCRATCH: a tool for automatic analysis of dma races.
Proceedings of the 16th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 2011

Test-case generation for embedded simulink via formal concept analysis.
Proceedings of the 48th Design Automation Conference, 2011

Interpolation-Based Software Verification with Wolverine.
Proceedings of the Computer Aided Verification - 23rd International Conference, 2011

Linear Completeness Thresholds for Bounded Model Checking.
Proceedings of the Computer Aided Verification - 23rd International Conference, 2011

Symmetry-Aware Predicate Abstraction for Shared-Variable Concurrent Programs.
Proceedings of the Computer Aided Verification - 23rd International Conference, 2011

Making Software Verification Tools Really Work.
Proceedings of the Automated Technology for Verification and Analysis, 2011

Soundness of Data Flow Analyses for Weak Memory Models.
Proceedings of the Programming Languages and Systems - 9th Asian Symposium, 2011

2010
Race analysis for systemc using model checking.
ACM Trans. Design Autom. Electr. Syst., 2010

Periodic orbits and equilibria in glass models for gene regulatory networks.
IEEE Trans. Inf. Theory, 2010

Verified software: theories, tools and experiments.
Int. J. Softw. Tools Technol. Transf., 2010

Context-aware counter abstraction.
Formal Methods Syst. Des., 2010

Verification and falsification of programs with loops using predicate abstraction.
Formal Aspects Comput., 2010

Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic (Extended Technical Report)
CoRR, 2010

Interpolant Strength.
Proceedings of the Verification, 2010

Automatic Analysis of Scratch-Pad Memory Code for Heterogeneous Multicore Processors.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2010

Boom: Taking Boolean Program Model Checking One Step Further.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2010

Interpolating Quantifier-Free Presburger Arithmetic.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2010

Tightening Test Coverage Metrics: A Case Study in Equivalence Checking Using k-Induction.
Proceedings of the Formal Methods for Components and Objects - 9th International Symposium, 2010

Coverage in interpolation-based model checking.
Proceedings of the 47th Design Automation Conference, 2010

Termination Analysis with Compositional Transition Invariants.
Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

Dynamic Cutoff Detection in Parameterized Concurrent Programs.
Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

Loopfrog - loop summarization for static analysis.
Proceedings of the Second International Workshop on Invariant Generation, 2010

Program Verification via Craig Interpolation for Presburger Arithmetic with Arrays.
Proceedings of the 6th International Verification Workshop, 2010

2009
Software Verification.
Proceedings of the Handbook of Satisfiability, 2009

An abstraction-based decision procedure for bit-vector arithmetic.
Int. J. Softw. Tools Technol. Transf., 2009

A framework for Satisfiability Modulo Theories.
Formal Aspects Comput., 2009

Speeding Up Simulation of SystemC Using Model Checking.
Proceedings of the Formal Methods: Foundations and Applications, 2009

Finding Lean Induced Cycles in Binary Hypercubes.
Proceedings of the Theory and Applications of Satisfiability Testing, 2009

Loopfrog: A Static Analyzer for ANSI-C Programs.
Proceedings of the ASE 2009, 2009

An Interpolating Decision Procedure for Transitive Relations with Uninterpreted Functions.
Proceedings of the Hardware and Software: Verification and Testing, 2009

Mutation-Based Test Case Generation for Simulink Models.
Proceedings of the Formal Methods for Components and Objects - 8th International Symposium, 2009

Mixed abstractions for floating-point arithmetic.
Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, 2009

Strengthening properties using abstraction refinement.
Proceedings of the Design, Automation and Test in Europe, 2009

Fixed points for multi-cycle path detection.
Proceedings of the Design, Automation and Test in Europe, 2009

Symbolic Counter Abstraction for Concurrent Software.
Proceedings of the Computer Aided Verification, 21st International Conference, 2009

2008
Decision Procedures - An Algorithmic Point of View
Texts in Theoretical Computer Science. An EATCS Series, Springer, ISBN: 978-3-540-74105-3, 2008

Computing Binary Combinatorial Gray Codes Via Exhaustive Search With SAT Solvers.
IEEE Trans. Inf. Theory, 2008

Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2008

A Survey of Automated Techniques for Formal Software Verification.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2008

Towards a Classification of Hamiltonian Cycles in the 6-Cube.
J. Satisf. Boolean Model. Comput., 2008

Craig Interpolation for Quantifier-Free Presburger Arithmetic
CoRR, 2008

Approximation Refinement for Interpolation-Based Model Checking.
Proceedings of the Verification, 2008

Scoot: A Tool for the Analysis of SystemC Models.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2008

Embedded software verification: challenges and solutions.
Proceedings of the 2008 International Conference on Computer-Aided Design, 2008

Loop Summarization Using Abstract Transformers.
Proceedings of the Automated Technology for Verification and Analysis, 2008

2007
Verification of Boolean programs with unbounded thread creation.
Theor. Comput. Sci., 2007

Verification of SpecC using predicate abstraction.
Formal Methods Syst. Des., 2007

VCEGAR: Verilog CounterExample Guided Abstraction Refinement.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

Deciding Bit-Vector Arithmetic with Abstraction.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

Model Checking with Abstraction for Web Services.
Proceedings of the Test and Analysis of Web Services, 2007

SAT-Based Summarization for Boolean Programs.
Proceedings of the Model Checking Software, 2007

A First Step Towards a Unified Proof Checker for QBF.
Proceedings of the Theory and Applications of Satisfiability Testing, 2007

Model checking concurrent linux device drivers.
Proceedings of the 22nd IEEE/ACM International Conference on Automated Software Engineering (ASE 2007), 2007

Verifying C++ with STL containers via predicate abstraction.
Proceedings of the 22nd IEEE/ACM International Conference on Automated Software Engineering (ASE 2007), 2007

Formal verification at higher levels of abstraction.
Proceedings of the 2007 International Conference on Computer-Aided Design, 2007

A Complete Bounded Model Checking Algorithm for Pushdown Systems.
Proceedings of the Hardware and Software: Verification and Testing, 2007

Lifting Propositional Interpolants to the Word-Level.
Proceedings of the Formal Methods in Computer-Aided Design, 7th International Conference, 2007

Interactive presentation: Image computation and predicate refinement for RTL verilog using word level proofs.
Proceedings of the 2007 Design, Automation and Test in Europe Conference and Exposition, 2007

An Algebraic Algorithm for the Identification of Glass Networks with Periodic Orbits Along Cyclic Attractors.
Proceedings of the Algebraic Biology, Second International Conference, 2007

2006
Error explanation with distance metrics.
Int. J. Softw. Tools Technol. Transf., 2006

Putting it all together - Formal verification of the VAMP.
Int. J. Softw. Tools Technol. Transf., 2006

Approximating Predicate Images for Bit-Vector Logic.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2006

ExpliSAT: Guiding SAT-Based Software Verification with Explicit States.
Proceedings of the Hardware and Software, 2006

Over-Approximating Boolean Programs with Unbounded Thread Creation.
Proceedings of the Formal Methods in Computer-Aided Design, 6th International Conference, 2006

Counterexamples with Loops for Predicate Abstraction.
Proceedings of the Computer Aided Verification, 18th International Conference, 2006

2005
Computational challenges in bounded model checking.
Int. J. Softw. Tools Technol. Transf., 2005

Computing Over-Approximations with Bounded Model Checking.
Proceedings of the Third International Workshop on Bounded Model Checking, 2005

Decision Procedures for the Grand Challenge.
Proceedings of the Verified Software: Theories, 2005

SATABS: SAT-Based Predicate Abstraction for ANSI-C.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2005

Symbolic Model Checking for Asynchronous Boolean Programs.
Proceedings of the Model Checking Software, 2005

Formal verification of SystemC by automatic hardware/software partitioning.
Proceedings of the 3rd ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2005), 2005

Word level predicate abstraction and refinement for verifying RTL verilog.
Proceedings of the 42nd Design Automation Conference, 2005

Cogent: Accurate Theorem Proving for Program Verification.
Proceedings of the Computer Aided Verification, 17th International Conference, 2005

2004
Predicate Abstraction of ANSI-C Programs Using SAT.
Formal Methods Syst. Des., 2004

Making the Most of BMC Counterexamples.
Proceedings of the 2nd International Workshop on Bounded Model Checking, 2004

Completeness and Complexity of Bounded Model Checking.
Proceedings of the Verification, 2004

A Tool for Checking ANSI-C Programs.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2004

Bounded Model Checking and Inductive Verification of Hybrid Discrete-continuous Systems.
Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2004

Accurate Theorem Proving for Program Verification.
Proceedings of the Leveraging Applications of Formal Methods, 2004

Counterexample Guided Abstraction Refinement Via Program Execution.
Proceedings of the Formal Methods and Software Engineering, 2004

Tutorial: Software Model Checking.
Proceedings of the Formal Methods and Software Engineering, 2004

Checking consistency of C and Verilog using predicate abstraction and induction.
Proceedings of the 2004 International Conference on Computer-Aided Design, 2004

Fault Tolerance Tradeoffs in Moving from Decentralized to Centralized Embedded Systems.
Proceedings of the 2004 International Conference on Dependable Systems and Networks (DSN 2004), 28 June, 2004

A SAT-based algorithm for reparameterization in symbolic simulation.
Proceedings of the 41th Design Automation Conference, 2004

Abstraction-Based Satisfiability Solving of Presburger Arithmetic.
Proceedings of the Computer Aided Verification, 16th International Conference, 2004

Understanding Counterexamples with explain.
Proceedings of the Computer Aided Verification, 16th International Conference, 2004

2003
Efficient Computation of Recurrence Diameters.
Proceedings of the Verification, 2003

Specifying and Verifying Systems with Multiple Clocks.
Proceedings of the 21st International Conference on Computer Design (ICCD 2003), 2003

Behavioral consistency of C and verilog programs using bounded model checking.
Proceedings of the 40th Design Automation Conference, 2003

Instantiating Uninterpreted Functional Units and Memory System: Functional Verification of the VAMP.
Proceedings of the Correct Hardware Design and Verification Methods, 2003

Hardware verification using ANSI-C programs as a reference.
Proceedings of the 2003 Asia and South Pacific Design Automation Conference, 2003

2001
Formal verification of pipelined microprocessors.
Proceedings of the Ausgezeichnete Informatikdissertationen 2001, 2001

Automated Pipeline Design.
Proceedings of the 38th Design Automation Conference, 2001

Formal verification of pipelined microprocessors.
PhD thesis, 2001

2000
Proving the Correctness of Pipelined Micro-Architectures.
Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), Frankfurt, Germany, February 28, 2000

Proving the Correctness of a Complete Microprocessor.
Proceedings of the Informatik 2000, 2000

1999
The Impact of Hardware Scheduling Mechanismus on the Performance and Cost of Processor Designs.
Proceedings of the Architektur von Rechensystemen, Systemarchitektur auf dem Weg ins 3. Jahrtausend: Neue Strukturen, Konzepte, Verfahren und Bewertungsmethoden, 1999


  Loading...