Fold/Unfold Transformations for Fixpoint Logic

DOI10.1007/978-3-030-45237-7_12zbMath1483.68196OpenAlexW3016484846MaRDI QIDQ5164174

Aarti Gupta, Grigory Fedyukovich, Naoki Kobayashi

Publication date: 10 November 2021

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-030-45237-7_12

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (3)

Verifying Catamorphism-Based Contracts using Constrained Horn Clauses ⋮ Asynchronous unfold/fold transformation for fixpoint logic ⋮ Temporal refinements for guarded recursive types

Cites Work

• Unnamed Item
• Unnamed Item
• SMT-based model checking for recursive programs
• Transformations of CLP modules
• Invariants for parameterised Boolean equation systems
• Equivalence-preserving first-order unfold/fold transformation systems
• On automation of \(\mathsf{CTL}^*\) verification for infinite-state systems
• Fairness modulo theory: a new approach to LTL software model checking
• Automating induction for solving Horn clauses
• Higher-order program verification via HFL model checking
• Parameterised Boolean equation systems
• Temporal verification of higher-order functional programs
• Proof Graphs for Parameterised Boolean Equation Systems
• Horn Clause Solvers for Program Verification
• Equivalence Checking for Infinite Systems Using Parameterized Boolean Equation Systems
• A Transformation System for Developing Recursive Programs
• Solving Horn Clauses on Inductive Data Types Without Induction
• Synchronizing Constrained Horn Clauses
• A Fixpoint Logic and Dependent Effects for Temporal Property Verification
• μ-definable sets of integers
• Making prophecies with decision predicates
• Syntax-guided termination analysis
• Abstract interpretation of CTL properties
• HoIce: an ICE-based non-linear Horn clause solver

This page was built for publication: Fold/Unfold Transformations for Fixpoint Logic