Towards the Generation of Correct Java Programs (Research Poster).
HPCS(2018)
摘要
Proof assistants such as Coq [1] can be used to develop very high assurance software such as a verified C compiler [2] and verified high performance computing programs [3]. Even when not used for a full system, using such a proof assistant to develop critical parts of a system could be interesting, for example security monitors [4] or the reconfiguration mechanism of a component based system.
更多查看译文
关键词
proof assistant,high performance computing programs,component based system,Coq code,Big Data applications,security monitors,Java development,code generation,Java code,C compiler,Coq development,Java programs
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络