On Fixpoint/Iteration/Variant Induction Principles for Proving Total Correctness of Programs with Denotational Semantics

Patrick Cousot

doi:10.1007/978-3-030-45260-5_1

On Fixpoint/Iteration/Variant Induction Principles for Proving Total Correctness of Programs with Denotational Semantics

Patrick Cousot

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

We study partial and total correctness proof methods based on generalized fixpoint/iteration/variant induction principles applied to the denotational semantics of first-order functional and iterative programs.

Original language	English (US)
Title of host publication	Logic-Based Program Synthesis and Transformation - 29th International Symposium, LOPSTR 2019, Revised Selected Papers
Editors	Maurizio Gabbrielli
Publisher	Springer
Pages	3-18
Number of pages	16
ISBN (Print)	9783030452599
DOIs	https://doi.org/10.1007/978-3-030-45260-5_1
State	Published - 2020
Event	29th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2019 - Porto, Portugal Duration: Oct 8 2019 → Oct 10 2019

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	12042 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	29th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2019
Country/Territory	Portugal
City	Porto
Period	10/8/19 → 10/10/19

Keywords

Denotational semantics
Induction principles
Partial and total correctness
Verification

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-030-45260-5_1

Cite this

Cousot, P. (2020). On Fixpoint/Iteration/Variant Induction Principles for Proving Total Correctness of Programs with Denotational Semantics. In M. Gabbrielli (Ed.), Logic-Based Program Synthesis and Transformation - 29th International Symposium, LOPSTR 2019, Revised Selected Papers (pp. 3-18). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12042 LNCS). Springer. https://doi.org/10.1007/978-3-030-45260-5_1

On Fixpoint/Iteration/Variant Induction Principles for Proving Total Correctness of Programs with Denotational Semantics. / Cousot, Patrick.
Logic-Based Program Synthesis and Transformation - 29th International Symposium, LOPSTR 2019, Revised Selected Papers. ed. / Maurizio Gabbrielli. Springer, 2020. p. 3-18 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12042 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Cousot, P 2020, On Fixpoint/Iteration/Variant Induction Principles for Proving Total Correctness of Programs with Denotational Semantics. in M Gabbrielli (ed.), Logic-Based Program Synthesis and Transformation - 29th International Symposium, LOPSTR 2019, Revised Selected Papers. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 12042 LNCS, Springer, pp. 3-18, 29th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2019, Porto, Portugal, 10/8/19. https://doi.org/10.1007/978-3-030-45260-5_1

Cousot P. On Fixpoint/Iteration/Variant Induction Principles for Proving Total Correctness of Programs with Denotational Semantics. In Gabbrielli M, editor, Logic-Based Program Synthesis and Transformation - 29th International Symposium, LOPSTR 2019, Revised Selected Papers. Springer. 2020. p. 3-18. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-45260-5_1

Cousot, Patrick. / On Fixpoint/Iteration/Variant Induction Principles for Proving Total Correctness of Programs with Denotational Semantics. Logic-Based Program Synthesis and Transformation - 29th International Symposium, LOPSTR 2019, Revised Selected Papers. editor / Maurizio Gabbrielli. Springer, 2020. pp. 3-18 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{097d7e28b0fe4a12bdc3c2eae7ea2220,

title = "On Fixpoint/Iteration/Variant Induction Principles for Proving Total Correctness of Programs with Denotational Semantics",

abstract = "We study partial and total correctness proof methods based on generalized fixpoint/iteration/variant induction principles applied to the denotational semantics of first-order functional and iterative programs.",

keywords = "Denotational semantics, Induction principles, Partial and total correctness, Verification",

author = "Patrick Cousot",

note = "Funding Information: I thank FrancescoRanzato for commetns and suggestions on earlier versionsof the paper. Work supported in part by NSF Grant CCF-1617717.; 29th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2019 ; Conference date: 08-10-2019 Through 10-10-2019",

year = "2020",

doi = "10.1007/978-3-030-45260-5_1",

language = "English (US)",

isbn = "9783030452599",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "3--18",

editor = "Maurizio Gabbrielli",

booktitle = "Logic-Based Program Synthesis and Transformation - 29th International Symposium, LOPSTR 2019, Revised Selected Papers",

}

TY - GEN

T1 - On Fixpoint/Iteration/Variant Induction Principles for Proving Total Correctness of Programs with Denotational Semantics

AU - Cousot, Patrick

N1 - Funding Information: I thank FrancescoRanzato for commetns and suggestions on earlier versionsof the paper. Work supported in part by NSF Grant CCF-1617717.

PY - 2020

Y1 - 2020

N2 - We study partial and total correctness proof methods based on generalized fixpoint/iteration/variant induction principles applied to the denotational semantics of first-order functional and iterative programs.

AB - We study partial and total correctness proof methods based on generalized fixpoint/iteration/variant induction principles applied to the denotational semantics of first-order functional and iterative programs.

KW - Denotational semantics

KW - Induction principles

KW - Partial and total correctness

KW - Verification

UR - http://www.scopus.com/inward/record.url?scp=85084182623&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85084182623&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-45260-5_1

DO - 10.1007/978-3-030-45260-5_1

M3 - Conference contribution

AN - SCOPUS:85084182623

SN - 9783030452599

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 3

EP - 18

BT - Logic-Based Program Synthesis and Transformation - 29th International Symposium, LOPSTR 2019, Revised Selected Papers

A2 - Gabbrielli, Maurizio

PB - Springer

T2 - 29th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2019

Y2 - 8 October 2019 through 10 October 2019

ER -

On Fixpoint/Iteration/Variant Induction Principles for Proving Total Correctness of Programs with Denotational Semantics

Abstract

Publication series

Conference

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this