16 citations · 26 across the 15 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…
Nonlinear Craig Interpolant Generation over Unbounded Domains by Separating Semialgebraic Sets
Hao Wu, Jie Wang, Bican Xia +3
Interpolation-based techniques become popular in recent years, as they can improve the scalability of existing verification techniques due to their inherent modularity and local re…
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…
Encoding inductive invariants as barrier certificates: synthesis via difference-of-convex programming
Qiuye Wang, Mingshuai Chen, Bai Xue +2
A barrier certificate often serves as an inductive invariant that isolates an unsafe region from the reachable set of states, and hence is widely used in proving safety of hybrid s…
Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming
Qiuye Wang, Mingshuai Chen, Bai Xue +2
A barrier certificate often serves as an inductive invariant that isolates an unsafe region from the reachable set of states, and hence is widely used in proving safety of hybrid s…
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…