Layered Fixed Point Logic

TL;DR

This paper introduces a novel layered fixed point logic that supports both inductive and co-inductive reasoning, enabling advanced static analysis and verification techniques with proven complexity bounds.

Contribution

It presents a new logic framework with theoretical guarantees and demonstrates its applicability across static analysis, constraint satisfaction, and model checking.

Findings

Supports inductive and co-inductive specifications

Provides a Moore Family theoretical result

Achieves worst case time complexity comparable to classical methods

Abstract

We present a logic for the specification of static analysis problems that goes beyond the logics traditionally used. Its most prominent feature is the direct support for both inductive computations of behaviors as well as co-inductive specifications of properties. Two main theoretical contributions are a Moore Family result and a parametrized worst case time complexity result. We show that the logic and the associated solver can be used for rapid prototyping and illustrate a wide variety of applications within Static Analysis, Constraint Satisfaction Problems and Model Checking. In all cases the complexity result specializes to the worst case time complexity of the classical methods.