Ternary Simulation as Abstract Interpretation

Description

We introduce a formalization of ternary simulation as abstract interpretation along with a widening operator to speed up convergence. With the same goal, we present a subsumption algorithm that can determine termination earlier than the usual approach using hash sets. Additionally, we introduce a narrowing operator that utilizes recent advances in backbone extraction, allowing to increase the overapproximation precision in simulation at any time. The experiments evaluate the presented techniques in the context of hardware model checking.

Period	15 Feb 2024
Event title	Methods and Description Languages for Modelling and Verification of Circuits and Systems 2024
Event type	Conference
Location	GermanyShow on map