Torben Amtoft | Associate Professor

Ph.D. - 1993, University of Aarhus, Denmark
Computer Science
M.Sc. - 1989, University of Copenhagen
Computer Science
B.S. - 1985, University of Copenhagen
Mathematics and Computer Science

Contact information

2179 Engineering Hall
785-532-7917
tamtoft@k-state.edu
Personal Website

Professional experience

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.

Research

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 focus on developing semantics-based techniques for analyzing correlations between variables and events.

Research keywords

semantics-based program analysis, program slicing, information flow analysis, probabilistic programming

Academic highlights

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.