SearcharxivSearch

arXiv subjects

Bohua Zhan

Publications and source records attributed to Bohua Zhan.

At least 19 recordsLinked to original sources

Compiler-Grounded Hierarchical Diagnosis for LLM-Based Triton Kernel Optimization

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 feedback and profiling metrics. These signals reveal that a kernel is slow, but not why the backend compiler fails to realize a profitable optimization, especially on emerging accelerators such as NPUs. We therefore formulate kernel optimization as a progressive cross-layer diagnosis problem that links runtime symptoms to IR structure and compiler behavior before rewriting source. Based on this insight, we present our system, a compiler-grounded and hierarchical optimization framework for Triton kernels. the system escalates from lightweight pattern triage and profiling diagnosis to IR attribution and compiler-grounded analysis only when deeper evidence is needed, then proposes evidence-backed source-level rewrites. We implement the system on Triton for Ascend NPUs and evaluate it on 37 successfully converted entries from a standardized NPUKernelBench-derived Ascend 950 benchmark. Across these entries, the system attains a geometric-mean speedup of 4.35$\times$ and a median speedup of 2.73$\times$ from the initial to optimized Triton kernel; 22/37 exceed 2$\times$ and 13/37 exceed 5$\times$. The complete distribution ranges from near-baseline entries to large wins, motivating transparent reporting of the current system's scope and limitations.

cs.AI

HHLPar: Automated Theorem Prover for Parallel Hybrid Communicating Sequential Processes

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 is able to reason about continuous-time properties of differential equations, as well as communication and parallel composition of parallel HCSP processes with the help of parameterised trace assertions and their synchronization. The logic was formalised and proved to be sound in Isabelle/HOL, which constitutes a trustworthy foundation for the verification conducted by HHLPar. HHLPar implements the Hybrid Hoare Logic in Python and supports automated verification: On one hand, it provides functions for symbolically decomposing HCSP processes, generating specifications for separate sequential processes and then composing them via synchronization to obtain the final specification for the whole parallel HCSP processes; On the other hand, it is integrated with external solvers for handling differential equations and real arithmetic properties. We have conducted experiments on a simplified cruise control system to validate the performance of the tool.

cs.LO

Compression of enumerations and gain

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 information embedded in the compressed enumeration. The existence of strong compression and weak gainless compression is shown for any computably enumerable (c.e.) set. The density problem of c.e. sets with respect to their prefix complexity is reduced to the question of whether every c.e. set is well-compressible, which we study via enumeration games.

cs.CL

OSVAuto: automatic proofs about functional specifications in OS verification

We present OSVAuto for automatic proofs about functional specifications that commonly arise when verifying operating system kernels. The algorithm behind OSVAuto is designed to support natively those data types that commonly occur in OS verification, including sequences, maps, structures and enumerations. Propositions about these data are encoded into a form that is suitable for SMT solving. For quantifier instantiation, we propose an extension of recent work for automatic proofs about sequences. We evaluate the algorithm on proof obligations adapted from existing verification of the uC-OS/II kernel in Coq, demonstrating that a large number of proof obligations can be solved automatically, significantly reducing the proof effort on the functional side.

cs.SC

HpC: A Calculus for Hybrid and Mobile Systems -- Full Version

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 mobile devices. The key feature of such systems is the hybrid and tight coupling of mobile and pervasive discrete communications in a continuously evolving environment (discrete computations with predominant continuous dynamics). In the aim of ensuring the correctness and reliability of such heterogeneous infrastructures, we introduce the hybrid π-calculus (HpC), to formally capture both mobility, pervasiveness and hybridisation in infrastructures where the network topology and its communicating entities evolve continuously in the physical world. The π-calculus proposed by Robin Milner et al. is a process calculus that can model mobile communications and computations in a very elegant manner. The HpC we propose is a conservative extension of the classical π-calculus, i.e., the extension is ``minimal'', and yet describes mobility, time and physics of systems, while allowing to lift all theoretical results (e.g. bisimulation) to the context of that extension. We showcase the HpC by considering a realistic handover protocol among mobile devices.

cs.PL

Verifying Randomized Consensus Protocols with Common Coins

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 their correctness. Threshold automata is a formal model designed for the verification of fault-tolerant consensus protocols. It has recently been extended to probabilistic threshold automata (PTAs) to verify randomized fault-tolerant consensus protocols. Nevertheless, PTA can only model randomized consensus protocols with local coins. In this work, we extend PTA to verify randomized fault-tolerant consensus protocols with common coins. Our main idea is to add a process to simulate the common coin (the so-called common-coin process). Although the addition of the common-coin process destroys the symmetry and poses technical challenges, we show how PTA can be adapted to overcome the challenges. We apply our approach to verify the agreement, validity and almost-sure termination properties of 8 randomized consensus protocols with common coins.

cs.DC

A Generalized Hybrid Hoare Logic

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 HSs is the cornerstone. Often, HSs are naturally modelled by concurrent processes that communicate with each other. However, existing specification logics cannot easily handle such models. In this paper, we present a specification logic and proof system for Hybrid Communicating Sequential Processes (HCSP), that extends CSP with ordinary differential equations (ODE) and interrupts to model interactions between continuous and discrete evolution. Because it includes a rich set of algebraic operators, complicated hybrid systems can be easily modelled in an algebra-like compositional way in HCSP. Our logic can be seen as a generalization and simplification of existing hybrid Hoare logics (HHL) based on duration calculus (DC), as well as a conservative extension of existing Hoare logics for concurrent programs. Its assertion logic is the first-order theory of differential equations (FOD), together with assertions about traces recording communications, readiness, and continuous evolution. We prove continuous relative completeness of the logic w.r.t. FOD, as well as discrete relative completeness in the sense that continuous behaviour can be arbitrarily approximated by discretization. Finally, we implement the above logic in Isabelle/HOL, and apply it to verify two case studies to illustrate the power and scalability of our logic.

cs.LO

KBX: Verified Model Synchronization via Formal Bidirectional Transformation

Complex safety-critical systems require multiple models for a comprehensive description, resulting in error-prone development and laborious verification. Bidirectional transformation (BX) is an approach to automatically synchronizing these models. However, existing BX frameworks lack formal verification to enforce these models' consistency rigorously. This paper introduces KBX, a formal bidirectional transformation framework for verified model synchronization. First, we present a matching logic-based BX model, providing a logical foundation for constructing BX definitions within the $\mathbb{K}$ framework. Second, we propose algorithms to synthesize formal BX definitions from unidirectional ones, which allows developers to focus on crafting the unidirectional definitions while disregarding the reverse direction and missing information recovery for synchronization. Afterward, we harness $\mathbb{K}$ to generate a formal synchronizer from the synthesized definitions for consistency maintenance and verification. To evaluate the effectiveness of KBX, we conduct a comparative analysis against existing BX frameworks. Furthermore, we demonstrate the application of KBX in constructing a BX between UML and HCSP for real-world scenarios, showcasing an 82.8\% reduction in BX development effort compared to manual specification writing in $\mathbb{K}$.

cs.SE

Mars 2.0: A Toolchain for Modeling, Analysis, Verification and Code Generation of Cyber-Physical Systems

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 improvements, allowing the design of cyber-physical systems using the combination of AADL and Simulink/Stateflow, which provide a unified graphical framework for modeling the functionality, physicality and architecture of the system to be developed. For a safety-critical system, formal analysis and verification of its combined AADL and Simulink/Stateflow model can be conducted via the following steps. First, the toolchain automatically translates AADL and Simulink/Stateflow models into Hybrid CSP (HCSP), an extension of CSP for formally modeling hybrid systems. Second, the HCSP processes can be simulated using the HCSP simulator, and to complement incomplete simulation, they can be verified using the Hybrid Hoare Logic prover in Isabelle/HOL, as well as the more automated HHLPy prover. Finally, implementations in SystemC or C can be automatically generated from the verified HCSP processes. The transformation from AADL and Simulink/Stateflow to HCSP, and the one from HCSP to SystemC or C, are both guaranteed to be correct with formal proofs. This approach allows model-driven design of safety-critical cyber-physical systems based on graphical and formal models and proven-correct translation procedures. We demonstrate the use of the toolchain on several benchmarks of varying complexity, including several industrial-sized examples.

cs.PL

Formally Verified C Code Generation from Hybrid Communicating Sequential Processes

Hybrid Communicating Sequential Processes (HCSP) is a formal model for hybrid systems, including primitives for evolution along an ordinary differential equation (ODE), communication, and parallel composition. Code generation is needed to convert HCSP models into code that can be executed in practice, and the correctness of this conversion is essential to ensure that the generated code accurately reflects the formal model. In this paper, we propose a code generation algorithm from HCSP to C with POSIX library for concurrency. The main difficulties include how to bridge the gap between the synchronized communication model in HCSP and the use of mutexes for synchronization in C, and how to discretize evolution along ODEs and support interrupt of ODE evolution by communication. To prove the correctness of code generation, we define a formal semantics for POSIX C, and build transition system models for both HCSP and C programs. We then define an approximate bisimulation relation between traces of transition systems, and show that under certain robustness conditions for HCSP, the generated C program is approximately bisimilar to the original model. Finally, we evaluate the code generation algorithm on a detailed model for automatic cruise control, showing its utility on real-world examples.

cs.PL

Efficient Local Search for Nonlinear Real Arithmetic

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 solution space and potential need to solve higher-degree polynomials. As a consequence, existing work on local search only considered fragments of the theory. In this work, we analyze the difficulties and propose ways to address them, resulting in an efficient search algorithm that covers the full theory of nonlinear real arithmetic. In particular, we present two algorithmic improvements: incremental computation of variable scores and temporary relaxation of equality constraints. We also discuss choice of candidate moves and a look-ahead mechanism in case when no critical moves are available. The resulting implementation is competitive on satisfiable problem instances against complete methods such as MCSAT in existing SMT solvers.

cs.SC

HHLPy: Practical Verification of Hybrid Systems using Hoare Logic

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 programs with pre- and postconditions, invariants, and proof rules for reasoning about ordinary differential equations. Verification conditions are generated from the annotations following the rules of hybrid Hoare logic. We designed labeling and highlighting mechanisms to distinguish and visualize different verification conditions. The tool is implemented in Python and has a web-based user interface. We evaluated the effectiveness of the tool on translations of Simulink/Stateflow models and on KeYmaera X benchmarks.

cs.LO

Active Learning of One-Clock Timed Automata using Constraint Solving

Active automata learning in the framework of Angluin's $L^*$ algorithm has been applied to learning many kinds of automata models. In applications to timed models such as timed automata, the main challenge is to determine guards on the clock value in transitions as well as which transitions reset the clock. In this paper, we introduce a new algorithm for active learning of deterministic one-clock timed automata and timed Mealy machines. The algorithm uses observation tables that do not commit to specific choices of reset, but instead rely on constraint solving to determine reset choices that satisfy readiness conditions. We evaluate our algorithm on randomly-generated examples as well as practical case studies, showing that it is applicable to larger models, and competitive with existing work for learning other forms of timed models.

cs.FL

Machine-checked executable semantics of Stateflow

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 machines and flow charts. However, Stateflow lacks an official formal semantics, making it difficult to formally prove properties of its models in safety-critical applications. In this paper, we define a formal semantics for a large subset of Stateflow, covering complex features such as hierarchical states and transitions, event broadcasts, early return, temporal operators, and so on. The semantics is formalized in Isabelle/HOL and proved to be deterministic. We implement a tactic for automatic execution of the semantics in Isabelle, as well as a translator in Python transforming Stateflow models to the syntax in Isabelle. Using these tools, we validate the semantics against a collection of examples illustrating the features we cover.

cs.FL

Learning One-Clock Timed Automata

We present an algorithm for active learning of deterministic timed automata with a single clock. The algorithm is within the framework of Angluin's $L^*$ algorithm and inspired by existing work on the active learning of symbolic automata. Due to the need of guessing for each transition whether it resets the clock, the algorithm is of exponential complexity in the size of the learned automata. Before presenting this algorithm, we propose a simpler version where the teacher is assumed to be smart in the sense of being able to provide the reset information. We show that this simpler setting yields a polynomial complexity of the learning process. Both of the algorithms are implemented and evaluated on a collection of randomly generated examples. We furthermore demonstrate the simpler algorithm on the functional specification of the TCP protocol.

cs.FL

HolPy: Interactive Theorem Proving in Python

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 producing, checking, and storing proofs, a JSON-based format for theories, and an API for implementing proof automation and other extensions in Python. A point-and-click-based user interface is implemented for general-purpose theorem proving. We describe the main design decisions of HolPy, current applications, and plans for the future.

cs.LO

NIL: Learning Nonlinear Interpolants

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 underlying synthesis problem, however, is challenging and existing methods have limitations on the form of formulae to be interpolated. We leverage classification techniques with space transformations and kernel tricks as established in the realm of machine learning, and present a counterexample-guided method named NIL for synthesizing polynomial interpolants, thereby yielding a unified framework tackling the interpolation problem for the general quantifier-free theory of nonlinear arithmetic, possibly involving transcendental functions. We prove the soundness of NIL and propose sufficient conditions under which NIL is guaranteed to converge, i.e., the derived sequence of candidate interpolants converges to an actual interpolant, and is complete, namely the algorithm terminates by producing an interpolant if there exists one. The applicability and effectiveness of our technique are demonstrated experimentally on a collection of representative benchmarks from the literature, where in particular, our method suffices to address more interpolation tasks, including those with perturbations in parameters, and in many cases synthesizes simpler interpolants compared with existing approaches.

cs.LO

Efficient verification of imperative programs using auto2

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 mechanism. In this paper, we apply auto2 to the verification of imperative programs. We describe the setup of auto2 for both stages of the proof process: verification of a functional version of the program, and refining to the imperative version using separation logic. As examples, we verify several data structures, including red-black trees, interval trees, priority queues, and union-find. We also verify several algorithms making use of these data structures. These examples show that our framework is able to verify complex algorithms efficiently and in a modular manner.

cs.LO