Daniel Kroening

According to our database1, Daniel Kroening authored at least 265 papers between 1999 and 2018.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Homepages:

On csauthors.net:

Bibliography

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. Embedded Comput. Syst., 2018

Logically-Constrained Neural Fitted Q-Iteration.
CoRR, 2018

Benchmarking of Java Verification Tools at the Software Verification Competition (SV-COMP).
CoRR, 2018

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

Concolic Testing for Deep Neural Networks.
CoRR, 2018

Automatic Heap Layout Manipulation for Exploitation.
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

Model Checking Boot Code from AWS Data Centers.
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

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 Asp. 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

Functional Requirements-Based Automated Testing for Avionics.
CoRR, 2017

Abstract Interpretation with Unfoldings.
CoRR, 2017

Lifting CDCL to Template-based Abstract Domains for Program Verification.
CoRR, 2017

Verifying Digital Systems with MATLAB.
CoRR, 2017

Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants.
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

SC-square: when Satisfiability Checking and Symbolic Computation join forces.
Proceedings of the ARCADE 2017, 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.
STTT, 2016

Preface: Special Issue on Interpolation.
J. Autom. Reasoning, 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

Verification of the Tree-Based Hierarchical Read-Copy Update in the Linux Kernel.
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.
CoRR, 2016

Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants.
CoRR, 2016

Satisfiability checking and symbolic computation.
ACM Comm. Computer 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

SC2: 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 in System Design, 2015

Unfolding-based Partial Order Reduction.
CoRR, 2015

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

Assisted Coverage Closure.
CoRR, 2015

Faster linearizability checking via $P$-compositionality.
CoRR, 2015

On partial order semantics for SAT/SMT-based symbolic encodings of weak memory concurrency.
CoRR, 2015

Using Program Synthesis for Program Analysis.
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 in System Design, 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

Proving Safety with Trace Automata and Bounded Model Checking.
CoRR, 2014

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

Property-Driven Fence Insertion using Reorder Bounded Model Checking.
CoRR, 2014

Unrestricted Termination and Non-Termination Arguments for Bit-Vector Programs.
CoRR, 2014

Propositional Reasoning about Safety and Termination of Heap-Manipulating Programs.
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

Lost in Abstraction: Monotonicity in Multi-threaded Programs.
Proceedings of the CONCUR 2014 - Concurrency Theory - 25th International Conference, 2014

Don't Sit on the Fence - A Static Analysis Approach to Automatic Fence Insertion.
Proceedings of the Computer Aided Verification - 26th International Conference, 2014

2013
Preface to the special issue "SI: Satisfiability Modulo Theories".
Formal Methods in System Design, 2013

Loop summarization using state and transition invariants.
Formal Methods in System Design, 2013

Ranking function synthesis for bit-vector relations.
Formal Methods in System Design, 2013

Partial Orders for Efficient BMC of Concurrent Software
CoRR, 2013

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

Don't sit on the fence: A static analysis approach to automatic fence insertion.
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

Under-Approximating Loops in C Programs for Fast Counterexample Detection.
Proceedings of the Computer Aided Verification - 25th International Conference, 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. on CAD of Integrated Circuits and Systems, 2012

Counterexample-guided abstraction refinement for symmetric concurrent programs.
Formal Methods in System Design, 2012

Software Verification for Weak Memory via Program Transformation
CoRR, 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. Reasoning, 2011

Automatic analysis of DMA races using model checking and k-induction.
Formal Methods in System Design, 2011

Editorial.
Formal Asp. 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. Information Theory, 2010

Verified software: theories, tools and experiments.
STTT, 2010

Context-aware counter abstraction.
Formal Methods in System Design, 2010

Verification and falsification of programs with loops using predicate abstraction.
Formal Asp. 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

Ranking Function Synthesis for Bit-Vector Relations.
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

An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic.
Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010

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

An abstraction-based decision procedure for bit-vector arithmetic.
STTT, 2009

A framework for Satisfiability Modulo Theories.
Formal Asp. 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. Information Theory, 2008

Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog.
IEEE Trans. on CAD of Integrated Circuits and Systems, 2008

A Survey of Automated Techniques for Formal Software Verification.
IEEE Trans. on CAD of Integrated Circuits and Systems, 2008

Towards a Classification of Hamiltonian Cycles in the 6-Cube.
JSAT, 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

Race analysis for SystemC using model checking.
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 in System Design, 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.
STTT, 2006

Putting it all together - Formal verification of the VAMP.
STTT, 2006

Computing Over-Approximations with Bounded Model Checking.
Electr. Notes Theor. Comput. Sci., 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.
STTT, 2005

Making the Most of BMC Counterexamples.
Electr. Notes Theor. Comput. Sci., 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 in System Design, 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

Verification of SpecC using predicate abstraction.
Proceedings of the 2nd ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2004), 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...