Notes on Proof Outline Logic
| dc.contributor.author | Schneider, Fred B. | en_US |
| dc.date.accessioned | 2007-04-23T16:27:00Z | |
| dc.date.available | 2007-04-23T16:27:00Z | |
| dc.date.issued | 1995-01 | en_US |
| dc.description.abstract | Formulas of Proof Outline Logic are program texts annotated with assertions. Assertions may contain control predicates as well as terms whose values depend on previous states, making the assertion language rather expressive. The logic is complete for proving safety properties of concurrent programs. A deductive system for the logic is presented. Solutions to the mutual exclusion and readers/writers problems illustrate how the logic can be used as a tool for program development. | en_US |
| dc.format.extent | 159920 bytes | |
| dc.format.extent | 334801 bytes | |
| dc.format.mimetype | application/pdf | |
| dc.format.mimetype | application/postscript | |
| dc.identifier.citation | http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR95-1476 | en_US |
| dc.identifier.uri | https://hdl.handle.net/1813/6085 | |
| dc.language.iso | en_US | en_US |
| dc.publisher | Cornell University | en_US |
| dc.subject | computer science | en_US |
| dc.subject | technical report | en_US |
| dc.title | Notes on Proof Outline Logic | en_US |
| dc.type | technical report | en_US |