arXiv subjects

Hanxi Chen

Publications and source records attributed to Hanxi Chen.

3 recordsLinked to original sources

arXiv2026

Oblivious Probabilistic Outcome Logic: Verifying Probabilistic Programs with an Oblivious Adversary

In the context of probabilistic programs, an oblivious adversary resolves nondeterminism without seeing the outcomes of random draws. Obliviousness is a common assumption in online algorithms and distributed protocols, but the complex interaction between random draws and adversarial choices makes it challenging to reason about correctness. While there has been significant progress toward reasoning about programs that combine randomization with nondeterminism, most of the work has focused on the adaptive model, whose omniscient view of program state is too powerful to establish correctness for certain classes of programs. We introduce Oblivious Probabilistic Outcome Logic (opOL), a new logic for reasoning about probabilistic programs with nondeterminism controlled by an oblivious adversary. Building on Outcome Logic and Probabilistic Separation Logic, opOL models adversarial choice as a resource and uses probabilistic independence to ensure that random outcomes are hidden from the adversary. The opOL proof system provides expressive and compositional rules for case analysis on both random and nondeterministic outcomes, and for proving almost-sure termination. Expressivity is tested through several case studies, including a paging algorithm and a leader election protocol. The opOL metatheory and case studies are mechanized in Lean 4.

cs.PL↗

arXiv2026

A Physics-Informed Neural Network for Small-Signal Stability in Multi-Inverter Power Systems

The whole-system impedance model has proven a powerful tool for assessing the small-signal stability of multi-inverter power systems; however, its application is limited to a small range around a steady-state operating point due to the inherent assumptions of time invariance and linearisation. In this paper, a dedicated physics-informed neural network (PINN) for small-signal stability analysis in high-dimensional multi-inverter power systems is developed. The PINN is trained with step-response data produced from limited sets of system electromagnetic transient (EMT) simulations, and the trained model can predict the poles and residues of the whole-system impedance/admittance model, i.e., the transfer functions, across the full operating space. Such a PINN offers unique insights into system stability that surpass what conventional analytical methods or EMT simulations can achieve. By characterising how the impedance model evolves with power flow variations, it predicts the dynamic behaviour of the time-varying system and reveals oscillation risks that may emerge while identifying their root causes. It also provides direct visualisation of the possible range of oscillatory modes under a given power flow condition, enabling an optimal generation distribution while maintaining safe operation of the system. The proposed PINN is fully validated on a 2-IBR system and a 4-IBR system, with its application details presented.

eess.SY↗

arXiv2024

A Two-Phase Infinite/Finite Low-Level Memory Model

This paper provides a novel approach to reconciling complex low-level memory model features, such as pointer--integer casts, with desired refinements that are needed to justify the correctness of program transformations. The idea is to use a "two-phased" memory model, one with and unbounded memory and corresponding unbounded integer type, and one with a finite memory; the connection between the two levels is made explicit by our notion of refinement that handles out-of-memory behaviors. This approach allows for more optimizations to be performed and establishes a clear boundary between the idealized semantics of a program and the implementation of that program on finite hardware. To demonstrate the utility of this idea in practice, we instantiate the two-phase memory model in the context of Zakowski et al.'s VIR semantics, yielding infinite and finite memory models of LLVM IR, including low-level features like undef and bitcast. Both the infinite and finite models, which act as specifications, can provably be refined to executable reference interpreters. The semantics justify optimizations, such as dead-alloca-elimination, that were previously impossible or difficult to prove correct.

cs.PL↗