Loading...
Please wait, while we are loading the content...
Similar Documents
Automatically Discovering Temporal Properties for Program Verification
| Content Provider | Semantic Scholar |
|---|---|
| Author | Yang, Jinlin Evans, David |
| Copyright Year | 2005 |
| Abstract | This paper reports on our experience using a dynamic analysis tool, Terracotta, to automatically infer temporal properties, and a model checker, Java PathFinder, to check the inferred properties. To our best knowledge, this is the first experiment using a model checker to check automatically inferred properties. We introduce two key ideas to make our approach effective. First, we develop techniques for handling context information in a program’s execution traces so that some interesting properties can be discovered. Second, we infer properties in a single threaded environment and to check them in a multi-threaded one. We evaluate our approach on a prototype implementation of a UNIX-like file system, Daisy. Our techniques revealed a bug in Daisy and identi fied several interesting and subtle temporal behaviors. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://www.cs.virginia.edu/jinlin/publications/TR05.pdf |
| Alternate Webpage(s) | http://www.cs.virginia.edu/~jy6q/publications/TR05.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
