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

• 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