Home Activities
Research and Development

  • 项目 Funding

  • 工具 Tools

  • TRust2: Rust语言可信工具链
        TRust2: Formally Verified Toolchain for Rust Language

  • Isabelle/Cloud定理证明云平台
        Isabelle/Cloud: Cloud IDE for Isabelle/HOL Theorem Prover

  • PiCore并发系统组合验证工具
        PiCore: A Rely-Guarantee Reasoning Framework

  • CSimpl并发语言与验证工具
        CSimpl: A Framework for Verifying Concurrent Programs

  • 团队/社区 Team & Community

  • 翔云创新团队
        FlyAir Innovation Lab

  • TPChina定理证明开放社区
       TPChina Theorem Proving Open Community

  • 矽望泛在操作系统社区
        SYSWONDER Ubiquitous Operating System Community

 
Publication

  • 论文 Papers

  • 报告和标准 Reports and Standards

  • 专著 Books (红-绿-蓝 三色书系列)

  • PiCore Formal Methods and Practices (Red Book)
        PiCore形式化方法与实践 (红书)

  • Functional Programming and Proof (Green Book)
        函数式程序设计与证明 (绿书)

  • Under Construction ... (Blue Book)
        正在编写 敬请期待...... (蓝书)

 
Teaching Call for papers