您目前的位置: 首页» 公共目录» 学术活动

学术报告:Interval Counterexamples for Loop Invariant Learning

       题:Interval Counterexamples for Loop Invariant Learning

    人:贺飞 清华大学副教授

       间:20201214日(周 14:00




  Loop invariant generation has long been a challenging problem. Black-box learning has recently emerged as a promising method for inferring loop invariants. However, the performance depends heavily on the quality of collected examples. In many cases, only after tens or even hundreds of constraint queries, can a feasible invariant be successfully inferred.

  To reduce the gigantic number of constraint queries and improve the performance of black-box learning, we introduce interval counterexamples into the learning framework. Each interval counterexample represents a set of counterexamples from constraint solvers. We propose three different generalization techniques to compute interval counterexamples. The existing decision tree algorithm is also improved to adapt interval counterexamples. We evaluate our techniques and report over 40% improvement on learning rounds and verification time over the state-of-the-art approach.


  贺飞,博士,清华大学副教授。主要从事形式化方法、程序分析与验证、可满足性判定等方面的研究。主持开发了模型检测工具Beagle,软件验证工具Ceagle等工具。研究成果成功应用于航空、航天、高铁等国家重大安全领域。在包括POPL, CAV, PLDI, OOPSLA, ICSE, FSE, ASE, TSE, TOSEM, TDSC, TC等在内的国际重要会议和期刊上发表论文60余篇。作为负责人主持和承担国家自然科学基金项目4项,作为主要技术骨干参与国家973项目、国家自然科学基金重大项目、国家科技支撑计划项目多项。曾担任CONCUR, FMCAD, APLAS, ICECCS, SETTA等重要国际学术会议的程序委员会委员。