Proof-Carrying Parameters in Certified Symbolic Execution: The Case Study of Antiunification

Autor:	Arusoaie, Andrei, Lucanu, Dorel
Rok vydání:	2021
Předmět:	Computer Science - Logic in Computer Science
Zdroj:	EPTCS 369, 2022, pp. 1-16
Druh dokumentu:	Working Paper
DOI:	10.4204/EPTCS.369.1
Popis:	Symbolic execution uses various algorithms (matching, (anti)unification), whose executions are parameters for proof object generation. This paper proposes a generic method for generating proof objects for such parameters. We present in detail how our method works for the case of antiunification. The approach is accompanied by an implementation prototype, including a proof object generator and a proof object checker. In order to investigate the size of the proof objects, we generate and check proof objects for inputs inspired from the K definitions of C and Java. Comment: In Proceedings FROM 2022, arXiv:2209.09208
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/2110.11700 Zobrazit plný text záznamu View this record from Arxiv