Fold/Unfold Transformations for Fixpoint Logic

Naoki Kobayashi; Grigory Fedyukovich; Aarti Gupta

doi:10.1007/978-3-030-45237-7_12

Fold/Unfold Transformations for Fixpoint Logic

Naoki Kobayashi, Grigory Fedyukovich, Aarti Gupta

Computer Science

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

6 Scopus citations

Abstract

Fixpoint logics have recently been drawing attention as common foundations for automated program verification. We formalize fold/unfold transformations for fixpoint logic formulas and show how they can be used to enhance a recent fixpoint-logic approach to automated program verification, including automated verification of relational and temporal properties. We have implemented the transformations in a tool and confirmed its effectiveness through experiments.

Original language	English (US)
Title of host publication	Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part II
Editors	Armin Biere, David Parker
Publisher	Springer
Pages	195-214
Number of pages	20
ISBN (Print)	9783030452360
DOIs	https://doi.org/10.1007/978-3-030-45237-7_12
State	Published - 2020
Event	26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020 - Dublin, Ireland Duration: Apr 25 2020 → Apr 30 2020

Publication series

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

Conference

Conference	26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020
Country/Territory	Ireland
City	Dublin
Period	4/25/20 → 4/30/20

All Science Journal Classification (ASJC) codes

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-030-45237-7_12

Cite this

Kobayashi, N., Fedyukovich, G., & Gupta, A. (2020). Fold/Unfold Transformations for Fixpoint Logic. In A. Biere, & D. Parker (Eds.), Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part II (pp. 195-214). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12079 LNCS). Springer. https://doi.org/10.1007/978-3-030-45237-7_12

Kobayashi, Naoki ; Fedyukovich, Grigory ; Gupta, Aarti. / Fold/Unfold Transformations for Fixpoint Logic. Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part II. editor / Armin Biere ; David Parker. Springer, 2020. pp. 195-214 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{285899480bfa451c8380ab9c9cddcf11,

title = "Fold/Unfold Transformations for Fixpoint Logic",

abstract = "Fixpoint logics have recently been drawing attention as common foundations for automated program verification. We formalize fold/unfold transformations for fixpoint logic formulas and show how they can be used to enhance a recent fixpoint-logic approach to automated program verification, including automated verification of relational and temporal properties. We have implemented the transformations in a tool and confirmed its effectiveness through experiments.",

author = "Naoki Kobayashi and Grigory Fedyukovich and Aarti Gupta",

note = "Publisher Copyright: {\textcopyright} 2020, The Author(s).; 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020 ; Conference date: 25-04-2020 Through 30-04-2020",

year = "2020",

doi = "10.1007/978-3-030-45237-7_12",

language = "English (US)",

isbn = "9783030452360",

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

publisher = "Springer",

pages = "195--214",

editor = "Armin Biere and David Parker",

booktitle = "Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part II",

}

Kobayashi, N, Fedyukovich, G & Gupta, A 2020, Fold/Unfold Transformations for Fixpoint Logic. in A Biere & D Parker (eds), Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part II. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 12079 LNCS, Springer, pp. 195-214, 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, 4/25/20. https://doi.org/10.1007/978-3-030-45237-7_12

Fold/Unfold Transformations for Fixpoint Logic. / Kobayashi, Naoki; Fedyukovich, Grigory; Gupta, Aarti.
Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part II. ed. / Armin Biere; David Parker. Springer, 2020. p. 195-214 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12079 LNCS).

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

TY - GEN

T1 - Fold/Unfold Transformations for Fixpoint Logic

AU - Kobayashi, Naoki

AU - Fedyukovich, Grigory

AU - Gupta, Aarti

PY - 2020

Y1 - 2020

N2 - Fixpoint logics have recently been drawing attention as common foundations for automated program verification. We formalize fold/unfold transformations for fixpoint logic formulas and show how they can be used to enhance a recent fixpoint-logic approach to automated program verification, including automated verification of relational and temporal properties. We have implemented the transformations in a tool and confirmed its effectiveness through experiments.

AB - Fixpoint logics have recently been drawing attention as common foundations for automated program verification. We formalize fold/unfold transformations for fixpoint logic formulas and show how they can be used to enhance a recent fixpoint-logic approach to automated program verification, including automated verification of relational and temporal properties. We have implemented the transformations in a tool and confirmed its effectiveness through experiments.

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

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

U2 - 10.1007/978-3-030-45237-7_12

DO - 10.1007/978-3-030-45237-7_12

M3 - Conference contribution

AN - SCOPUS:85083971316

SN - 9783030452360

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

SP - 195

EP - 214

BT - Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part II

A2 - Biere, Armin

A2 - Parker, David

PB - Springer

T2 - 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020

Y2 - 25 April 2020 through 30 April 2020

ER -

Kobayashi N, Fedyukovich G, Gupta A. Fold/Unfold Transformations for Fixpoint Logic. In Biere A, Parker D, editors, Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part II. Springer. 2020. p. 195-214. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-45237-7_12

Fold/Unfold Transformations for Fixpoint Logic

Abstract

Publication series

Conference

All Science Journal Classification (ASJC) codes

Access to Document

Other files and links

Fingerprint

Cite this