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 Rocq Prover 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

• Andreas Lindner, Karl Palmskog, Scott Constable, Mads Dam, Roberto Guanciale, and Hamed Nemati
  Forward Symbolic Execution for Trustworthy Automation of Binary Code Verification
  International Conference on Verification, Model Checking, and Abstract Interpretation
  (VMCAI 2026), to appear, Rennes, France, January 2026.
• Karl Palmskog, Mattias Nyberg, and Dilian Gurov
  Machine-Checked Compositional Specification and Proofs for Embedded Systems
  International Symposium on Theoretical Aspects of Software Engineering
  (TASE 2025), pp. 67-82, Limassol, Cyprus, July 2025.
• Ana de Almeida Borges, Annalí Casanueva Artís, Jean-Rémy Falleri, Emilio Jesús Gallego Arias, Érik Martin-Dorel, Karl Palmskog, Alexander Serebrenik, and Théo Zimmermann
  Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users
  Journal of Automated Reasoning
  Volume 69, article number 8, February 2025.
• Gustav Ung, Jesper Amilon, Dilian Gurov, Christian Lidström, Mattias Nyberg, and Karl Palmskog
  Post-Hoc Formal Verification of Automotive Software with Informal Requirements: An Experience Report
  International Requirements Engineering Conference
  (RE 2024), Reykjavik, Iceland, June 2024.
• Ana de Almeida Borges, Annalí Casanueva Artís, Jean-Rémy Falleri, Emilio Jesús Gallego Arias, Érik Martin-Dorel, Karl Palmskog, Alexander Serebrenik, and Théo Zimmermann
  Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users
  International Conference on Interactive Theorem Proving
  (ITP 2023), 12:1-12:18, Bialystok, Poland, August 2023.
• Vlad Zamfir, Denisa Diaconescu, Wojciech Kołowski, Brandon Moore, Karl Palmskog, Traian Florin Serbanuta, and Ioan Teodorescu
  VLSM: A General Coq Framework for Reasoning About Faulty Distributed Systems
  The Coq Workshop
  (Coq 2023), Bialystok, Poland, July 2023.
• Anoud Alshnakat, Didrik Lundberg, Roberto Guanciale, Mads Dam, and Karl Palmskog
  HOL4P4: semantics for a verified data plane
  International Workshop on P4 in Europe
  (EuroP4 2022), 39-45, Rome, Italy, December 2022.
• Karl Palmskog, Xiaomo Yao, Ning Dong, Roberto Guanciale, and Mads Dam
  Foundations and Tools in HOL4 for Analysis of Microarchitectural Out-of-Order Execution
  Formal Methods in Computer-Aided Design
  (FMCAD 2022), 129-137, Trento, Italy, October 2022.
• Ana de Almeida Borges, Jean-Rémy Falleri, Jim Fehrle, Emilio Jesús Gallego Arias, Erik Martin-Dorel, Karl Palmskog, Alexander Serebrenik and Théo Zimmermann
  Coq Community Survey 2022: Summary of Results
  The Coq Workshop
  (Coq 2022), Haifa, Israel, August 2022.
• Pierre Castéran, Jérémy Damour, Karl Palmskog, Clément Pit-Claudel, and Théo Zimmermann
  Hydras & Co.: Formalized mathematics in Coq for inspiration and entertainment
  Journées Francophones des Langages Applicatifs
  (JFLA 2022), St-Médard d'Excideuil, France, June 2022.
• Karl Palmskog, Enrico Tassi, and Théo Zimmermann
  Reliably Reproducing Machine-Checked Proofs with the Coq Platform
  Workshop on Reproducibility and Replication of Research Results
  (RRRR 2022), Munich, Germany, April 2022.
• Pengyu Nie, Karl Palmskog, Junyi Jessy Li, and Milos Gligoric
  Roosterize: Suggesting Lemma Names for Coq Verification Projects Using Deep Learning
  International Conference on Software Engineering, Tool Demonstrations Track
  (ICSE Demo 2021), 21-24, Madrid, Spain, June 2021.
• Pengyu Nie, Karl Palmskog, Junyi Jessy Li, and Milos Gligoric
  Learning to Format Coq Code Using Language Models
  The Coq Workshop
  (Coq 2020), Paris, France, July 2020.
• Pengyu Nie, Karl Palmskog, Junyi Jessy Li, and Milos Gligoric
  Deep Generation of Coq Lemma Names Using Elaborated Terms
  International Joint Conference on Automated Reasoning
  (IJCAR 2020), 97-118, Paris, France, July 2020.
• Kush Jain, Karl Palmskog, Ahmet Celik, Emilio Jesús Gallego Arias, and Milos Gligoric
  mCoq: Mutation Analysis for Coq Verification Projects
  International Conference on Software Engineering, Tool Demonstrations Track
  (ICSE Demo 2020), 89-92, Seoul, South Korea, July 2020.
• Karl Palmskog, Ahmet Celik, and Milos Gligoric
  Practical Machine-Checked Formalization of Change Impact Analysis
  International Conference on Tools and Algorithms for the Construction and Analysis of Systems
  (TACAS 2020), 137-157, 2020.
• 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), 539-551, San Diego, CA, 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), 362-367, Porto, Portugal, October 2019.
• Faria Kalim, Karl Palmskog, Jayasi Mehar, Adithya Murali, P. Madhusudan, and Indranil Gupta
  Kaizen: Building a Performant Blockchain System Verified for Consensus and Integrity
  International Conference on Formal Methods in Computer-Aided Design
  (FMCAD 2019), 96-104, San Jose, CA, USA, 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), Vol. 5: No. 2-3, pp 102-281, September 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, Tool Demonstrations Track
  (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

• Coq-community
• Proof Engineering (GitHub)
• Distributed Components (GitHub)

ε 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:

• Algorand Verification
• Chip
• Verdi
• Verdi Raft
• Disel

Proof Engineering Software:

• SerAPI
• mCoq
• Ott