Daniel Kroening

Last updated

Daniel Kroening (born 6 November 1975 [1] ) is a German computer scientist, Professor in computer science at the University of Oxford, and Chief Science Officer at the company he co-founded, Diffblue Ltd. [2] He is a fellow of Magdalen College.

Contents

Early life

Kroening was born in Mainz, Rhineland-Palatinate, Germany. He attended Marie-Therese-Gymnasium, Erlangen, Bavaria from 1986 to 1990 and Rotenbühl Gymnasium, Saarbrücken, Saarland from 1990 to 1995. [1] Kroening's early work in those highschool years includes implementations of data transfer protocols [3] and a bulletin board system (BBS) software package with Internet access management for small ISPs, which he released under free/open source licenses. [4] [5] In 1992, Kroening joined Handshake e.V., a local non-profit ISP. [3] From 1993, he hosted and operated Handshake's main BBS system and by the end of 1994, it was running his software. [6] Since 1996, he was also involved in Handshake's executive management. [1] After high school, Kroening completed his compulsory community service.

Career

In winter term 1996, Kroening started studying computer science and economics at Saarland University. [1] He received his diploma and doctoral degrees in 1999 and 2001. [2] He was one of the fastest students in the history of the faculty, taking just four and a half years from first year student to doctorate. [1]

After receiving his doctorate, Kroening worked at Carnegie Mellon University as a postdoc before joining ETH Zürich as assistant professor. [7] He finally settled at Oxford University.

Kroening's research has its focus on program and hardware analysis. [8]

He published textbooks on decision procedures and hardware design. [8]

Kroening's professional activities include being a committee member of the leading program analysis conference CAV. [8]

In his area of expertise, Kroening served as a consultant for companies like Intel, IBM and Fujitsu. [7] In 2016 he co-founded Diffblue Ltd [9] a developer tools company using artificial intelligence to write code. [10] [11] He is currently the Chief Science Officer of Diffblue. [12]

Selected publications

Related Research Articles

<span class="mw-page-title-main">Bulletin board system</span> Computer server

A bulletin board system (BBS), also called a computer bulletin board service (CBBS), is a computer server running software that allows users to connect to the system using a terminal program. Once logged in, the user can perform functions such as uploading and downloading software and data, reading news and bulletins, and exchanging messages with other users through public message boards and sometimes via direct chatting. In the early 1980s, message networks such as FidoNet were developed to provide services such as NetMail, which is similar to internet-based email.

Software engineering is an engineering-based approach to software development. A software engineer is a person who applies the engineering design process to design, develop, test, maintain, and evaluate computer software. The term programmer is sometimes used as a synonym, but may emphasize software implementation over design and can also lack connotations of engineering education or skills.

In computer science, static program analysis is the analysis of computer programs performed without executing them, in contrast with dynamic program analysis, which is performed on programs during their execution.

In computer science, formal methods are mathematically rigorous techniques for the specification, development, analysis, and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.

Software verification is a discipline of software engineering, programming languages, and theory of computation whose goal is to assure that software satisfies the expected requirements.

The Bread Board System (TBBS) is a multiline MS-DOS based commercial bulletin board system software package written in 1983 by Philip L. Becker. He originally created the software as the result of a poker game with friends that were praising the BBS software created by Ward Christensen. Becker said he could do better and founded eSoft, Inc. in 1984 based on the strength of TBBS sales.

Nando was an American internet news service and Internet service provider (ISP), founded in 1993 by the publishers of The News & Observer newspaper in Raleigh, North Carolina. Initially it relied on access via bulletin board technology. One of the first 24-hour news websites, the Nando Times, was launched in 1994, providing edited information from major news agencies that had not then developed their own websites.

<span class="mw-page-title-main">Department of Computer Science, University of Oxford</span> Department of the University of Oxford

The Department of Computer Science is the computer science department of the University of Oxford, England, which is part of the university's Mathematical, Physical and Life Sciences Division. It was founded in 1957 as the Computing Laboratory. By 2014 the staff count was 52 members of academic staff and over 80 research staff. The 2019, 2020 and 2021 Times World University Subject Rankings places Oxford University 1st in the world for Computer Science. Oxford University is also the top university for computer science in the UK and Europe according to Business Insider. The 2020 QS University Subject Rankings places The University of Oxford 5th in the world for Computer Science.

<span class="mw-page-title-main">Saarland University</span> University

Saarland University is a public research university located in Saarbrücken, the capital of the German state of Saarland. It was founded in 1948 in Homburg in co-operation with France and is organized in six faculties that cover all major fields of science. In 2007, the university was recognized as an excellence center for computer science in Germany.

In computer science and mathematical logic, satisfiability modulo theories (SMT) is the problem of determining whether a mathematical formula is satisfiable. It generalizes the Boolean satisfiability problem (SAT) to more complex formulas involving real numbers, integers, and/or various data structures such as lists, arrays, bit vectors, and strings. The name is derived from the fact that these expressions are interpreted within ("modulo") a certain formal theory in first-order logic with equality. SMT solvers are tools that aim to solve the SMT problem for a practical subset of inputs. SMT solvers such as Z3 and cvc5 have been used as a building block for a wide range of applications across computer science, including in automated theorem proving, program analysis, program verification, and software testing.

<span class="mw-page-title-main">Technical University of Kaiserslautern</span>

Technical University of Kaiserslautern was a public research university in Kaiserslautern, Germany.

<span class="mw-page-title-main">Patrick Cousot</span> French computer scientist

Patrick Cousot is a French computer scientist, currently Silver Professor of Computer Science at the Courant Institute of Mathematical Sciences, New York University, USA. Before he was Professor at the École Normale Supérieure (ENS), Paris, France, the École Polytechnique, Palaiseau, France and the University of Metz, France and a Research Scientist at the French National Center for Scientific Research (CNRS) at the Joseph Fourier University, Grenoble, France.

<span class="mw-page-title-main">Marta Kwiatkowska</span> British computer scientist

Marta Zofia Kwiatkowska is a Polish theoretical computer scientist based in the United Kingdom.

Johannes Maria Pistorius is a German badminton player. Born in Roth, Bavaria, Pistorius started playing badminton at aged 5, trained at the NSP Nürnberg since 2008, and joined the TSV 1906 Freystadt in 2014. He was the bronze medalists at the 2013 European Junior Championships in the boys' doubles and mixed team event. He graduated from Bertolt-Brecht school, and now educated at the Saarland University of Applied Sciences.

<span class="mw-page-title-main">Hardware backdoor</span> Hardware or firmware of computer chips

Hardware backdoors are backdoors in hardware, such as code inside hardware or firmware of computer chips. The backdoors may be directly implemented as hardware Trojans in the integrated circuit.

David Lansing Dill is a computer scientist and academic noted for contributions to formal verification, electronic voting security, and computational systems biology.

Michael Backes is a German professor of computer science. He is the founding director and CEO of the CISPA Helmholtz Center for Information Security. He is known for his work on formal methods, cryptography and privacy-enhancing technologies.

In model checking, a branch of computer science, linear time properties are used to describe requirements of a model of a computer system. Example properties include "the vending machine does not dispense a drink until money has been entered" or "the computer program eventually terminates". Fairness properties can be used to rule out unrealistic paths of a model. For instance, in a model of two traffic lights, the liveness property "both traffic lights are green infinitely often" may only be true under the unconditional fairness constraint "each traffic light changes colour infinitely often".

Diffblue Ltd is a spin-out from University of Oxford whose Cover product uses AI to automatically write unit tests for Java code. It is similar to GitHub Copilot in that it uses AI to write code, but differs in that it writes code fully autonomously vs. providing code suggestions for humans to review and edit. Diffblue was founded by Daniel Kroening and Peter Schrammel in 2016, and Mathew Lodge became CEO in July 2019

<span class="mw-page-title-main">Ofer Strichman</span>

Ofer Strichman is a professor of computational logic and computer science at the Davidson Industrial Engineering and Management, Technion – Israel Institute of Technology. He holds the Joseph Gruenblat chair in production engineering.

References

  1. 1 2 3 4 5 Kröning, Daniel. "Formal Verification of Pipelined Microprocessors" (PDF). emis.de. p. 80.
  2. 1 2 "Professor Daniel Kroening | Magdalen College Oxford". Magd.ox.ac.uk. Retrieved 28 June 2017.
  3. 1 2 "Daniel Kröning". www.kroening.handshake.de. Retrieved 10 May 2018.
  4. ↑ Kroening, Daniel. "DBOX BBS Package". www.dbox.handshake.de. Retrieved 10 May 2018.
  5. ↑ "DBOX". freshmeat.sourceforge.net. Retrieved 10 May 2018.
  6. ↑ Both, Andreas. "Chronik des Handshake e.V." www.handshake.de. Retrieved 10 May 2018.
  7. 1 2 "VorteQ Consulting - Daniel Kröning". www.vorteqconsulting.com. Archived from the original on 1 July 2016. Retrieved 10 May 2018.
  8. 1 2 3 "Home". kroening.com.
  9. ↑ "Diffblue". www.diffblue.com.
  10. ↑ "Daniel Kroening | HuffPost UK". Huffingtonpost.co.uk. 17 February 2017. Retrieved 28 June 2017.
  11. ↑ "An Oxford University artificial intelligence startup has raised £17 million to check code for errors". uk.news.yahoo.com. 2 July 2017. Retrieved 1 August 2017.
  12. ↑ "About Us".
This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.