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.