23 citations · 68 across the 22 of their papers we have counts for
24 papers
Compiler-Grounded Hierarchical Diagnosis for LLM-Based Triton Kernel Optimization
Dongjie Chen, Ping Zhao, Bohua Zhan +11
Recent advances in large language models (LLMs) have enabled automated kernel generation and optimization, but most existing approaches rely on surface signals such as compilation…
HpC: A Calculus for Hybrid and Mobile Systems -- Full Version
Xiong Xu, Jean-Pierre Talpin, Shuling Wang +4
Networked cybernetic and physical systems of the Internet of Things (IoT) immerse civilian and industrial infrastructures into an interconnected and dynamic web of hybrid and mobil…
Verifying Randomized Consensus Protocols with Common Coins
Song Gao, Bohua Zhan, Zhilin Wu +1
Randomized fault-tolerant consensus protocols with common coins are widely used in cloud computing and blockchain platforms. Due to their fundamental role, it is vital to guarantee…
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…
KBX: Verified Model Synchronization via Formal Bidirectional Transformation
Jianhong Zhao, Yongwang Zhao, Peisen Yao +3
Complex safety-critical systems require multiple models for a comprehensive description, resulting in error-prone development and laborious verification. Bidirectional transformati…
Mars 2.0: A Toolchain for Modeling, Analysis, Verification and Code Generation of Cyber-Physical Systems
Bohua Zhan, Xiong Xu, Qiang Gao +4
We introduce Mars 2.0 for modeling, analysis, verification and code generation of Cyber-Physical Systems. Mars 2.0 integrates Mars 1.0 with several important extensions and improve…
OSVAuto: automatic proofs about functional specifications in OS verification
Yulun Wu, Bican Xia, Jiale Xu +2
We present OSVAuto for automatic proofs about functional specifications that commonly arise when verifying operating system kernels. The algorithm behind OSVAuto is designed to sup…
Formally Verified C Code Generation from Hybrid Communicating Sequential Processes
Shuling Wang, Zekun Ji, Bohua Zhan +3
Hybrid Communicating Sequential Processes (HCSP) is a formal model for hybrid systems, including primitives for evolution along an ordinary differential equation (ODE), communicati…
Efficient Local Search for Nonlinear Real Arithmetic
Zhonghan Wang, Bohua Zhan, Bohan Li +1
Local search has recently been applied to SMT problems over various arithmetic theories. Among these, nonlinear real arithmetic poses special challenges due to its uncountable solu…
Compression of enumerations and gain
George Barmpalias, Xiaoyan Zhang, Bohua Zhan
We study the compressibility of enumerations in the context of Kolmogorov complexity, focusing on strong and weak forms of compression and their gain: the amount of auxiliary infor…
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…
Active Learning of One-Clock Timed Automata using Constraint Solving
Runqing Xu, Jie An, Bohua Zhan
Active automata learning in the framework of Angluin's algorithm has been applied to learning many kinds of automata models. In applications to timed models such as timed aut…
Machine-checked executable semantics of Stateflow
Shicheng Yi, Shuling Wang, Bohua Zhan +1
Simulink is a widely used model-based development environment for embedded systems. Stateflow is a component of Simulink for modeling event-driven control via hierarchical state ma…
Learning One-Clock Timed Automata
Jie An, Mingshuai Chen, Bohua Zhan +2
We present an algorithm for active learning of deterministic timed automata with a single clock. The algorithm is within the framework of Angluin's algorithm and inspired by…
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…
Combinatorial Proofs in Bordered Heegaard Floer homology
Bohua Zhan
Using bordered Floer theory, we give a combinatorial construction and proof of invariance for the hat version of Heegaard Floer homology. As a part of the proof, we also establish…
Explicit Koszul-dualizing bimodules in bordered Heegaard Floer homology
Bohua Zhan
We give a combinatorial proof of the quasi-invertibility of in bordered Heegaard Floer homology, which implies a Koszul self-duality on the…
Super-Polynomial Quantum Speed-ups for Boolean Evaluation Trees with Hidden Structure
Bohua Zhan, Shelby Kimmel, Avinatan Hassidim
We give a quantum algorithm for evaluating a class of boolean formulas (such as NAND trees and 3-majority trees) on a restricted set of inputs. Due to the structure of the allowed…