Ternary simulation as abstract interpretation (Work in Progress)
Froleyks N, Yu Z, Biere A. Ternary simulation as abstract interpretation (Work in Progress). 27th Workshop on Methods and Description Languages for Modeling and Verification of Circuits and Systems. MBMV: Methods and Description Languages for Modeling and Verification of Circuits and Systems, 148–151.
Download
No fulltext has been uploaded. References only!
Conference Paper
| Submitted
| English
Scopus indexed
Author
Froleyks, Nils;
Yu, ZhengqiISTA;
Biere, Armin
Department
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.
Publishing Year
Date Published
2024-02-01
Proceedings Title
27th Workshop on Methods and Description Languages for Modeling and Verification of Circuits and Systems
Acknowledgement
This work is supported by the Austrian Science Fund (FWF) under the project W1255-N23, the LIT AI Lab funded by the State of Upper Austria, the ERC-2020-AdG 101020093 and by a gift from Intel Corporation.
Page
148-151
Conference
MBMV: Methods and Description Languages for Modeling and Verification of Circuits and Systems
Conference Location
Kaiserslautern, Germany
Conference Date
2024-02-14 – 2024-02-15
ISBN
IST-REx-ID
Cite this
Froleyks N, Yu Z, Biere A. Ternary simulation as abstract interpretation (Work in Progress). In: 27th Workshop on Methods and Description Languages for Modeling and Verification of Circuits and Systems. ; :148-151.
Froleyks, N., Yu, Z., & Biere, A. (n.d.). Ternary simulation as abstract interpretation (Work in Progress). In 27th Workshop on Methods and Description Languages for Modeling and Verification of Circuits and Systems (pp. 148–151). Kaiserslautern, Germany.
Froleyks, Nils, Zhengqi Yu, and Armin Biere. “Ternary Simulation as Abstract Interpretation (Work in Progress).” In 27th Workshop on Methods and Description Languages for Modeling and Verification of Circuits and Systems, 148–51, n.d.
N. Froleyks, Z. Yu, and A. Biere, “Ternary simulation as abstract interpretation (Work in Progress),” in 27th Workshop on Methods and Description Languages for Modeling and Verification of Circuits and Systems, Kaiserslautern, Germany, pp. 148–151.
Froleyks N, Yu Z, Biere A. Ternary simulation as abstract interpretation (Work in Progress). 27th Workshop on Methods and Description Languages for Modeling and Verification of Circuits and Systems. MBMV: Methods and Description Languages for Modeling and Verification of Circuits and Systems, 148–151.
Froleyks, Nils, et al. “Ternary Simulation as Abstract Interpretation (Work in Progress).” 27th Workshop on Methods and Description Languages for Modeling and Verification of Circuits and Systems, pp. 148–51.
Google Scholar
ISBN Search