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

  • Ahmet Celik, Karl Palmskog, Marinela Parovic, Emilio Jesús Gallego Arias, and Milos Gligoric
    Mutation Analysis for Coq
    International Conference on Automated Software Engineering
    (ASE 2019), to appear, San Diego, USA, November 2019.
  • Musab A. Alturki, Jing Chen, Victor Luchangco, Brandon Moore, Karl Palmskog, Lucas Peña, and Grigore Roşu
    Towards a Verified Model of the Algorand Consensus Protocol in Coq
    Workshop on Formal Methods for Blockchains
    (FMBC 2019), to appear, Porto, Portugal, October 2019.
  • 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
    (LNCS 11665), 315-339, July 2019.
  • Karl Palmskog, Milos Gligoric, Lucas Peña, and Grigore Roşu
    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
    (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