A Generic Dynamic Logic for Program Reasoning based on Operational Semantics
Yuanrui Zhang, Zhibin Yang
HHLPar: Automated Theorem Prover for Parallel Hybrid Communicating Sequential Processes
Xiangyu Jin, Bohua Zhan, Shuling Wang, Naijun Zhan
Separation Logic with Heap Variables: A Decision Procedure and Its Application
Xie Li, Yutian Zhu, Taolue Chen, Fu Song, Zhilin Wu
Efficient Decomposition Identification of Deterministic Finite Automata from Examples
Junjie Meng, Jie An, Yong Li, Andrea Turrini, Fanjiang Xu, Naijun Zhan, Miaomiao Zhang
Modular Data Refinement
David Faitelson, Leonid Shepetovsky, Shmuel Tyszberowicz
TBD