Karl Palmskog

α About Me

I am a Research Fellow at The University of Texas at Austin, working in Milos Gligoric's group.

I was previously a Postdoctoral Research Associate and Visiting Scholar at the University of Illinois at Urbana-Champaign. I obtained my Ph.D. in Computer Science in 2014 from KTH Royal Institute of Technology in Stockholm, Sweden, advised by Mads Dam. Earlier, in 2007, I received my M.Sc. from KTH in Computer Science and Engineering.

See also my CV and GitHub profile.

β Research Interests

My interests span programming languages, formal methods, and software engineering. In particular, I am interested in how to construct large-scale distributed software systems with both formal and empirical evidence of correctness, and development of complementary proof engineering and testing techniques that make such construction possible.

I am an avid user of the Coq proof assistant for both proving and programming, usually complemented by a measure of OCaml.

Read my summary of our regression proving research from a Coq perspective, which includes suggestions for better support in proof assistants.

γ Recent Publications

  • Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric, and Zachary Tatlock
    QED at Large: A Survey of Engineering of Formally Verified Software
    Foundations and Trends in Programming Languages
    (FTPL), to appear, 2019.
  • Faria Kalim, Karl Palmskog, Jayasi Mehar, Adithya Murali, P. Madhusudan, and Indranil Gupta
    Kaizen: Building a Verified and Performant Blockchain System
    International Conference on Formal Methods in Computer-Aided Design
    (FMCAD 2019), to appear, San Jose, California, USA, October 2019.
  • Minas Charalambides, Karl Palmskog, and Gul Agha
    Types for Progress in Actor Programs
    Models, Languages, and Tools for Concurrent and Distributed Programming: Essays Dedicated to Rocco De Nicola on the Occasion of His 65th Birthday
    (LNCS 11665), 315-339, July 2019.
  • Karl Palmskog, Milos Gligoric, Lucas Pena, and Grigore Rosu
    Verifying Finality for Blockchain Systems
    International Workshop on Coq for Programming Languages
    (CoqPL 2019), Cascais, Portugal, January 2019.
  • Karl Palmskog, Ahmet Celik, and Milos Gligoric
    piCoq: Parallel Regression Proving for Large-Scale Verification Projects
    International Symposium on Software Testing and Analysis
    (ISSTA 2018), 344-355, Amsterdam, The Netherlands, July 2018.
  • Gul Agha and Karl Palmskog
    Transforming Threads into Actors: Learning Concurrency Structure from Execution Traces
    Principles of Modeling: Essays Dedicated to Edward A. Lee on the Occasion of His 60th Birthday
    (LNCS 10760), 16-37, July 2018.
  • Ahmet Celik, Karl Palmskog, and Milos Gligoric
    A Regression Proof Selection Tool for Coq
    International Conference on Software Engineering, Demo Papers
    (ICSE Demo 2018), 117-120, Gothenburg, Sweden, May 2018.
  • Gul Agha and Karl Palmskog
    A Survey of Statistical Model Checking
    ACM Trans. Model. Comput. Simul.
    (TOMACS), 28(1):6:1–6:39, January 2018.
  • Ahmet Celik, Karl Palmskog, and Milos Gligoric
    iCoq: Regression Proof Selection for Large-Scale Verification Projects
    International Conference on Automated Software Engineering
    (ASE 2017), 171-182, Urbana-Champaign, IL, USA, November 2017.
  • Ryan Doenges, James R. Wilcox, Doug Woos, Zachary Tatlock, and Karl Palmskog
    Verifying Implementations of Churn-Tolerant Distributed Systems
    International Workshop on Coq for Programming Languages
    (CoqPL 2017), Paris, France, January 2017.

δ Current Projects

ε Past Projects

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

ϛ Contributions to Proof Engineering Software and Verified Software