On computing the fixpoint of a set of boolean equations
Viktor Kuncak, K. Rustan M. Leino
TL;DR
This paper introduces an efficient method for computing the least fixpoint of boolean equations, significantly reducing computation time compared to iterative evaluation.
Contribution
It proposes a novel approach for fixpoint computation that shortens the process for boolean systems.
Findings
The method reduces computation time substantially.
It guarantees correct fixpoint calculation.
Applicable to large boolean systems.
Abstract
This paper presents a method for computing a least fixpoint of a system of equations over booleans. The resulting computation can be significantly shorter than the result of iteratively evaluating the entire system until a fixpoint is reached.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Polynomial and algebraic computation · Advanced Optimization Algorithms Research