版权所有:内蒙古大学图书馆 技术提供:维普资讯• 智图
内蒙古自治区呼和浩特市赛罕区大学西街235号 邮编: 010021
作者机构:Alexandru Ioan Cuza Univ Fac Comp Sci Iasi Romania Inria Lille Nord Europe Le Chesnay France
出 版 物:《JOURNAL OF SYMBOLIC COMPUTATION》 (符号计算杂志)
年 卷 期:2017年第80卷第Part1期
页 面:125-163页
核心收录:
学科分类:08[工学] 0701[理学-数学] 0812[工学-计算机科学与技术(可授工学、理学学位)]
主 题:Symbolic execution Programming language Formal operational semantics Reachability logic Circular coinduction Program verification
摘 要:We propose a language-independent symbolic execution framework. The approach is parameterised by a language definition, which consists of a signature for the syntax and execution infrastructure of the language, a model interpreting the signature, and rewrite rules for the language s operational semantics. Then, symbolic execution amounts to computing symbolic paths using a derivative operation. We prove that the symbolic execution thus defined has the properties naturally expected from it, meaning that the feasible symbolic executions of a program and the concrete executions of the same program mutually simulate each other. We also show how a coinduction-based extension of symbolic execution can be used for the deductive verification of programs. We show how the proposed symbolic-execution approach, and the coinductive verification technique based on it, can be seamlessly implemented in language definition frameworks based on rewriting such as the K framework. A prototype implementation of our approach has been developed in K. We illustrate it on the symbolic analysis and deductive verification of nontrivial programs. (C) 2016 Elsevier Ltd. All rights reserved.