[1] |
Wang Ji,Zhan Nai-jun,Feng Xin-yu,et al.Overview of formal methods[J].Journal of Software,2019,30(1):33-61.(in Chinese)
|
[2] |
Mukherjee R,Tautschnig M,Kroening D.v2c—A Verilog to C translator[C]∥Proc of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems,2016:580-586.
|
[3] |
Mukherjee R.Precise abstract interpretation of hardware designs[D].Oxford:University of Oxford,2018.
|
[4] |
Noonan R E.An algorithm for generating abstract syntax trees[J].Computer Languages,1985,10(3-4):225-236.
|
[5] |
Cousot P, Cousot R. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[C]∥Proc of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, 1977:238-252.
|
[6] |
Fan G,Chen T,Yin B,et al.Static bound analysis of dynamically allocated resources for C programs[C]∥Proc of the 2021 IEEE 32nd International Symposium on Software Reliability Engineering,2021:390-400.
|
[7] |
Kirchner F,Kosmatov N,Prevosto V,et al.Frama-C:A software analysis perspective[J].Formal Aspects of Computing,2015,27(3):573-609.
|
[8] |
Jung Y,Yi K.Practical memory leak detector based on parameterized procedural summaries[C]∥Proc of the 7th International Symposium on Memory Management,2008:131-140.
|
[9] |
Clarke E M, Emerson E A. Design and synthesis of synchronization skeletons using branching time temporal logic[C]∥Proc of Workshop on Logic of Programs, 1981:52-71.
|
[10] |
Beyer D,Keremoglu M E.CPAchecker:A tool for configurable software verification[C]∥Proc of the 23rd International Conference on Computer Aided Verification,2011:184-190.
|
[11] |
Kroening D, Tautschnig M.CBMC—C bounded model checker—(Competition Contribution)[C]∥Porc of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems,2014:389-391.
|
[12] |
King J C.Symbolic execution and program testing[J].Communications of the ACM,1976,19(7):385-394.
|
[13] |
Li Y,Albarghouthi A,Kincaid Z,et al.Symbolic optimization with SMT solvers[C]∥Proc of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages,2014:607-618.
|
[14] |
Cadar C,Dunbar D,Engler D. KLEE:Unassisted and automatic generation of high-coverage tests for complex systems programs[C]∥Proc of the 8th USENIX Conference on Operating Systems Design and Implementation,2008:209-224.
|
[15] |
Burnim J, Sen K. Heuristics for scalable dynamic test generation[C]∥Proc of the 23rd IEEE/ACM International Conference on Automated Software Engineering,2008:443-446.
|
[16] |
Ma K K, Phang K Y,Foster J S,et al.Directed symbolic execution[C]∥Proc of the 18th International Symposium on Static Analysis,2011:95-111.
|
[17] |
Kroening D,Purandare M.EBMC[EB/OL].[2023-01-15]. http://www.cprover.org/ebmc.
|
[18] |
Pedroni V A.Circuit design with VHDL[M].3rd ed.Cambridge:MIT Press,2020.
|
[19] |
Panda P R.SystemC:A modeling platform supporting multiple design abstractions[C]∥Proc of the 14th International Symposium on Systems Synthesis,2001:75-80.
|
[20] |
Huang C,Gao H,Zhong Y,et al.A high-performance bidirectional compiler for conversion between system C and verilog[C]∥Proc of the 6th International Conference on High Performance Compilation,Computing and Communications,2022:124-130.
|
[21] |
Greaves D J. A verilog to C compiler[C]∥Proc of the 11th International Workshop on Rapid System Prototyping,2000:122-127.
|
[22] |
Dai Di,Zhang Fu-xin.Design and implementation of Verilog to C translation tool[J].Computer Engineering,2006,32(9):267-269.(in Chinese)
|
[23] |
Brayton R, Mishchenko A.ABC:An academic industrial-strength verification tool[C]∥Proc of the 22nd International Conference on Computer Aided Verification,2010:24-40.
|
[24] |
Goel A, Sakallah K.AVR:Abstractly verifying reachability[C]∥Proc of the 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems,2020:413-422.
|
[25] |
Irfan A,Cimatti A,Griggio A,et al.Verilog2SMV:A tool for word-level verification[C]∥Proc of 2016 Design,Automation & Test in Europe Conference & Exhibition,2016:1156-1159.
|
[26] |
Zhang R,Deutschbein C,Huang P,et al.End-to-end automated exploit generation for validating the security of processor designs[C]∥Proc of 2018 51st Annual IEEE/ACM International Symposium on Microarchitecture,2018:815-827.
|
[27] |
Mukherjee R,Kroening D,Melham T.Hardware verification using software analyzers[C]∥Proc of 2015 IEEE Computer Society Annual Symposium on VLSI,2015:7-12.
|
[28] |
Mukherjee R,Schrammel P,Kroening D,et al.Unbounded safety verification for hardware using software analyzers[C]∥Proc of 2016 Design,Automation & Test in Europe Conference & Exhibition,2016:1152-1155.
|
|
附中文参考文献:
|
[1] |
王戟,詹乃军,冯新宇,等.形式化方法概貌[J].软件学报,2019,30(1):33-61.
|
[22] |
戴笛,张福新.Verilog到C翻译器的设计与实现[J].计算机工程,2006,32(9):267-269.
|