Loading...
Please wait, while we are loading the content...
Bug Catching : Automated Program Verification Lecture Notes on Diamonds and Total Correctness
| Content Provider | Semantic Scholar |
|---|---|
| Author | Fredrikson, Matt Platzer, André |
| Copyright Year | 2017 |
| Abstract | The previous lectures gave us a good understanding of how to reason about [·] properties of programs. We saw how to decompose in logic properties of the form [α;β]P and [if(Q)α elseβ]P etc. That is all good and useful, but we need to remember that [α]P means that P holds after all runs of program α. Since while programs α are deterministic and, thus, have at most one run, the formula [α]P , in particular, means that: |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://www.cs.cmu.edu/~15414/lectures/08-diamonds.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Notes |
