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	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
Computer Science(all)

Access to Document

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

Fingerprint Dive into the research topics of 'On Fixpoint/Iteration/Variant Induction Principles for Proving Total Correctness of Programs with Denotational Semantics'. Together they form a unique fingerprint.

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)). https://doi.org/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 -