Torben Amtoft | Associate Professor
Ph.D. - 1993, University of Aarhus, Denmark
M.Sc. - 1989, University of Copenhagen
B.S. - 1985, University of Copenhagen
Mathematics and Computer Science
Torben Amtoft received a bachelor's degree in mathematics and computer science from the University of Copenhagen, Denmark in 1985. He then focused on computer science and pursued graduate studies while working as a teaching assistant. After receiving a master's degree in 1989 from the University of Copenhagen, he received his Ph.D. in 1993 from the University of Aarhus, Denmark. The following decade he worked as a postdoctoral researcher — first at the University of Aarhus on a project funded by the European Union, next at Boston University on a project funded by the NSF, and most recently at Heriot-Watt University in Edinburgh, Scotland. In 2002 Amtoft joined the department of computing and information science at Kansas State University as an assistant professor; in 2008, he was promoted to associate professor with tenure. At K-State, in addition to being active in research, he has had a strong focus on teaching, providing courses on algorithms, programming languages, formal language theory, logical foundations of programming, software specification and databases.
Amtoft's research interest is in programming languages with a focus on semantics-based program analysis. Initially his focus was on type and effect systems, in particular predicting behavior of concurrent programs. Since coming to K-State, his main interest has been analysis of information flow and dependencies with applications to language-based security and program slicing. In the area of language-based security, Amtoft has extended his seminal work from 2004 — a joint effort with Anindya Banerjee on logic-based information flow analysis in several directions in collaboration with John Hatcliff's group at K-State — to also include conditional information flow, and to give a precise analysis of various features found in realistic programming languages such as objects and aliases, procedures and arrays. He also led efforts to design a system for formal verification of information flow contracts — the idea implemented in the context of Spark and using the Coq proof assistant to let programs carry ``evidence'' they do satisfy certain information flow properties. In the area of program slicing, Amtoft has been able to extend the concept while providing semantic justifications to new programming paradigms such as reactive systems designed to run interactively, this in collaboration with John Hatcliff's group; systems with non-deterministic choices, this in collaboration with Mark Harman's group in London; and probabilistic programs, this in collaboration with Anindya Banerjee. Recently he has been exploring models for probabilistic programming with numerous potential applications such as game theory.
semantics-based program analysis, program slicing, information flow analysis, probabilistic programming
Amtoft has co-authored one monograph, 10 journal papers, 19 conference papers and five other reviewed papers; in all but six of these publications, he is listed as first author. He received, jointly with Anindya Banerjee, the Best Paper Award for the 2004 edition of the Static Analysis Symposium.