Patrick Cousot, On fixpoint/iteration/variant induction principles for proving total correctness of programs with denotational semantics

Patrick Cousot.
On fixpoint/iteration/variant induction principles for proving total correctness of programs with denotational semantics
In "Informal pre-proceedings of 29th International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR 2019), Maurizio Gabbrielli (Ed), Porto, Portugal, October 8-10, 2019. (Best paper award.)
Paper:
- PDF (590 KB)
Slides of the 25mn presentation at LOPSTR 2019:
- 1 slides per landscape page, (655 KB)
Abstract:
We study partial and total correctness proof methods based on generalized fixpoint and iteration induction principles applied to the denotational semantics of first-order functional and iterative programs.
Keywords:
Induction principles, Denotational semantics, Partial correctness, Total correctness, Verification

Bibliographic reference:

@inproceedings{DBLP:conf/lopstr/Cousot19,
  author    = {Patrick Cousot},
  title     = {On fixpoint/iteration/variant induction principles for proving total correctness of programs with denotational semantics},
  booktitle = {{LOPSTR} 2019},
  series    = {Lecture Notes in Computer Science},
  volume    = {to appear},
  publisher = {Springer},
  year      = {2019},
  url       = {http://cs.unibo.it/projects/lopstr19/proceedingsLOPSTR19.pdf}
}

copyright notice, Springer copyright notice
Last modified: Tue Oct 8 19:03:53 WEST 2019