[论文阅读笔记]DyTa: dynamic symbolic execution guided with static verification results

昨天到今天，抽了一些时间很快地浏览了一下这篇文章：

X. Ge, K. Taneja, T. Xie, and N. Tillmann, "DyTa: dynamic symbolic execution guided with static verification results," in Proceeding of the 33rd international conference on Software engineering, Waikiki, Honolulu, HI, USA, 2011, pp. 992-994.

觉得这篇文章和我们的工作很接近，不过还好只是一个3页的短文，并且着重于系统实现。

文章主要解决的问题是：动态符号执行面临着路径空间爆炸的问题，而静态分析存在很多false positives，文章的工作就是把两者结合，用动态符号执行来验证静态分析生成的defects，用静态分析的结果来指导动态符号执行的路径选择。

唉，这个想法真是和我半年前的想法一模一样！可见有了想法，一定要尽快付诸实施，要不随时可能被别人做了。还好这篇文章只是简单地提到这个想法，并没有在算法和效率上进行提高。并且针对的是C#代码。我们得尽快把之前的想法形成论文了。

-------------------------------------------------------------------------

文章用到的DSE（动态符号执行）框架是Pex，最早介绍Pex的论文是：

N. Tillmann and J. De Halleux, "Pex: white box test generation for .NET," in Proceedings of the 2nd international conference on Tests and proofs, Prato, Italy, 2008, pp. 134-153.

Pex的网址是：

http://research.microsoft.com/en-us/projects/pex/

-------------------------------------------------------------------------

另外，文章用到的静态分析工具是微软研究院开发的Code Contracts，该工具有一个Invited Talk：

F. Logozzo, "Practical verification for the working programmer with codecontracts and abstract interpretation," in Proceedings of the 12th international conference on Verification, model checking, and abstract interpretation, Austin, TX, USA, 2011, pp. 19-22.

下载的网址：http://research.microsoft.com/en-us/projects/contracts/ 似乎是可以免费使用的，文章中介绍，用户可使用该工具对C#源代码的preconditions，postconditions和class invariants进行预先设定，工具同时提供了对一些常见的C#编程错误（如dereferencing a null pointer，division by zero）进行检测的功能。文章中介绍，作者开发的工具可以从Code Contracts生成的对可能缺陷的描述中，提取contract-violation conditions（也就是error conditions），个人认为，能够生成contract-violation conditions，也就是这个工具的特点和名称的由来。

最后，这篇文章开发的系统的源码可以在：http://pexase.codeplex.com/ 中找到；该系统还有一个google site：
https://sites.google.com/site/asergrp/projects/dyta，不过由于GFW，后面这个网址访问不了。

今天就简单总结这么多。