内容

学术讲座:机器学习算法及模型检验

阅读数:850    发布:2017-06-12 09:59    

时间:619日上午10

地点:计算机楼938


摘要:模型检验是通过遍历待验证系统的状态空间来验证系统模型是否满足给定的时序性质。如果不满足性质时模型检验会给出具体反例路径。状态空间爆炸是模型检验技术面临的最大挑战。组合验证、反例制导的抽象精化方法被提出来缓解此问题。其基本思路为构造系统抽象模型,验证(通常小得多)抽象后模型。当抽象后模型违反给定性质时,将相关反例在原系统上确认是否真实,如确认真实则性质不成立,否则分析出抽象模型中导致虚假反例出现的因素,进一步对抽象进行精化。如何构造抽象模型是这个技术的关键。另一方面,基于自动机的机器学习算法L*被广泛应用到模型检验等形式化方法。我们将讨论如何扩展L*到更一般自动机学习,已经如何将其应用到抽象模型构造、组合验证框架中去。


简历:张立军,毕业于德国萨尔大学,博士,中国科学院软件研究所计算机国家重点实验室研究员。作为软件所重点实验室概率模型检验方向学术带头人,张立军在形式化方法、模型检验理论创新、算法设计和工具实现三方面取得重要成果。在理论上改善模型检验的状态空间爆炸的瓶颈,有丰富的工具开发经验,带领团队开发出了多个概率模型检验工具。研究成果在国际相关领域得到认可:谷歌学术收录论文60余篇,被引用一千三百余次。于 2012 年被聘为丹麦科技大学终身副教授。发表论文60余篇,包括CCF A17篇、B23篇。


深圳大学计算机与软件学院 2009-2016