Lattice based Least Fixed Point Logic

TL;DR

This paper introduces LLFP, a logic formalism for static analysis over arbitrary complete lattices, with guarantees of unique solutions and an algorithm for computing least models, enhancing flexibility over previous powerset-based approaches.

Contribution

It presents LLFP, a novel logic that extends static analysis capabilities to general lattices, along with theoretical guarantees and a solving algorithm.

Findings

Guarantees a unique least solution via Moore Family theorem

Develops an algorithm to compute the least model of LLFP formulas

Extends static analysis formalism beyond powerset domains

Abstract

As software systems become more complex, there is an increasing need for new static analyses. Thanks to the declarative style, logic programming is an attractive formalism for specifying them. However, prior work on using logic programming for static analysis focused on analyses defined over some powerset domain, which is quite limiting. In this paper we present a logic that lifts this restriction, called Lattice based Least Fixed Point Logic (LLFP), that allows interpretations over any complete lattice satisfying Ascending Chain Condition. The main theoretical contribution is a Moore Family result that guarantees that there always is a unique least solution for a given problem. Another contribution is the development of solving algorithm that computes the least model of LLFP formulae guaranteed by the Moore Family result.