@inproceedings{4d311632916742b698c011f79c485d9d,
title = "KUPC: A formal tool for modeling and verifying dynamic updating of C programs",
abstract = "Dynamic Software Updating (DSU) is a useful technique for updating running software without incurring any downtime. Its correctness must be guaranteed because updating a running software is a complicated and safety-critical process. In this paper, we present a formal tool called KupC for modeling and verifying dynamic updating of C programs. The tool is built on K –a formal semantic framework for programming languages. We formalize a patch-based dynamic updating mechanism in K based on the formal executable operational semantics of C. The formalization automatically yields an interpreter and several verification tools, which can be used to formally analyze the correctness of dynamic updating for C programs. To our knowledge, KupC is the first formal tool for code-level verification of dynamic software updating.",
author = "Jiaqi Qian and Min Zhang and Yi Wang and Kazuhiro Ogata",
note = "Publisher Copyright: {\textcopyright} The Author(s) 2019.; 22nd International Conference on Fundamental Approaches to Software Engineering, FASE 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019 ; Conference date: 06-04-2019 Through 11-04-2019",
year = "2019",
doi = "10.1007/978-3-030-16722-6\_17",
language = "英语",
isbn = "9783030167219",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "299--305",
editor = "Reiner H{\"a}hnle and \{van der Aalst\}, Wil",
booktitle = "Fundamental Approaches to Software Engineering - 22nd International Conference, FASE 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings",
address = "德国",
}