arXiv subjects

Guanxuan Wu

Publications and source records attributed to Guanxuan Wu.

3 recordsLinked to original sources

arXiv2026

Typed Flexible-Arity Slotted E-Graphs: A Soundness Construction and an Alloy Case Study

Slotted e-graphs represent open terms modulo consistent renaming, while algebraic operators benefit from canonical sequence, bag, or set children. We compose the two at a specification level: typed slot-mapped invocations inhabit operator-declared ports whose sibling quotient and recursive flattening licenses are certified separately. A generic finite quotient presentation proves exactness of its least-orbit normal form, while certified records specify effective-support kernel extraction and collision. For abstract obligation traces carrying local endpoint certificates, we prove finite-unfolding equational soundness. An Alloy case study compares seven related pipeline arms on a frozen corpus and a controlled transformation suite. Its measurements characterize bounded capability and structural consolidation; they do not establish refinement of the Java artifact or experimental replay against the formal model.

cs.PL↗

arXiv2024

AlloyASG: Alloy Predicate Code Representation as a Compact Structurally Balanced Graph

Writing declarative models has numerous benefits, ranging from automated reasoning and correction of design-level properties before systems are built to automated testing and debugging of their implementations after they are built. Unfortunately, the model itself needs to be correct to gain these benefits. Alloy is a commonly used modeling language that has several existing efforts to repair faulty models automatically. Currently, these efforts are search-based methods that use an Abstract Syntax Tree (AST) representation of the model and do not scale. One issue is that ASTs themselves suffer from exponential growth in their data size due to the limitation that ASTs will often have identical nodes separately listed in the tree. To address this issue, we introduce a novel code representation schema, Complex Structurally Balanced Abstract Semantic Graph (CSBASG), which represents code as a complex-weighted directed graph that lists a semantic element as a node in the graph and ensures its structural balance for almost finitely enumerable code segments. We evaluate the efficiency of our CSBASG representation for Alloy models in terms of it's compactness compared to ASTs, and we explore if a CSBASG can ease the process of comparing two Alloy predicates. Moreover, with this representation in place, we identify several future applications of CSBASG, including Alloy code generation and automated repair.

cs.SE↗

arXiv2023

Structural Balance of Complex Weighted Graphs and Multi-partite Consensus

The structural balance of a signed graph is known to be necessary and sufficient to obtain a bipartite consensus among agents with friend-foe relationships. In the real world, relationships are multifarious, and the coexistence of different opinions is ubiquitous. We are therefore motivated to study the multi-partite consensus problem of multi-agent systems, for which we extend the concept of structural balance to graphs with complex edge weights. It is shown that the generalized structural balance property is necessary and sufficient for achieving multi-partite consensus.

eess.SY↗