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