In this article, we give an overview of our project on higher-order program verification based on HFL (higher-order fixpoint logic) model checking. After a brief introduction to HFL, we explain how it can be applied to program verification, and summarize the current status of the project.
翻译：在本文中,我们根据HFL(高阶固定点逻辑)模型检查,概述了我们关于高阶方案核查的项目。在简要介绍HFL之后,我们解释了如何将其应用于程序核查,并总结了项目的现状。
相关内容
ACM/IEEE第23届模型驱动工程语言和系统国际会议，是模型驱动软件和系统工程的首要会议系列，由ACM-SIGSOFT和IEEE-TCSE支持组织。自1998年以来，模型涵盖了建模的各个方面，从语言和方法到工具和应用程序。模特的参加者来自不同的背景，包括研究人员、学者、工程师和工业专业人士。MODELS 2019是一个论坛，参与者可以围绕建模和模型驱动的软件和系统交流前沿研究成果和创新实践经验。今年的版本将为建模社区提供进一步推进建模基础的机会，并在网络物理系统、嵌入式系统、社会技术系统、云计算、大数据、机器学习、安全、开源等新兴领域提出建模的创新应用以及可持续性。
官网链接：http://www.modelsconference.org/
专知会员服务
18+阅读 · 2020年4月25日
Arxiv
0+阅读 · 2021年11月1日
相关VIP内容
专知会员服务
18+阅读 · 2020年4月25日
相关资讯
相关论文
Arxiv
0+阅读 · 2021年11月1日
微信扫码咨询专知VIP会员