Daniel Kroening

Foto

Daniel Kröning

Computing Laboratory, Oxford University.
Fellow of Magdalen College
Phone: +44-1865-283506
E-Mail: kroening@handshake.de
My PGP public key is here

NEWS

Decision Procedures
An Algorithmic Point of View

Digitaltechnik
Eine praxisnahe Einführung

SOFTWARE VERIFICATION

CBMC - ANSI-C Bounded Model Checker
SATABS - Predicate Abstraction for ANSI-C

HARDWARE VERIFICATION

VCEGAR - Predicate Abstraction for Verilog
Formal Verification of Pipelined Microprocessors (Dissertation)
Coming soon: Behavioral Verilog Synthesis tools

SELECTED PAPERS

The Impact of Hardware Scheduling Mechanisms on the Performance and Cost of Processor Designs
Proving the Correctness of Processors with Delayed Branch using Delayed PC
This paper appreared previously at the HLVDT workshop.
Proving the Correctness of Pipelined Micro-Architectures
Automated Pipeline Design
Application Specific Higher Order Logic Theorem Proving
Formal Verification of Pipelined Microprocessors
This paper is a summary of my thesis.
Efficient Computation of Recurrence Diameters
Hardware Verification using ANSI-C Programs as a Reference
Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking
A long version of this paper is available as CMU Technical Report.
Specifying and Verifying Systems with Multiple Clocks
Using SAT based Image Computation for Reachability Analysis
Instantiating uninterpreted functional units and memory system: functional verification of the VAMP processor
Completeness and Complexity of Bounded Model Checking
A Tool for Checking ANSI-C Programs
Predicate Abstraction of ANSI-C Programs using SAT
A previous version of this paper is also available as CMU technical report.
A short version of this paper appeared previously at a DSN workshop.
Fault Tolerance Tradeoffs in Moving from Decentralized to Centralized Embedded System Architectures
A SAT-Based Algorithm for Reparameterization in Symbolic Simulation
A previous version of this paper is also available as CMU technical report.
Understanding Counterexamples with explain
Bounded Model Checking and Inductive Verification of Hybrid Discrete-continuous Systems
Abstraction-based Satisfiability Solving of Presburger Arithmetic
A previous version of this paper is also available as CMU technical report.
Experiments with SAT-Based Symbolic Simulation Using Reparameterization in the Abstraction Refinement Framework
Making the Most of BMC Counterexamples
Checking Consistency of C and Verilog using Predicate Abstraction and Induction
A previous version of this paper is also available as CMU technical report.
Counterexample Guided Abstraction Refinement via Program Execution
Computational Challenges in Bounded Model Checking
SATABS: SAT-based Predicate Abstraction for ANSI-C
Cogent: Accurate theorem proving for program verification
A full version of this paper is available in the Post-Proceedings of ISoLA 2004
Error Explanation with Distance Metrics
Putting it all together - Formal Verification of the VAMP
Formal Verification of SystemC by Automatic Hardware/Software Partitioning
Symbolic model checking for asynchronous Boolean programs
A previous version of this paper is available as ETH Technical Report.
Computing Over-Approximations with Bounded Model Checking
A previous version of this paper is available as ETH Technical Report.
Verification of SpecC using Predicate Abstraction
A previous version of this paper appeared at MEMOCODE 2004
Approximating Predicate Images for Bit-Vector Logic
Counterexamples with Loops for Predicate Abstraction
Decision Procedures for the Grand Challenge
ExpliSAT: Guiding SAT-Based Software Verification with Explicit States
Image Computation and Predicate Refinement for RTL Verilog using Word Level Proofs
VCEGAR: Verilog CounterExample Guided Abstraction Refinement
A First Step Towards a Unified Proof Checker for QBF
An Algebraic Algorithm for the Identification of Glass Networks with Periodic Orbits along Cyclic Attractors
SAT-based Summarisation for Boolean Programs
Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog
This is an extended version of a paper that appeared at DAC 2005.
A previous version of this paper is also available as CMU technical report.
Model Checking with Abstraction for Web Services
Verification of Boolean Programs with Unbounded Thread Creation
This is an extended version of a paper that appeared at FMCAD 2006.
Lifting Propositional Interpolants to the Word-Level
Static Analysis to Enhance the Power of Model Checking for Concurrent Software
Verifying C++ with STL Containers via Predicate Abstraction
Model Checking Concurrent Linux Device Drivers
A Complete Bounded Model Checking Algorithm for Pushdown Systems
Approximation Refinement for Interpolation-Based Model Checking
Formal Verification at Higher Levels of Abstraction
Scoot: A Tool for the Analysis of SystemC Models
A Survey of Automated Techniques for Formal Software Verification
Computing Binary Combinatorial Gray Codes via Exhaustive Search with SAT-Solvers
An extended version of this paper is available as ETH Technical Report.
Classification of Hamiltonian Cycles in the 6-Cube
Deciding Bit-Vector Arithmetic with Abstraction
A previous version of this paper has appeared at TACAS.
Race Analysis for SystemC using Model Checking
Loop Summarization using Abstract Transformers

TEACHING

At CMU:

15-820A: Theorem Proving and Model Checking in PVS (Spring 2003)
17-651A: Models of Software Systems (Fall 2003)

At ETH:

251-0247-00 Formal Verification
251-0207-00 Seminar Digitaltechnik und Rechnerarchitektur
251-0211-00 Spezifikation und Verifikation objektorientierter Software
252-0014-00 Digitaltechnik
251-0276-00 Software Engineering Seminar

In Oxford:

Object Oriented Design
Automated Software Verification

MISC

I am on the PC of MEMOCODE 2004, CAV 2005, SoftMC 2005, MEMOCODE 2005, SVV 2005, BMC 2006, IBM Verification Conference 2006, MEMOCODE 2006, PDPAR 2006, FMCAD 2007, BMC 2007, ProVecs 2007, CAV 2008, FMCAD 2008, HVC 2008, and DATE 2009.