Input-based Three-valued Abstraction Refinement

TL;DR

The paper addresses the limitation that CEGAR cannot verify all $\mu$-calculus properties and that existing TVAR frameworks rely on modal-transition formalisms or are non-monotone, hindering practical usage. It introduces a simulator-based TVAR framework that constructs and refines the abstract state space by input-based splitting, omitting modal transitions to yield a simpler, monotone, and complete approach for $\mu$-calculus properties under existential abstraction. The authors prove soundness, monotonicity, and completeness under mild conditions and implement an instance in the tool machine-check to verify non-trivial machine-code systems. They demonstrate verification of AVR machine-code programs and identify a bug using a non-linear-time property not verifiable by CEGAR, marking the first practical TVAR application to machine-code verification. The work suggests a scalable, programmable path for hardware verification with full $\mu$-calculus reach.

Abstract

Unlike Counterexample-Guided Abstraction Refinement (CEGAR), Three-Valued Abstraction Refinement (TVAR) is able to verify all properties of the mu-calculus. We present a novel algorithmic framework for TVAR that employs a simulator-like approach to build and refine the abstract state space with input-based splitting. This leads to a state space formalism that is much simpler than in previous TVAR frameworks, which use modal transitions. We implemented the framework in our open-source tool machine-check and verified properties of machine-code systems for the AVR architecture, showing the ability to verify systems and mu-calculus properties not verifiable by naive model checking or CEGAR, respectively. This is the first practical use of TVAR for machine-code verification.