{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,15]],"date-time":"2025-06-15T04:04:25Z","timestamp":1749960265253,"version":"3.41.0"},"reference-count":72,"publisher":"Association for Computing Machinery (ACM)","issue":"3","funder":[{"name":"Strategic Priority Research Program of the Chinese Academy of Sciences","award":["XDA0320000 and XDA0320300"],"award-info":[{"award-number":["XDA0320000 and XDA0320300"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2025,9,30]]},"abstract":"<jats:p>This article proposes a term-level generalized symbolic trajectory evaluation (GSTE) to tackle parameterized hardware verification. We develop a theorem-proving technique for parameterized GSTE verification. In our technique, a constraint is associated with a node in GSTE graphs to specify reachable states. Generalized inductive relations between nodes of GSTE graphs are formulated; instantaneous implications are formalized on the edges of GSTE graphs. Based on this formalization, parameterized GSTE are verified. We moreover formalize our techniques in Isabelle. Furthermore, once a parametrized design is verified at the term level, we can convert the generally parameterized invariants into concrete ones, which can be used to verify a synthesized netlist of an instance of the parameterized design at the Boolean level. We demonstrate the effectiveness of our techniques in case studies. Interestingly, subtleties between different implementations of FIFOs are discovered by our parameterized verification, although these circuits have been extensively studied previously.<\/jats:p>","DOI":"10.1145\/3716828","type":"journal-article","created":{"date-parts":[[2025,2,25]],"date-time":"2025-02-25T09:42:26Z","timestamp":1740476546000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Parameterized Hardware Verification Through A Term-level Generalized Symbolic Trajectory Evaluation And Its Linkage With Concrete Hardware Verification At Netlist Level"],"prefix":"10.1145","volume":"37","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2817-063X","authenticated-orcid":false,"given":"Yongjian","family":"Li","sequence":"first","affiliation":[{"name":"Institute of Software Chinese Academy of Sciences, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-3602-1941","authenticated-orcid":false,"given":"Zhenghai","family":"Cai","sequence":"additional","affiliation":[{"name":"East China Normal University Shanghai Key Laboratory of Trustworthy Computing, Shanghai, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5757-545X","authenticated-orcid":false,"given":"Bow-Yaw","family":"Wang","sequence":"additional","affiliation":[{"name":"Institute of Information Science Academia Sinica, Taipei China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9561-7403","authenticated-orcid":false,"given":"Yongxin","family":"Zhao","sequence":"additional","affiliation":[{"name":"East China Normal University Shanghai Key Laboratory of Trustworthy Computing, Shanghai, China"}]}],"member":"320","published-online":{"date-parts":[[2025,6,14]]},"reference":[{"key":"e_1_3_2_2_2","first-page":"300","volume-title":"Proceedings of the 3rd International Conference on Formal Methods in Computer-Aided Design (FMCAD 2000) (Austin, TX, November 1\u20133, 2000)","author":"Aagaard Mark D.","year":"2000","unstructured":"Mark D. Aagaard, Robert B. Jones, Thomas F. Melham, John W. O\u2019Leary, and Carl-Johan H. Seger. 2000. A methodology for large-scale hardware verification. In Proceedings of the 3rd International Conference on Formal Methods in Computer-Aided Design (FMCAD 2000) (Austin, TX, November 1\u20133, 2000). Springer, 300\u2013319."},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/309847.309968"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1109\/FAMCAD.2007.27"},{"volume-title":"reFLect: Intel\u2019s Next Generation Formal Tools Environment (2003 ed.)","key":"e_1_3_2_5_2","unstructured":"An Introductory Tutorial to Open Binary reFLectf or Academic Research. Intel Corporation [n.d.]. reFLect: Intel\u2019s Next Generation Formal Tools Environment (2003 ed.). An Introductory Tutorial to Open Binary reFLectf or Academic Research. Intel Corporation."},{"key":"e_1_3_2_6_2","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1007\/3-540-44585-4_19","volume-title":"Proceedings of the International Conference on Computer Aided Verification","author":"Arons Tamarah","year":"2001","unstructured":"Tamarah Arons, Amir Pnueli, Sitvanit Ruah, Ying Xu, and Lenore Zuck. 2001. Parameterized verification with automatically computed inductive assertions?. In Proceedings of the International Conference on Computer Aided Verification. Springer, 221\u2013234."},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/2228360.2228584"},{"key":"e_1_3_2_8_2","first-page":"197","article-title":"Berkeley logic interchange format (BLIF)","volume":"2","author":"Berkeley UoC","year":"1992","unstructured":"UoC Berkeley. 1992. Berkeley logic interchange format (BLIF). Oct Tools Distribution 2 (1992), 197\u2013247.","journal-title":"Oct Tools Distribution"},{"key":"e_1_3_2_9_2","first-page":"1","volume-title":"Proceedings of the International Conference on Theory and Applications of Satisfiability Testing","author":"Bradley Aaron R.","year":"2012","unstructured":"Aaron R. Bradley. 2012. Understanding IC3. In Proceedings of the International Conference on Theory and Applications of Satisfiability Testing. Springer, 1\u201314."},{"key":"e_1_3_2_10_2","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/978-3-642-39799-8_14","volume-title":"Computer Aided Verification","author":"Braibant Thomas","year":"2013","unstructured":"Thomas Braibant and Adam Chlipala. 2013. Formal verification of hardware synthesis. In Computer Aided Verification, Natasha Sharygina and Helmut Veith (Eds.). Springer Berlin, Berlin,, 213\u2013228."},{"key":"e_1_3_2_11_2","first-page":"428","volume-title":"Proceedings of the 8th International Conference on Computer Aided Verification (CAV \u201996).","author":"Brayton Robert","year":"1996","unstructured":"Robert Brayton, Gary D. Hachtel, Alberto Sangiovanni-Vincentelli, Fabio Somenzi, Adnan Aziz, Szu tsung Cheng, and Stephen Edwards. 1996. VIS: A system for verification and synthesis. In Proceedings of the 8th International Conference on Computer Aided Verification (CAV \u201996).. Springer-Verlag, 428\u2013432."},{"key":"e_1_3_2_12_2","unstructured":"Zhenghai Cai and Yongjian Li. [n.d.]. WCSTE model checker. https:\/\/github.com\/cccccc96\/WCSTE"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_8"},{"key":"e_1_3_2_14_2","volume-title":"A General Compositional Approach to Verifying Hierarchical Cache Coherence Protocols","author":"Chen Xiaofang","year":"2006","unstructured":"Xiaofang Chen and Ganesh Gopalakrishnan. 2006. A General Compositional Approach to Verifying Hierarchical Cache Coherence Protocols. Technical Report. Technical Report UUCS-06-014, School of Computing, University of Utah, Salt Lake City, UT, November 26."},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1109\/FAMCAD.2007.11"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/1391469.1391508"},{"key":"e_1_3_2_17_2","doi-asserted-by":"crossref","unstructured":"Ching-Tsun Chou Phanindra K. Mannava and Seungjoon Park. 2004. A simple method for parameterized verification of cache coherence protocols. In Proceedings of the Formal Methods in Computer Aided Design (FMCAD\u201904) Vol. 4. Springer 382\u2013398.","DOI":"10.1007\/978-3-540-30494-4_27"},{"key":"e_1_3_2_18_2","article-title":"A faithful semantics for generalised symbolic trajectory evaluation","volume":"5","author":"Claessen Koen","year":"2009","unstructured":"Koen Claessen and Jan-Willem Roorda. 2009. A faithful semantics for generalised symbolic trajectory evaluation. Logical Methods in Computer Science 5 (2009).","journal-title":"Logical Methods in Computer Science"},{"key":"e_1_3_2_19_2","first-page":"718","volume-title":"Proceedings of CAV","author":"Conchon Sylvain","year":"2012","unstructured":"Sylvain Conchon, Amit Goel, Sava Krstic, Alain Mebsout, and Fatiha Za\u0131di. 2012. Cubicle: A parallel SMT-based model checker for parameterized systems. In Proceedings of CAV. Springer, 718\u2013724."},{"key":"e_1_3_2_20_2","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1109\/FMCAD.2013.6679392","volume-title":"Proceedings of the Formal Methods in Computer Aided Design (FMCAD\u201913),","author":"Conchon Sylvain","year":"2013","unstructured":"Sylvain Conchon, Amit Goel, Sava Krsti\u0107, Alain Mebsout, and Fatiha Za\u00efdi. 2013. Invariants for finite instances and beyond. In Proceedings of the Formal Methods in Computer Aided Design (FMCAD\u201913),. IEEE, 61\u201368."},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_22_2","first-page":"1","volume-title":"Proceedings of the 2006 10th International Conference on Computer Supported Cooperative Work in Design","author":"Deng Shujun","year":"2006","unstructured":"Shujun Deng, Weimin Wu, and Jinian Bian. 2006. Cooperative bounded model checking using STE and hybrid three-valued SAT solving. In Proceedings of the 2006 10th International Conference on Computer Supported Cooperative Work in Design. IEEE, 1\u20137."},{"issue":"2","key":"e_1_3_2_23_2","first-page":"1","article-title":"The YICES SMT solver","volume":"2","author":"Dutertre Bruno","year":"2006","unstructured":"Bruno Dutertre and Leonardo De Moura. 2006. The YICES SMT solver. Tool Paper at http:\/\/yices. csl. sri. com\/tool-paper. pdf 2, 2 (2006), 1\u20132.","journal-title":"Tool Paper at http:\/\/yices. csl. sri. com\/tool-paper. pdf"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-35355-0_2"},{"key":"e_1_3_2_25_2","doi-asserted-by":"crossref","first-page":"618","DOI":"10.23919\/DATE.2019.8715289","volume-title":"Proceedings of the 2019 Design, Automation & Test in Europe Conference & Exhibition (DATE\u201919)","author":"Goel Aman","year":"2019","unstructured":"Aman Goel and Karem Sakallah. 2019. Empirical evaluation of IC3-based model checking techniques on verilog RTL designs. In Proceedings of the 2019 Design, Automation & Test in Europe Conference & Exhibition (DATE\u201919). IEEE, 618\u2013621."},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-76384-8_9"},{"key":"e_1_3_2_27_2","unstructured":"Mike Gordon. 2011. Directions in Formal and Semi-Formal Verification. http:\/\/www.cl.cam.ac.uk\/mjcg\/Research00\/"},{"key":"e_1_3_2_28_2","first-page":"115","volume-title":"Proceedings of the 18th USENIX Symposium on Networked Systems Design and Implementation (NSDI\u201921)","author":"Hance Travis","year":"2021","unstructured":"Travis Hance, Marijn Heule, Ruben Martins, and Bryan Parno. 2021. Finding invariants of distributed systems: It\u2019s a small (enough) world after all. In Proceedings of the 18th USENIX Symposium on Networked Systems Design and Implementation (NSDI\u201921). USENIX Association, 115\u2013131. https:\/\/www.usenix.org\/conference\/nsdi21\/presentation\/hance"},{"key":"e_1_3_2_29_2","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1109\/FMCAD.2013.6679405","volume-title":"Proceedings of the 2013 Formal Methods in Computer-Aided Design","author":"Hassan Zyad","year":"2013","unstructured":"Zyad Hassan, Aaron R. Bradley, and Fabio Somenzi. 2013. Better generalization in IC3. In Proceedings of the 2013 Formal Methods in Computer-Aided Design. IEEE, 157\u2013164."},{"key":"e_1_3_2_30_2","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/3-540-63475-4_1","article-title":"Symbolic trajectory evaluation","author":"Hazelhurst Scott","year":"1997","unstructured":"Scott Hazelhurst and Carl-Johan H. Seger. 1997. Symbolic trajectory evaluation. Formal Hardware Verification (1997), 3\u201378.","journal-title":"Formal Hardware Verification"},{"key":"e_1_3_2_31_2","unstructured":"S. Ja\u015bkowski. 1934. On the Rules of Suppositions in Formal Logic. Nak\u0142adem Seminarjum Filozoficznego Wydzia\u0142u Matematyczno-Przyrodniczego Uniwersytetu Warszawskiego. https:\/\/books.google.com.hk\/books?id=6w0vRAAACAAJ"},{"key":"e_1_3_2_32_2","volume-title":"Applications of symbolic simulation to the formal verification of microprocessors","author":"Jones Robert Brent","year":"1999","unstructured":"Robert Brent Jones. 1999. Applications of symbolic simulation to the formal verification of microprocessors. Ph. D. Dissertation. Stanford, CA,. Advisor(s) Dill, David L. AAI9958122."},{"issue":"4","key":"e_1_3_2_33_2","doi-asserted-by":"crossref","first-page":"16","DOI":"10.1109\/54.936245","article-title":"Practical formal verification in microprocessor design","volume":"18","author":"Jones Robert B.","year":"2001","unstructured":"Robert B. Jones, John W. O\u2019Leary, C.-J. H. Seger, Mark D. Aagaard, and Thomas F. Melham. 2001. Practical formal verification in microprocessor design. IEEE Design & Test of Computers 18, 4 (2001), 16\u201325.","journal-title":"IEEE Design & Test of Computers"},{"key":"e_1_3_2_34_2","doi-asserted-by":"crossref","first-page":"108","DOI":"10.1109\/FMCAD.2009.5351133","volume-title":"Proceedings of the 2009 Formal Methods in Computer-Aided Design","author":"Khasidashvili Zurab","year":"2009","unstructured":"Zurab Khasidashvili, Gavriel Gavrielov, and Tom Melham. 2009. Assume-guarantee validation for STE properties within an SVA environment. In Proceedings of the 2009 Formal Methods in Computer-Aided Design. IEEE, 108\u2013115."},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386018"},{"key":"e_1_3_2_36_2","article-title":"Parameterized system verification with guard strengthening and parameter abstraction","author":"Krstic Sava","year":"2005","unstructured":"Sava Krstic. 2005. Parameterized system verification with guard strengthening and parameter abstraction. Automated Verification of Infinite State Systems (2005).","journal-title":"Automated Verification of Infinite State Systems"},{"key":"e_1_3_2_37_2","first-page":"42","volume-title":"Proceedings of the 33rd ACM Symposium on Principles of Programming Languages","author":"Leroy Xavier","year":"2006","unstructured":"Xavier Leroy. 2006. Formal certification of a compiler back-end, or: Programming a compiler with a proof assistant. In Proceedings of the 33rd ACM Symposium on Principles of Programming Languages. ACM, 42\u201354. http:\/\/xavierleroy.org\/publi\/compiler-certif.pdf"},{"key":"e_1_3_2_38_2","unstructured":"Y. Li. [n.d.]. Parameterized Generalized Symbolic Trajetory Eveluation. https:\/\/github.com\/raphelIos\/parametricGste"},{"key":"e_1_3_2_39_2","unstructured":"YongJian Li and Zhenghai Cai. [n.d.]. A Linkage with GSTE at Boolean Level.https:\/\/github.com\/LinkageWithGSTE\/A-Linkage-With-GSTE-At-Boolean-Level"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD50377.2020.00073"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/3232164"},{"key":"e_1_3_2_42_2","first-page":"403","volume-title":"Formal Methods and Software Engineering","author":"Li Yongjian","year":"2019","unstructured":"Yongjian Li and Bow-yaw Wang. 2019. Parameterized hardware verification through a term-level generalized symbolic trajectory evaluation. In Formal Methods and Software Engineering, Yamine Ait-Ameur and Shengchao Qin (Eds.). Springer International Publishing, Cham, 403\u2013419."},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/bxs161"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/3437992.3439916"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2007.371252"},{"key":"e_1_3_2_46_2","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1007\/3-540-44798-9_17","volume-title":"Advanced Research Working Conference on Correct Hardware Design and Verification Methods","author":"McMillan Kenneth L.","year":"2001","unstructured":"Kenneth L. McMillan. 2001. Parameterized verification of the FLASH cache coherence protocol by compositional model checking. In Advanced Research Working Conference on Correct Hardware Design and Verification Methods. Springer, 179\u2013195."},{"key":"e_1_3_2_47_2","first-page":"36","volume-title":"Proceedings of the 4th International Conference on Integrated Formal Methods: (IFM 2004), (Canterbury, UK, April 4\u20137, 2004).","author":"Melham Tom","year":"2004","unstructured":"Tom Melham. 2004. Integrating model checking and theorem proving in a reflective functional language. In Proceedings of the 4th International Conference on Integrated Formal Methods: (IFM 2004), (Canterbury, UK, April 4\u20137, 2004).. Springer, 36\u201339."},{"key":"e_1_3_2_48_2","first-page":"831","article-title":"Symbolic trajectory evaluation","author":"Melham Tom","year":"2018","unstructured":"Tom Melham. 2018. Symbolic trajectory evaluation. Handbook of Model Checking (2018), 831\u2013870.","journal-title":"Handbook of Model Checking"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.3233\/SAT190101"},{"key":"e_1_3_2_50_2","first-page":"69","volume-title":"Proceedings of the 2nd ACM and IEEE International Conference on Formal Methods and Models for Co-Design, 2004. MEMOCODE\u201904.","author":"Nikhil Rishiyur","year":"2004","unstructured":"Rishiyur Nikhil. 2004. Bluespec System Verilog: Efficient, correct RTL from high level specifications. In Proceedings of the 2nd ACM and IEEE International Conference on Formal Methods and Models for Co-Design, 2004. MEMOCODE\u201904. IEEE, 69\u201370."},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.5555\/1791547"},{"key":"e_1_3_2_52_2","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1109\/FMCAD.2013.6679397","volume-title":"Proceedings of the 2013 Formal Methods in Computer-Aided Design","author":"O\u2019Leary John","year":"2013","unstructured":"John O\u2019Leary, Roope Kaivola, and Tom Melham. 2013. Relational STE and theorem proving for formal verification of industrial circuit designs. In Proceedings of the 2013 Formal Methods in Computer-Aided Design. IEEE, 97\u2013104."},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.1995.528929"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1145\/266021.266056"},{"key":"e_1_3_2_55_2","first-page":"82","volume-title":"Proceedings of TACAS","volume":"1","author":"Pnueli Amir","year":"2001","unstructured":"Amir Pnueli, Sitvanit Ruah, and Lenore Zuck. 2001. Automatic deductive verification with invisible invariants. In Proceedings of TACAS, Vol. 1. Springer, 82\u201397."},{"key":"e_1_3_2_56_2","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/11817963_19","volume-title":"Proceedings of the 18th International Conference on Computer Aided Verification: , (CAV 2006) (Seattle, WA, USA, August 17\u201320).","author":"Roorda Jan-Willem","year":"2006","unstructured":"Jan-Willem Roorda and Koen Claessen. 2006. SAT-based assistance in abstraction refinement for symbolic trajectory evaluation. In Proceedings of the 18th International Conference on Computer Aided Verification: , (CAV 2006) (Seattle, WA, USA, August 17\u201320).. Springer, 175\u2013189."},{"key":"e_1_3_2_57_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01383966"},{"key":"e_1_3_2_58_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2005.850814"},{"key":"e_1_3_2_59_2","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2011.5970515"},{"key":"e_1_3_2_60_2","volume-title":"Specifying Properties of Generalized Symbolic Trajectory Evaluation","author":"Smith Edward","year":"2008","unstructured":"Edward Smith. 2008. Specifying Properties of Generalized Symbolic Trajectory Evaluation. Ph. D. Dissertation. University of Oxford."},{"key":"e_1_3_2_61_2","first-page":"10","volume-title":"Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design","author":"Talupur Murali","year":"2008","unstructured":"Murali Talupur and Mark R. Tuttle. 2008. Going with the flow: Parameterized verification using message flows. In Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design. IEEE Press, 10."},{"volume-title":"Forte\/fl User Guide (2003 ed.)","key":"e_1_3_2_62_2","unstructured":"Technical Publications and Training, Intel Corporation [n.d.]. Forte\/fl User Guide (2003 ed.). Technical Publications and Training, Intel Corporation."},{"key":"e_1_3_2_63_2","doi-asserted-by":"publisher","DOI":"10.5555\/1502144"},{"key":"e_1_3_2_64_2","first-page":"113","article-title":"A technique for invariant generation","author":"Tiwari Ashish","year":"2001","unstructured":"Ashish Tiwari, Harald Rue\u00df, Hassen Sa\u00efdi, and Natarajan Shankar. 2001. A technique for invariant generation. Tools and Algorithms for the Construction and Analysis of Systems (2001), 113\u2013127.","journal-title":"Tools and Algorithms for the Construction and Analysis of Systems"},{"key":"e_1_3_2_65_2","unstructured":"Clifford Wolf. 2016. Yosys Open Synthesis Suite."},{"key":"e_1_3_2_66_2","doi-asserted-by":"publisher","DOI":"10.1145\/774572.774651"},{"volume-title":"Generalized Symbolic Trajectory Evaluation","author":"Yang Jin","key":"e_1_3_2_67_2","unstructured":"Jin Yang and Carl-Johan H. Seger. [n.d.]. Generalized Symbolic Trajectory Evaluation. Intel SCL Technical Report."},{"key":"e_1_3_2_68_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.2001.955052"},{"key":"e_1_3_2_69_2","first-page":"70","volume-title":"Proceedings of the International Conference on Formal Methods in Computer-Aided Design","author":"Yang Jin","year":"2002","unstructured":"Jin Yang and Carl-Johan H. Seger. 2002. Generalized symbolic trajectory evaluation\u2013abstraction in action. In Proceedings of the International Conference on Formal Methods in Computer-Aided Design. Springer, 70\u201387."},{"issue":"3","key":"e_1_3_2_70_2","doi-asserted-by":"crossref","first-page":"345","DOI":"10.1109\/TVLSI.2003.812320","article-title":"Introduction to generalized symbolic trajectory evaluation","volume":"11","author":"Yang Jin","year":"2003","unstructured":"Jin Yang and Carl-Johan H. Seger. 2003. Introduction to generalized symbolic trajectory evaluation. IEEE Trans. VLSI Syst. 11, 3 (2003), 345\u2013353.","journal-title":"IEEE Trans. VLSI Syst."},{"key":"e_1_3_2_71_2","first-page":"485","volume-title":"Proceedings of the16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2022) (Carlsbad, CA, USA, July 11\u201313, 2022","author":"Yao Jianan","year":"2022","unstructured":"Jianan Yao, Runzhou Tao, Ronghui Gu, and Jason Nieh. 2022. DuoAI: Fast, automated inference of inductive invariants for verifying distributed protocols. In Proceedings of the16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2022) (Carlsbad, CA, USA, July 11\u201313, 2022) Marcos K. Aguilera and Hakim Weatherspoon (Eds.). USENIX Association, 485\u2013501. https:\/\/www.usenix.org\/conference\/osdi22\/presentation\/yao"},{"key":"e_1_3_2_72_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632877"},{"key":"e_1_3_2_73_2","first-page":"405","volume-title":"Proceedings of the 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI\u201921)","author":"Yao Jianan","year":"2021","unstructured":"Jianan Yao, Runzhou Tao, Ronghui Gu, Jason Nieh, Suman Jana, and Gabriel Ryan. 2021. DistAI: Data-drivegn automated invariant learning for distributed protocols. In Proceedings of the 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI\u201921). USENIX Association, 405\u2013421. https:\/\/www.usenix.org\/conference\/osdi21\/presentation\/yao"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3716828","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,14]],"date-time":"2025-06-14T12:01:45Z","timestamp":1749902505000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3716828"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,14]]},"references-count":72,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2025,9,30]]}},"alternative-id":["10.1145\/3716828"],"URL":"https:\/\/doi.org\/10.1145\/3716828","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2025,6,14]]},"assertion":[{"value":"2023-09-15","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-02-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-14","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}