无需模型检查即可实现符号执行 [英] implement symbolic execution without model-checking

问题描述

如何在不使用model checking和Finite State Machine (FSM)例如not(例如Java Path Finder)的情况下为particular language实现symbolic execution?我需要一个细节.例如，我可以使用哪种语言来实现此符号执行，还需要知道哪些其他内容?

How can I implement symbolic execution for particular language without using model checking and Finite State Machine (FSM) for example not such as Java Path Finder? I need a detail about it. for example by what language I can implement this symbolic execution and what other things I need to know?

推荐答案

您需要:

• 用于符号执行的语言的解析器，可以构建AST
• 名称解析(和相关的符号表)，因此当您的执行引擎遇到标识符时，它可以确定相关的类型和值
• 控制流分析，以便符号执行引擎可以通过程序跟踪控制流
• 可以构成和简化符号项的符号代数. 这需要一个解析器(因此您可以输入这样的方程式)和prettyprinter(因此您可以查看其计算结果)
• 一种在符号执行开始时指定假定值的方法

• A parser for the language to be symbolically executed that can build ASTs
• Name resolution (and associated symbol tables), so when your execution engine encounters an identifier it can determine the associated type and value
• Control flow analysis, so that the symbolic execution engine can follow flow of control through the program
• A symbolic algebra that can compose and simplify symbolic terms. This needs a parser (so you can enter such equations) and prettyprinter (so you can see what it computes)
• A way to specify assumed values at the point of symbolic execution start

这是很多机器，很难在一处找到所有东西.仅用一个工具就很难构建全部功能，这是您找不到很多这样的工具的部分原因.

This is rather a lot of machinery, and it is hard to find it all in one place. It is harder to build it all just for one tool, which is part of the reason you don't find many tools like this.

我们的 DMS软件再造工具包具有所有必要条件.您可能会找到一个示例 DMS实现的符号语言的概念有趣.

Our DMS Software Reengineering Toolkit has all the requisites. You may find an example of a symbolic language implemented with DMS interesting.

这篇关于无需模型检查即可实现符号执行的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！