Chun Tian (binghe)

orcid.org/0000-0002-2777-9443

Postdoc (until May 2023) at Fondazione Bruno Kessler (FBK)
Email (personal): binghe.lisp@gmail.com

Area of Interests

• Runtime Verification (RV)
• Interactive Theorem Proving (Formal Mathematics)
  

Publications (Until May 2023)

1. Cimatti, Alessandro, Chun Tian, and Stefano Tonetta. "Assumption-based Runtime Verification." Formal Methods in System Design (2023): 1-48.
2. Tian, Chun: Assumption-Based Runtime Verification of Finite- and Infinite-State Systems, PhD thesis, Università di Trento, November, 2022.
   
3. Cimatti, A., Tian, C., Tonetta, S.: Assumption-Based Runtime Verification of Infinite-State Systems. In: Feng, L. and Fisman, D. (eds.) LNCS 12974 - Runtime Verification (RV 2021). pp. 207–227. Springer International Publishing (2021).
   
4. Tian, C., Sangiorgi, D.: Unique solutions of contractions, CCS, and their HOL formalisation. Inf. Comput. 104606 (2020).
   
5. Cimatti, A., Tian, C., Tonetta, S.: Assumption-Based Runtime Verification with Partial Observability and Resets. In: Finkbeiner, B. and Mariani, L. (eds.) LNCS 11757 - Runtime Verification (RV 2019). pp. 165–184 Springer International Publishing, Porto, Portugal (2019).
6. Cimatti, A., Tian, C., Tonetta, S.: NuRV: A nuXmv Extension for Runtime Verification. In: Finkbeiner, B. and Mariani, L. (eds.) LNCS 11757 - Runtime Verification (RV 2019). pp. 382–392 Springer International Publishing, Porto, Portugal (2019).
   
7. Tian, C., Sangiorgi, D.: Unique solutions of contractions, CCS, and their HOL formalisation. In Jorge A. Pérez and Simone Tini: Proceedings Combined 25th International Workshop on Expressiveness in Concurrency and 15th Workshop on Structural Operational Semantics (EXPRESS/SOS 2018), Beijing, China, September 3, 2018, Electronic Proceedings in Theoretical Computer Science 276, pp. 122–139.
8. Tian, C. A Formalization of Unique Solutions of Equations in Process Algebra, MSc thesis, Università di Bologna, December, 2017.
   

Software

• NuRV: a nuXmv extension package for Runtime Verification
  
• OSCAR - the general-purpose defeasible reasoner and architecture for a rational agent (Open Source)
• SWCLOS - OWL Full Processor on top of Common Lisp Object System (CLOS) (Open Source)
• usocket - universal socket library for Common Lisp (Open Source)
• cl-net-snmp: Simple Network Management Protocol (SNMP) for Common Lisp (Open Source)
• HOL Theorem Prover
  

(also see my GitHub profile for my contributions in various open source projects)

Participated Projects

• CITADEL - Critical Infrastructure Protection using Adaptive MILS (2017-2018)
• RobDT
• VIVAS