Rigorous Development of High-integrity Java Applications

报告题目： Rigorous Development of High-integrity Java Applications

报告人：Frank Zeyda 副教授

主持人： 朱惠彪 教授

时间：2016年4月14日周四 10：00—11：30

地点：中北校区理科楼B1002

报告摘要：

    The talk presents and overview of my work on the High-integrity Java Applications using Circus project (hiJAC) at York from 2010 to 2014. The aim of this project was to develop novel verification techniques for Safety-Critical Java (SCJ). SCJ is still a fairly recent initiative to define a restricted version of Java that is amenable to formal analysis and certification.  The challenge of hiJAC is to address many features of SCJ in a single refinement notation with a unified semantics, including time, interaction, the SCJ execution paradigm, memory models, and object orientation. I shall touch on various aspects, comprising the issue of specifying and modelling SCJ programs, establishing correctness of implementations via refinement, and on-going work on mechanising the semantics of the underlying formal notations, which are based on the Circus family of languages.