Synthesizing Modular Invariants for Synchronous Code

TL;DR

This paper presents new methods for synthesizing modular invariants for synchronous code, enabling better analysis and transformation, using property-directed reachability and invariant minimization techniques.

Contribution

It introduces two novel techniques for generating modular invariants for Lustre code, one direct and one from monolithic invariants, enhancing analysis capabilities.

Findings

Two techniques successfully generate modular invariants for Lustre code.

Invariant minimization improves efficiency of analysis.

Methods leverage property-directed reachability for synthesis.

Abstract

In this paper, we explore different techniques to synthesize modular invariants for synchronous code encoded as Horn clauses. Modular invariants are a set of formulas that characterizes the validity of predicates. They are very useful for different aspects of analysis, synthesis, testing and program transformation. We describe two techniques to generate modular invariants for code written in the synchronous dataflow language Lustre. The first technique directly encodes the synchronous code in a modular fashion. While in the second technique, we synthesize modular invariants starting from a monolithic invariant. Both techniques, take advantage of analysis techniques based on property-directed reachability. We also describe a technique to minimize the synthesized invariants.