Loading...
Please wait, while we are loading the content...
Similar Documents
The Modularity and Automation of Object Propositions
| Content Provider | Semantic Scholar |
|---|---|
| Author | Nistor, Ligia Aldrich, Jonathan |
| Copyright Year | 2014 |
| Abstract | Developing a formal veri cation system that is powerful, modular, and provides good support for automation is challenging. In this paper, we explore the expressiveness, modularity, and automation of our recently proposed object propositions veri cation system, using two examples. The rst example is a spreadsheet of simple cells that add their inputs and share their output with other spreadsheet cells. The second example is a simulator for two queues of jobs, one containing large jobs the other small jobs, along with a producer, consumer, and controller. The examples illustrate challenges for modular reasoning in the presence of shared state (the cells or queues). We specify the examples using object propositions, prove their correctness, and then compare to separation logic speci cations with respect to modularity. We also present the translation rules needed for the automatic translation of the object propositions veri cation methodology into the Boogie intermediate veri cation language. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://www.cs.cmu.edu/~lnistor/ictac14.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
