arXiv subjects

Hengbiao Yu

Publications and source records attributed to Hengbiao Yu.

3 recordsLinked to original sources

arXiv2026

Taylor-Approximation-Based Repair of High Floating-Point Errors

Numerical libraries can still lose many bits of accuracy on localized ill-conditioned inputs, such as roots, poles, cancellation points, and branch boundaries. This paper presents NPTaylor, a Taylor-approximation-based framework for repairing localized high floating-point errors in numerical C routines. Given a high-error input, a localized repair domain, a high-precision oracle, and an error threshold, NPTaylor searches over Taylor degree, expansion center, segmentation, and floating-point evaluation strategy. It emits guarded C patches that use a generated Taylor evaluator inside the repair domain and fall back to the original routine outside it. Candidate patches are accepted only after validating the emitted C code on recorded local samples, guard endpoints, and the pre-repair peak input. The generated evaluator uses coefficient splitting and compensated Horner evaluation to reduce rounding error introduced by the patch itself. We evaluate NPTaylor on GSL benchmark workloads. On 38 one-input functions, both NPTaylor and AutoRNP repair all 114 configurations across three accuracy thresholds. NPTaylor is 3.33x faster by geometric-mean offline repair time and emits 0.162x as many C bytes. In the strictest setting, its median repair time is 3.74s versus 81.97s for AutoRNP. NPTaylor also repairs localized multi-input benchmark cases beyond AutoRNP's implemented one-input workflow. These results show that Taylor-based guarded patches can provide compact, efficient local repairs, while the claims remain validation-relative rather than full-domain proofs.

cs.SE↗

arXiv2020

Combining Symbolic Execution and Model Checking to Verify MPI Programs

Message passing is the standard paradigm of programming in high-performance computing. However, verifying Message Passing Interface (MPI) programs is challenging, due to the complex program features (such as non-determinism and non-blocking operations). In this work, we present MPI symbolic verifier (MPI-SV), the first symbolic execution based tool for automatically verifying MPI programs with non-blocking operations. MPI-SV combines symbolic execution and model checking in a synergistic way to tackle the challenges in MPI program verification. The synergy improves the scalability and enlarges the scope of verifiable properties. We have implemented MPI-SV (footnote: https://mpi-sv.github.io) and evaluated it with 111 real-world MPI verification tasks. The pure symbolic execution-based technique successfully verifies 61 out of the 111 tasks (55\%) within one hour, while in comparison, MPI-SV verifies 100 tasks (90\%). On average, compared with pure symbolic execution, MPI-SV achieves 19x speedups on verifying the satisfaction of the critical property and 5x speedups on finding violations.

cs.PL↗

arXiv2018

Boosting the Robustness Verification of DNN by Identifying the Achilles's Heel

Deep Neural Network (DNN) is a widely used deep learning technique. How to ensure the safety of DNN-based system is a critical problem for the research and application of DNN. Robustness is an important safety property of DNN. However, existing work of verifying DNN's robustness is time-consuming and hard to scale to large-scale DNNs. In this paper, we propose a boosting method for DNN robustness verification, aiming to find counter-examples earlier. Our observation is DNN's different inputs have different possibilities of existing counter-examples around them, and the input with a small difference between the largest output value and the second largest output value tends to be the achilles's heel of the DNN. We have implemented our method and applied it on Reluplex, a state-of-the-art DNN verification tool, and four DNN attacking methods. The results of the extensive experiments on two benchmarks indicate the effectiveness of our boosting method.

cs.LG↗