Skip to main content

Matthias Daum

Matthias Daum
Researcher

Research Interests

Matthias' research interest is in Formal Methods, more specifically in interactive theorem proving, software verification, and concurrency.

Contact Details

Phone: +61 2 9376 2339

More contact information is available at the Contact page.

Photo of Matthias Daum

Publication List

Projects

Past

Matthias works in the formal verification team of NICTA's Software Systems Research Group (SSRG). He is currently involved in the Trustworthy Systems project.

Career Summary

Prior to joining NICTA, Matthias has worked for more than 6 years in the Verisoft and Verisoft XT projects at the Saarland University.

Qualifications

Matthias holds a PhD in Computer Science from Saarland University.

Affiliations

Matthias is a Conjoint Lecturer at the School of Computer Science and Engineering of the University of New South Wales.

Publications

NICTA Papers

2014

Abstract PDF Matthias Daum, Nelson Billing and Gerwin Klein
Concerned with the unprivileged: User programs in kernel refinement
Formal Aspects of Computing, Volume 26, Number 6, pp. 1205-1229, October, 2014

2012

Abstract PDF Timothy Bourke, Matthias Daum, Gerwin Klein and Rafal Kolanski
Challenges and experiences in managing large-scale proofs
Conferences on Intelligent Computer Mathematics (CICM) / Mathematical Knowledge Management, pp. 32-48, Bremen, Germany, July, 2012

Non-NICTA Papers

2010

Abstract PDF Matthias Daum
On the formal foundation of a verification approach for system-level concurrent programs
PhD Thesis, Saarland University, Saarbrücken, 2010
You can find the corresponding theory files in release vlibvamos-trunk-r31570.tar.gz (5.2M) of the Verisoft Repository.
Abstract PDF Matthias Daum, Norbert W. Schirmer and Mareike Schmidt
From operating-system correctness to pervasively verified applications
International Conference on Integrated Formal Methods, pp. 105–120, Nancy, France, 2010
The original publication is available at www.springerlink.com.

2009

Abstract PDF Matthias Daum, Jan Dörrenbächer and Burkhart Wolff
Proving fairness and implementation correctness of a microkernel scheduler
Journal of Automated Reasoning: Special Issue on Operating System Verification, Volume 42, Number 2–4, pp. 349–388, 2009
The original publication is available at www.springerlink.com.
Abstract PDF Matthias Daum, Norbert W. Schirmer and Mareike Schmidt
Implementation correctness of a real-time operating system
IEEE International Conference on Software Engineering and Formal Methods, pp. 23–32, Hanoi, Vietnam, 2009
The original publication is available at www.computer.org.

2008

Abstract PDF Matthias Daum, Jan Dörrenbächer, Mareike Schmidt and Burkhart Wolff
A verification approach for system-level concurrent programs
Verified Software: Theories, Tools and Experiments, pp. 161–176, Toronto, Canada, October, 2008
Abstract PDF Matthias Daum, Jan Dörrenbächer and Sebastian Bogan
Model stack for the pervasive verification of a microkernel-based operating system
International Verification Workshop, pp. 56–70, Sydney, Australia, August, 2008