Daniel Kröning

News

NEW: We are hiring Postdocs and PhD students!

Research

I am interested in formal methods for the correct construction of hardware and software sys­tems, with a focus on automated methods for checking compliance of an implementation with a specification.

I am particularily interested in applying these methods to practical hard- and software im­ple­mentations given in languages like C or C++.

Selected Papers

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

A full list of my papers is available here.

• Automatic Analysis of Scratch-pad Memory Code for Heterogeneous Multicore Processors
• Ranking Function Synthesis for Bit-Vector Relations
• Symbolic Counter Abstraction for Concurrent Software
• Mixed Abstractions for Floating-Point Arithmetic
• Verification and Falsification of Programs with Loops using Predicate Abstraction
  A previous version of this paper has appeared at CAV.
• A Survey of Automated Techniques for Formal Software Verification
  This paper is at rank 7 on this list.
• Deciding Bit-Vector Arithmetic with Abstraction
  A previous version of this paper has appeared at TACAS.
• Verification of Boolean Programs with Unbounded Thread Creation
• Approximating Predicate Images for Bit-Vector Logic
• Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog
  A previous version of this paper appeared at DAC 2005.
• Computational Challenges in Bounded Model Checking
• A Tool for Checking ANSI-C Programs
• Predicate Abstraction of ANSI-C Programs using SAT
• Abstraction-based Satisfiability Solving of Presburger Arithmetic
• Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking

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
• Computer-Aided Formal Verification

Service

• 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, HWVW 2010, TACAS 2010, and CAV 2010.

• I am co-chairing SMT 2010.

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