程序正确性验证与树自动机

本项目建立在lambda-演算,并发理论,类型理论,模型检测和树自动机理论及其相关领域的基础上。拟开展下列三方面的研究：..（1）以树自动机为媒介，研究程序正确性验证的两个基本方法(即:模型检测和逻辑推理)之间的互补关系，以及正确性判定的能行性和复杂性。以期建立更为优化的程序正确性判断的自动一致的检验方法。并予以实现。.（2）分析研究程序正确性判定的项模式（term schema）算法。以期建立相应于项模式不同归约的序列演算（sequent calculus）。进而研究演算的性质以及相应的"Curry-Howard对应"。.（3）以树自动机为平台，建立串行演算在并发演算中的嵌入。