Karl Palmskog

39 papers A* 2A 2B 4C 1Misc 1Journal 15Unranked 13
YearRankTypeTitle / Venue / Authors
2026 B conf
Forward Symbolic Execution for Trustworthy Automation of Binary Code Verification.
VMCAI
Andreas Lindner, Karl Palmskog, Scott Constable, Mads Dam, Roberto Guanciale, Hamed Nemati
2025 J jnl
Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users.
J. Autom. Reason.
Ana de Almeida Borges, Annalí Casanueva Artís, Jean-Rémy Falleri, Emilio Jesús Gallego Arias, Érik Martin-Dorel, Karl Palmskog, Alexander Serebrenik, Théo Zimmermann
2025 Misc conf
Machine-Checked Compositional Specification and Proofs for Embedded Systems.
TASE
Karl Palmskog, Mattias Nyberg, Dilian Gurov
2025 J jnl
Trustworthy Verification of RISC-V Binaries Using Symbolic Execution in HolBA.
CoRR
Karl Palmskog, Andreas Lindner, Scott Constable, Roberto Guanciale, Hamed Nemati
2024 A conf
Post-Hoc Formal Verification of Automotive Software with Informal Requirements: An Experience Report.
RE
Gustav Ung, Jesper Amilon, Dilian Gurov, Christian Lidström, Mattias Nyberg, Karl Palmskog
2023 B conf
Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users.
ITP
Ana de Almeida Borges, Annalí Casanueva Artís, Jean-Rémy Falleri, Emilio Jesús Gallego Arias, Érik Martin-Dorel, Karl Palmskog, Alexander Serebrenik, Théo Zimmermann
2022 B conf
Foundations and Tools in HOL4 for Analysis of Microarchitectural Out-of-Order Execution.
FMCAD
Karl Palmskog, Xiaomo Yao, Ning Dong, Roberto Guanciale, Mads Dam
2022 — conf
HOL4P4: semantics for a verified data plane.
EuroP4@CoNEXT
Anoud Alshnakat, Didrik Lundberg, Roberto Guanciale, Mads Dam, Karl Palmskog
2022 J jnl
Reliably Reproducing Machine-Checked Proofs with the Coq Platform.
CoRR
Karl Palmskog, Enrico Tassi, Théo Zimmermann
2022 J jnl
VLSM: Validating Labelled State Transition and Message Production Systems.
CoRR
Vlad Zamfir, Mihai Calancea, Denisa Diaconescu, Brandon M. Moore, Karl Palmskog, Traian-Florin Serbanuta, Michael Stay
2021 — conf
Roosterize: Suggesting Lemma Names for Coq Verification Projects Using Deep Learning.
ICSE (Companion Volume)
Pengyu Nie, Karl Palmskog, Junyi Jessy Li, Milos Gligoric
2021 J jnl
Roosterize: Suggesting Lemma Names for Coq Verification Projects Using Deep Learning.
CoRR
Pengyu Nie, Karl Palmskog, Junyi Jessy Li, Milos Gligoric
2020 — conf
Deep Generation of Coq Lemma Names Using Elaborated Terms.
IJCAR (2)
Pengyu Nie, Karl Palmskog, Junyi Jessy Li, Milos Gligoric
2020 J jnl
Deep Generation of Coq Lemma Names Using Elaborated Terms.
CoRR
Pengyu Nie, Karl Palmskog, Junyi Jessy Li, Milos Gligoric
2020 J jnl
Learning to Format Coq Code Using Language Models.
CoRR
Pengyu Nie, Karl Palmskog, Junyi Jessy Li, Milos Gligoric
2020 — conf
Practical Machine-Checked Formalization of Change Impact Analysis.
TACAS (2)
Karl Palmskog, Ahmet Çelik, Milos Gligoric
2020 J jnl
QED at Large: A Survey of Engineering of Formally Verified Software.
CoRR
Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric, Zachary Tatlock
2020 J jnl
Specification of the Giskard Consensus Protocol.
CoRR
Elaine Li, Karl Palmskog, Mircea Sebe, Grigore Rosu
2020 — conf
mCoq: mutation analysis for Coq verification projects.
ICSE (Companion Volume)
Kush Jain, Karl Palmskog, Ahmet Çelik, Emilio Jesús Gallego Arias, Milos Gligoric
2019 B conf
Kaizen: Building a Performant Blockchain System Verified for Consensus and Integrity.
FMCAD
Faria Kalim, Karl Palmskog, Jayasi Mehar, Adithya Murali, Indranil Gupta, P. Madhusudan
2019 A* conf
Mutation Analysis for Coq.
ASE
Ahmet Çelik, Karl Palmskog, Marinela Parovic, Emilio Jesús Gallego Arias, Milos Gligoric
2019 J jnl
QED at Large: A Survey of Engineering of Formally Verified Software.
Found. Trends Program. Lang.
Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric, Zachary Tatlock
2019 — conf
Towards a Verified Model of the Algorand Consensus Protocol in Coq.
FM Workshops (1)
Musab A. Alturki, Jing Chen, Victor Luchangco, Brandon M. Moore, Karl Palmskog, Lucas Peña, Grigore Rosu
2019 J jnl
Towards a Verified Model of the Algorand Consensus Protocol in Coq.
CoRR
Musab A. Alturki, Jing Chen, Victor Luchangco, Brandon M. Moore, Karl Palmskog, Lucas Peña, Grigore Rosu
2019 — conf
Types for Progress in Actor Programs.
Models, Languages, and Tools for Concurrent and Distributed Programming
Minas Charalambides, Karl Palmskog, Gul Agha
2018 J jnl
A Survey of Statistical Model Checking.
ACM Trans. Model. Comput. Simul.
Gul Agha, Karl Palmskog
2018 — conf
A regression proof selection tool for coq.
ICSE (Companion Volume)
Ahmet Çelik, Karl Palmskog, Milos Gligoric
2018 — conf
Transforming Threads into Actors: Learning Concurrency Structure from Execution Traces.
Principles of Modeling
Gul Agha, Karl Palmskog
2018 A conf
piCoq: parallel regression proving for large-scale verification projects.
ISSTA
Karl Palmskog, Ahmet Çelik, Milos Gligoric
2017 J jnl
Inferring Formal Properties of Production Key-Value Stores.
CoRR
Edgar Pek, Pranav Garg, Muntasir Raihan Rahman, Karl Palmskog, Indranil Gupta, P. Madhusudan
2017 A* conf
iCoq: regression proof selection for large-scale verification projects.
ASE
Ahmet Çelik, Karl Palmskog, Milos Gligoric
2015 J jnl
A Case Study on Executing Instrumented Code in Java PathFinder.
ACM SIGSOFT Softw. Eng. Notes
Karl Palmskog, Farah Hariri, Darko Marinov
2015 J jnl
Location-independent routing in process network overlays.
Serv. Oriented Comput. Appl.
Mads Dam, Karl Palmskog
2014 C conf
Location Independent Routing in Process Network Overlays.
PDP
Mads Dam, Karl Palmskog
2014 — —
Towards Correct and Efficient Program Execution in Decentralized Networks: Programming Languages, Semantics, and Resource Management.
Karl Palmskog
2013 — conf
ABS-NET: Fully Decentralized Runtime Adaptation for Distributed Objects.
ICE
Karl Palmskog, Mads Dam, Andreas Lundblad, Ali Jafari
2013 — conf
Efficient and fully abstract routing of futures in object network overlays.
AGERE!@SPLASH
Mads Dam, Karl Palmskog
2012 — conf
Secure distributed top-k aggregation.
ICC
Kristján Valur Jónsson, Karl Palmskog, Ymir Vigfusson
2007 — conf
Session Layer Resurgence: Towards Mobile, Disconnection- and Delay-Tolerant Communication.
ECUMN
Yuri Ismailov, Karl Palmskog, Micael Widell, Petter Arvidsson, YaoShuang Wang