Fold/Unfold Transformations for Fixpoint Logic

Naoki Kobayashi, Grigory Fedyukovich, Aarti Gupta

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 languageEnglish (US)
Title of host publicationTools 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
EditorsArmin Biere, David Parker
PublisherSpringer
Pages195-214
Number of pages20
ISBN (Print)9783030452360
DOIs
StatePublished - 2020
Event26th 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 2020Apr 30 2020

Publication series

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

Conference

Conference26th 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
CountryIreland
CityDublin
Period4/25/204/30/20

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Fold/Unfold Transformations for Fixpoint Logic'. Together they form a unique fingerprint.

Cite this