Model Checking Regular Language Constraints

TL;DR

This paper introduces Boolean finite automata combined with the IC3 model checking algorithm to efficiently handle regular language constraints, improving performance on complex string membership problems in program analysis.

Contribution

It presents a novel approach using Boolean finite automata and IC3 for efficient regular language constraint solving, addressing performance issues in existing SMT solvers.

Findings

Efficiently solves emptiness and universality problems for Boolean finite automata.

Decides satisfiability of multi-variable string membership problems.

Demonstrates effectiveness on benchmarks and real-world regular expressions.

Abstract

Even the fastest SMT solvers have performance problems with regular expressions from real programs. Because these performance issues often arise from the problem representation (e.g. non-deterministic finite automata get determinized and regular expressions get unrolled), we revisit Boolean finite automata, which allow for the direct and natural representation of any Boolean combination of regular languages. By applying the IC3 model checking algorithm to Boolean finite automata, not only can we efficiently answer emptiness and universality problems, but through an extension, we can decide satisfiability of multiple variable string membership problems. We demonstrate the resulting system's effectiveness on a number of popular benchmarks and regular expressions.