equal
deleted
inserted
replaced
309 session "HOL-Hoare" in Hoare = HOL + |
309 session "HOL-Hoare" in Hoare = HOL + |
310 description " |
310 description " |
311 Verification of imperative programs (verification conditions are generated |
311 Verification of imperative programs (verification conditions are generated |
312 automatically from pre/post conditions and loop invariants). |
312 automatically from pre/post conditions and loop invariants). |
313 " |
313 " |
314 theories Hoare |
314 theories |
|
315 Examples |
|
316 ExamplesAbort |
|
317 ExamplesTC |
|
318 Pointers0 |
|
319 Pointer_Examples |
|
320 Pointer_ExamplesAbort |
|
321 SchorrWaite |
|
322 Separation |
315 document_files "root.bib" "root.tex" |
323 document_files "root.bib" "root.tex" |
316 |
324 |
317 session "HOL-Hoare_Parallel" (timing) in Hoare_Parallel = HOL + |
325 session "HOL-Hoare_Parallel" (timing) in Hoare_Parallel = HOL + |
318 description " |
326 description " |
319 Verification of shared-variable imperative programs a la Owicki-Gries. |
327 Verification of shared-variable imperative programs a la Owicki-Gries. |