职位描述
1.前沿技术研究与攻关：深耕实时系统形式化基础理论，开展时间自动机、时序逻辑（STL/LTL/CTL）、时间自动机网络、模型学习（主动/被动学习算法）等方向的技术研究，突破高可信软件验证中的可判定性、表达能力、验证效率等核心技术瓶颈。
2.验证工具研发与迭代：参与公司现有形式化验证工具链的研发与升级，负责实时系统验证引擎、WCET（最坏执行时间）分析工具等核心模块的算法设计与工程实现；牵头或参与AI可信研发体系下全流程验证工具的规划与落地，覆盖需求形式化规约、自动化建模、性质验证到结果输出的完整工具链路；基于抽象解释、符号执行、数据流分析、指针分析、别名分析等技术，针对内存安全、空指针、越界访问、资源泄漏、并发缺陷、注入与信息泄露等问题建立可解释的缺陷模型与检测规则。
3.工业项目技术支撑：面向高端制造、高端芯片等安全攸关领域客户项目，输出形式化验证整体技术方案，解决操作系统内核、嵌入式软件、FPGA逻辑等场景的实时性、安全性验证难题，保障项目交付质量与行业合规要求。
4.技术沉淀与知识产权建设：跟踪形式化方法、可信AI领域的学术与工业前沿，产出高质量技术专利、学术论文与内部技术资产，持续迭代工具核心能力，构建公司自主技术壁垒。
5.跨团队协同与技术落地：与产品、售前、项目交付团队协同，推动形式化验证技术从实验室原型到工业级产品的落地转化，优化工具的工程实用性、易用性与大规模验证效率。任职要求
1.硕士以上学历，计算机软件与理论、计算机科学与技术、电子信息、应用数学等相关专业。
2.系统掌握形式化验证基础理论，精通时间自动机、模型检验、定理证明中至少一个方向，熟悉SMT求解原理与常用求解器的工程应用。
3.具备扎实的科研产出能力，在RTSS、CAV、TACAS、FM等形式化与实时系统领域顶级会议或期刊发表过学术论文者优先。
4.有安全攸关软件、嵌入式软件的形式化验证相关项目经验，了解高可信软件全生命周期验证流程。
5.具备良好的工程实现能力，熟练掌握C/C++/Python/OCaml等至少一种编程语言，有形式化工具开发、验证引擎研发经验者优先。
6.熟悉UPPAAL、SPIN、Coq、Z3、NuSMV等主流形式化工具的原理与二次开发者优先；有LLVM/Clang Static Analyzer、CodeQL、Soot、WALA、SVF、KLEE、angr、Cppcheck、Infer等工具使用或二次开发经验者优先。
7.有AI模型可信验证、大模型形式化规约与验证、AI辅助测试相关研究或实践经验者优先。
8.具备优秀的逻辑思维、问题分析能力与技术文档撰写能力，能够独立开展课题研究与技术攻关。
