岗位职责
- 用形式化方法对程序语言的内存安全、功能安全性进行验证，特别是Rust语言方向；
- 用形式化方法对安全时序逻辑和功能、协议设计、算法设计的安全属性，进行验证；
- 用形式化方法对较简单的、小规模的AI系统的安全属性，进行验证；
- 探索形式化方法，发表高水平论文或专利，提升蚂蚁集团在该领域的业界影响力；
- 与国内外形式化验证领域的一流研究机构进行交流与合作。
职位要求
- 有相关研究背景的博士生，特别优秀的硕士生亦可；
- 有良好的研究背景和成果，在高水平国际会议或者学术期刊发表过形式化验证相关论文；
- 具备发现问题的能力和开发实现能力，能够把研究想法转化为Demo应用；
- 有良好的表达和沟通能力及协作精神，工作认真严谨，有强烈的责任心；
- 熟悉某种形式化工具，如Coq,Isabelle,ProVerif,Tamarin,NvSMV,TLA+,KLEE,BMC,Astree,TrustInSoft等；
- 至少3个月的实习工作。
