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

Decision Procedures An Algorithmic Point of View

Digitaltechnik Eine praxisnahe Einführung

News: I am looking to hire PhD (DPhil) students at Oxford University.
The description of the post is here. I am also looking for PostDocs (RAs) in systems design and/or verification.

Read the proposal for a theory for lists/sets/maps for the SMT-Lib.

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

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

• 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
• 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
  A previous version of this paper appeared at DAC 2005.
  An earlier 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
  A previous version of this paper 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
  This paper is at rank 7 on this list.
• 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
• An Efficient SAT Encoding of Circuit Codes
• Strengthening Properties using Abstraction Refinement
• Fixed Points in Multi-Cycle Path Detection
• Verification and Falsification of Programs with Loops using Predicate Abstraction
  A previous version of this paper has appeared at CAV.
• A Framework for Decision Procedures in Program Verification
• Symbolic Counter Abstraction for Concurrent Software
• A Propositional Encoding of Lean Induced Cycles in Binary Hypercubes

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

• 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

• Object Oriented Design
• Automated Software Verification
• Computer-Aided Formal Verification

• 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, DATE 2009, APV 2009, MEMOCODE 2009, CAV 2009, FMICS 2009, FMCAD 2009, SMT 2009, DATE 2010, and TACAS 2010.

• I am co-organizing the Tools Workshop at VSTTE 2008.