Record link: 
http://hdl.handle.net/20.500.12708/228560
-
Title: 
ReVEAL: GNN-Guided Reverse Engineering for Formal Verification of Optimized Multipliers
en
Citation: 
Chen, C., Kaufmann, D., Deng, C., Song, Z., Zhang, H., & Yu, C. (2026). ReVEAL: GNN-Guided Reverse Engineering for Formal Verification of Optimized Multipliers. In S. Junges & G. Katz (Eds.), Tools and Algorithms for the Construction and Analysis of Systems : 32nd International Conference, TACAS 2026, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2026, Turin, Italy, April 11–16, 2026, Proceedings, Part II (pp. 309–333). Springer. https://doi.org/10.1007/978-3-032-22749-2_16
-
Publisher DOI: 
10.1007/978-3-032-22749-2_16
-
Publication Type: 
Inproceedings - Full-Paper Contribution
en
Language: 
English
-
Authors: 
Chen, Chen 
Kaufmann, Daniela 
Deng, Chenhui 
Song, Zhan 
Zhang, Hongce 
Yu, Cunxi 
-
Organisational Unit: 
E192-04 - Forschungsbereich Formal Methods in Systems Engineering 
-
Published in: 
Tools and Algorithms for the Construction and Analysis of Systems : 32nd International Conference, TACAS 2026, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2026, Turin, Italy, April 11–16, 2026, Proceedings, Part II 
-
ISBN: 
978-3-032-22749-2
-
Volume: 
16506
-
DOI of the book: 
10.1007/978-3-032-22749-2
-
Date (published): 
15-Apr-2026
-
Event name: 
32nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2026) 
en
Event date: 
13-Apr-2026 - 16-Apr-2026
-
Event place: 
Italy
-
Number of Pages: 
25
-
Publisher: 
Springer, Cham
-
Peer reviewed: 
Yes
-
Keywords: 
Computer algebra; Formal verification; Graph learning; Multiplier; Reverse engineering; Automated Reasoning; Hardware Verification; Graph Neural Networks
en
Abstract: 
We present ReVEAL, a graph-learning-based method for reverse engineering of multiplier architectures to improve algebraic circuit verification techniques. Our framework leverages structural graph features and learning-driven inference to identify architecture patterns at scale, enabling robust handling of large optimized multipliers. We demonstrate applicability across diverse multiplier benchmarks and show improvements in scalability and accuracy compared to traditional rule-based approaches. The method integrates smoothly with existing verification flows and supports downstream algebraic proof strategies.
en
Project title: 
Wortbasiertes Reasoning mit Computeralgebra und SAT: ESP 666-N (FWF - Österr. Wissenschaftsfonds) 
-
Research Areas: 
Logic and Computation: 100%
-
Science Branch: 
1020 - Informatik: 80%
1010 - Mathematik: 20%
-
Appears in Collections:
Conference Paper

Show full item record

Page view(s)

8
checked on Jun 9, 2026

Google ScholarTM

Check