Input-based Three-valued Abstraction Refinement

TL;DR

This paper introduces a novel input-based three-valued abstraction refinement framework that simplifies state space formalism and enables practical machine-code verification of mu-calculus properties, surpassing traditional CEGAR methods.

Contribution

The paper presents a new algorithmic framework for TVAR using input-based splitting, making the approach more practical and effective for machine-code verification.

Findings

Successfully verified properties of machine-code systems for AVR architecture.

Demonstrated ability to verify mu-calculus properties not accessible by naive model checking.

First practical application of TVAR in machine-code verification.

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.