在Isabelle中形式化规约与证明Forensic Lucid的操作语义
计算机科学中的逻辑
2009-05-08 v1 密码学与安全
编程语言
摘要
为进行内涵式网络取证分析，已提出一种Forensic Lucid内涵编程语言。该语言在很大程度上基于由高阶内涵逻辑（HOIL）统一约束的各种前驱和后继Lucid方言。本工作形式化规约了Forensic Lucid语言的操作语义，并利用证明助手系统Isabelle编译了其构造的理论。
引用
@article{arxiv.0904.3789,
title = {Formally Specifying and Proving Operational Aspects of Forensic Lucid in Isabelle},
author = {Serguei A. Mokhov and Joey Paquet},
journal= {arXiv preprint arXiv:0904.3789},
year = {2009}
}
备注
23 pages, 3 listings, 3 figures, 1 table, 1 Appendix with theorems, pp. 76--98. TPHOLs 2008 Emerging Trends Proceedings, August 18-21, Montreal, Canada. Editors: Otmane Ait Mohamed and Cesar Munoz and Sofiene Tahar. The individual paper's PDF is at http://users.encs.concordia.ca/~tphols08/TPHOLs2008/ET/76-98.pdf