Ternary Simulation as Abstract Interpretation (Work in Progress)

Conference: MBMV 2024 - 27. Workshop
02/14/2024 - 02/15/2024 at Kaiserslautern

Proceedings: ITG-Fb. 314: MBMV 2024

Pages: 4Language: englishTyp: PDF

Authors:
Froleyks, Nils (Johannes Kepler University Linz, Austria)
Yu, Emily (Inst. of Science and Technology Austria, Austria)
Biere, Armin (University of Freiburg, Germany)

Abstract:
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.