Karl Palmskog

α About Me

I am a teacher and researcher at KTH Royal Institute of Technology in the Theoretical Computer Science division and the STEP research group. I do research primarily on topics related to program verification and proof engineering.

I was previously a postdoc at The University of Texas at Austin and University of Illinois at Urbana-Champaign. I obtained my Ph.D. in Computer Science in 2014 from KTH, advised by Mads Dam. Earlier, in 2007, I received my M.Sc. from KTH in Computer Science and Engineering.

See also my CV and my profiles on GitHub, Google Scholar, DBLP, ORCID, and LinkedIn.

β Research Interests

I am interested in development of techniques and tools based on proof assistants for construction of functionally correct and secure software systems. I also take a broad interest in programming languages, software engineering, and formal verification.

I am an avid user of the Coq proof assistant for both proving and programming, usually complemented by a measure of OCaml. I also use HOL4 and other dialects in the ML family.

γ Recent Publications

δ Current Projects

ε Past Projects

  • Trustfull (SSF)
  • Model-based, Event Driven Scalable Programming for the Mobile Cloud (NSF)
  • Highly Adaptable and Trustworthy Software (EU FP7)
  • 4WARD Future Internet (EU FP7)

ϛ Some Contributions to Software

Verified Software:

Proof Engineering Software: