Quick Links
Daniel Kröning
|
Computer Science Department,
Oxford University. |
|
| Phone: | +44-1865-283506 |
| E-Mail: |
kroening@handshake.de My PGP public key is here. |
News
NEW: We are hiring Postdocs and PhD students!
Research
I am interested in formal methods for the correct construction of hardware and software systems, 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 implementations 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.
- NEW Symmetry-Aware Predicate Abstraction for Shared-Variable Concurrent Programs
- NEW Linear Completeness Thresholds for Bounded Model Checking
- NEW Test-Case Generation for Embedded Simulink via Formal Concept Analysis
- NEW Loop Summarization and Termination Analysis
- Termination Analysis with Compositional Transition Invariants
- Dynamic Cutoff Detection in Parameterized Concurrent Programs
- An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic
- Automatic Analysis of Scratch-pad Memory Code for Heterogeneous Multicore Processors
- Ranking Function Synthesis for Bit-Vector Relations
- Symbolic Counter Abstraction for Concurrent Software
- 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. - A Tool for Checking ANSI-C Programs
- Predicate Abstraction of ANSI-C Programs using SAT
Teaching
At CMU:- 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
- Software Verification
- Computer-Aided Formal Verification
- Computer Architecture
Service
I am on the PC of DATE 2010, TACAS 2010, CAV 2010, CAV 2011 and TACAS 2012.