咨询与建议

看过本文的还看了

相关文献

该作者的其他文献

文献详情 >A generic framework for symbol... 收藏

A generic framework for symbolic execution: A coinductive approach

为符号的执行的一个通用框架: 一条 coinductive 途径

作     者:Lucanu, Dorel Rusu, Vlad Arusoaie, Andrei 

作者机构: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.

读者评论 与其他读者分享你的观点

用户名:未登录
我的评分