报告一题目：面向符号执行的不可满足约束求解优化
报告时间：2025年5月23日上午10:30
报告地点：计算机学院B404会议室
报告人：帅子琦
报告人单位：武汉大学计算机学院
报告人简介：帅子琦，武汉大学弘毅博士后，2024年于国防科技大学获得工学博士学位，并于2025年4月入职武汉大学计算机学院，主要研究方向为程序分析和约束求解。在FSE、ISSTA、ASE、JSS、JSEP、APSEC等软件工程领域的主流会议与期刊上发表学术论文9篇，获得授权发明专利5项。研究成果获得一项ACM SIGSOFT杰出论文奖（ISSTA 2021）。在学术服务方面，多次担任JASE、SoftwareX、EMSE、JSS、软件学报等领域内重要期刊的审稿人。
报告摘要：现代符号执行引擎广泛应用缓存机制来加速约束求解过程。然而，已有的约束求解缓存机制主要针对可满足约束设计，对于不可满足约束的处理能力较弱。当缓存未命中时，符号执行仍需调用重量级的SMT求解器判断约束的可满足性，其中通常包含大量不可满足的约束。因此，提升不可满足约束的求解效率，有望提高符号执行的整体性能。本报告将介绍报告人近期在该方向的研究进展，探讨如何利用SMT求解器输出的典型中间信息—不可满足核—来优化符号执行中不可满足约束的求解效率。
报告二题目：Human Pose Estimation for Embodied Medical AI
报告时间：2025年5月23日上午11:00
报告地点：计算机学院B404会议室
报告人：张敬
报告人单位：武汉大学计算机学院
报告人简介：张敬，博士，武汉大学计算机学院教授、博士生导师。2024年入选国家高层次青年人才、湖北省高层次人才。从事计算机视觉、医学大模型、机器人等领域的研究。发表CCF A类国际期刊和会议论文100余篇，谷歌学术引用13,000余次。2023年晋升IEEE Senior Member。2022-2024连续三年入选斯坦福全球前2%科学家榜单。担任NeurIPS AC、AAAI/IJCAI SPC、领域内顶级国际会议和期刊的审稿人、国内外知名高校博士/硕士论文评审专家。
报告摘要：人体姿态估计旨在从单张图像（或者多视角、连续图像序列）中检测人体2D/3D稀疏或者稠密关键点，可作为动作识别、行为分析、动画驱动与渲染、人机交互等任务的基本输入表征，在数字人、具身智能等领域应用广泛。本报告将重点介绍单目人体姿态估计领域的研究进展，以及课题组近年来所取得的相关研究成果，并将以课题组开发的超声机器人原型为例，阐述此项技术在医学具身智能领域的应用前景。
