23 citations · 68 across the 22 of their papers we have counts for
9 papers · 1 filter
HHLPar: Automated Theorem Prover for Parallel Hybrid Communicating Sequential Processes
Xiangyu Jin, Bohua Zhan, Shuling Wang +1
We present a tool called HHLPar for verifying hybrid systems modelled in Hybrid Communicating Sequential Processes (HCSP). HHLPar is built upon a Hybrid Hoare Logic for HCSP, which…
A Generalized Hybrid Hoare Logic
Naijun Zhan, Xiangyu Jin, Bohua Zhan +2
Deductive verification of hybrid systems (HSs) increasingly attracts more attention in recent years because of its power and scalability, where a powerful specification logic for H…
HHLPy: Practical Verification of Hybrid Systems using Hoare Logic
Huanhuan Sheng, Alexander Bentkamp, Bohua Zhan
We present a tool for verification of hybrid systems expressed in the sequential fragment of HCSP (Hybrid Communicating Sequential Processes). The tool permits annotating HCSP prog…
NIL: Learning Nonlinear Interpolants
Mingshuai Chen, Jian Wang, Jie An +3
Nonlinear interpolants have been shown useful for the verification of programs and hybrid systems in contexts of theorem proving, model checking, abstract interpretation, etc. The…
HolPy: Interactive Theorem Proving in Python
Bohua Zhan
HolPy is an interactive theorem proving system implemented in Python. It uses higher-order logic as the logical foundation. Its main features include a pervasive use of macros in p…
Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle
Bohua Zhan, Maximilian P. L. Haslbeck
We present a framework in Isabelle for verifying asymptotic time complexity of imperative programs. We build upon an extension of Imperative HOL and its separation logic to include…
Formalization of the fundamental group in untyped set theory using auto2
Bohua Zhan
We present a new framework for formalizing mathematics in untyped set theory using auto2. Using this framework, we formalize in Isabelle/FOL the entire chain of development from th…
Efficient verification of imperative programs using auto2
Bohua Zhan
Auto2 is a recently introduced prover for the proof assistant Isabelle. It is designed to be both highly customizable from within Isabelle, and also have a powerful proof search me…
AUTO2, a saturation-based heuristic prover for higher-order logic
Bohua Zhan
We introduce a new theorem prover for classical higher-order logic named auto2. The prover is designed to make use of human-specified heuristics when searching for proofs. The core…