张昕荻(Xindi Zhang)的主页

本人目前就读于 中国科学院软件研究所, 计算机科学国家重点实验室, 指导老师为 蔡少伟研究员. 研究兴趣主要集中于 SAT, SMT, EDA 等问题.

教育经历

• 2018.09 - 至今. 硕博连读. 中国科学院软件研究所，计算机科学与技术
• 2014.09 - 2018.06. 本科. 吉林大学. 软件学院，工科试验班（软件工程方向）; 经济学院，金融学

获奖和荣誉

• 2023年，中国软件大会(CCF ChinaSoft) 优秀博士生 (全国选择14名博士生于相关论坛报告)

• 2023年，奋进奖学金 – 集成电路人才培养（全国共95名）

• 2023年，”朱李月华”优秀博士生奖学金（中科院300人，软件所2人）

• 2023年，国际 SAT 竞赛。金牌 3 项Main-Parallel-Track (ALL, SAT, UNSAT), PRS-sc23; 银牌 1 项 Cloud-Track

• 2023 年，国际 SMT 竞赛。最大领先奖， 最大贡献奖，多个细分赛道冠军, QF-LIA(;,‖,T,mv), QF_NLIA(;,‖,T,⊥,24), QF_NIA(;,‖,T), QF_IDL(⊥), z3++

• 2023年，第六届“强网杯”全国网络安全挑战赛，密码数学专项赛，（CMixSAT队伍）， 冠军

• 2022年，集成电路EDA设计精英挑战赛。“高位宽运算电路的逻辑等价性验证”赛题。二等奖、企业特别奖（海思）

• 2022年，国际SAT竞赛。金牌2项 [Main-Parallel-Track, Main-Parallel-Track-SAT] 冠军1项 [NoLimits-Track]; 银牌2项 [Main-Track, Main-Track-SAT]; 中国首次并行组冠军 , kissat_inc, kissat_pre, parkissat_rs

• 2022年，联合逻辑会议（FLoc）奥林匹克竞赛。SAT赛道金牌1块 [Parallel Track]; SMT赛道金牌两块 [Gold Biggest Lead Model Validation: Z3++，Glod Largest Contribution Model Validation: Z3++] Z3++

• 2022年，国际SMT竞赛。六个赛道冠军[Single Query Track: QF-NIA(UNSAT parallel), QF-NRA/QF-LIA(SAT parallel), QF-IDL(ALL); Model Validation Track: QF-LIA(ALL), QF-IDL(ALL)]

• 2021年，国际SAT竞赛。银牌2项 [Main-Track-SAT, Main-Track-UNSAT]；荣誉提名一项 [Crypto (Cadical Hack)]

• 2021年，国际SMT竞赛。中国首个世界冠军 [IDL-Track]

• 2020年，国际SAT竞赛。金牌一项[Main-Track-SAT], 亚军一项

• 2018年，国际SAT竞赛。NoLimit-Track 冠军

• 2018年，SAT Sparkle Challenge。亚军

• 2017年，美国数学建模竞赛。一等奖

• 2016年，高教社杯数学建模竞赛。国家级二等奖

• 2016年，国际遗传工程机器大赛(iGEM)。金奖（吉林大学首次）

• 2014-2018年，吉林大学“求实思源 服务社会”优秀学生培养计划（第三期）

• 曾获多次硕士研究生、博士研究生国家奖学金。

代表作

• Shaowei Cai, Xindi Zhang. Deep Cooperation of CDCL and Local Search for SAT. In SAT 2021. 共同一作, [中国首次最佳论文奖].

• *Shaowei Cai, Bohan Li, Xindi Zhang. Local Search For SMT on Linear Integer Arithmetic. In CAV 2022. 共同一作，姓名排序

• Xindi Zhang, Bohan Li, Shaowei Cai. Deep Combination of CDCL(T) and Local Search for Satisfiability Modulo Non-Linear Integer Arithmetic Theory. In ICSE 2024. 一作

其他文献详情请参见谷歌学术主页