arXiv subjects

Zhenjiang Hu

Publications and source records attributed to Zhenjiang Hu.

At least 19 recordsLinked to original sources

arXiv2025

Stellis: A Strategy Language for Purifying Separation Logic Entailments

Automatically proving separation logic entailments is a fundamental challenge in verification. While rule-based methods rely on separation logic rules (lemmas) for automation, these rule statements are insufficient for describing automation strategies, which usually involve the alignment and elimination of corresponding memory layouts in specific scenarios. To overcome this limitation, we propose Stellis, a strategy language for purifying separation logic entailments, i.e., removing all spatial formulas to reduce the entailment to a simpler pure entailment. Stellis features a powerful matching mechanism and a flexible action description, enabling the straightforward encoding of a wide range of strategies. To ensure strategy soundness, we introduce an algorithm that generates a soundness condition for each strategy, thereby reducing the soundness of each strategy to the correctness of its soundness condition. Furthermore, based on a mechanized reduction soundness theorem, our prototype implementation generates correctness proofs for the overall automation. We evaluate our system on a benchmark of 229 entailments collected from verification of standard linked data structures and the memory module of a microkernel, and the evaluation results demonstrate that, with such flexibility and convenience provided, our system is also highly effective, which automatically purifies 95.6% (219 out of 229) of the entailments using 5 libraries with 98 strategies.

cs.SE↗

arXiv2025

Functional design of efficient and parallelizable combinatorial generators using convolution

The application of program transformation and algebraic methods to the development of efficient combinatorial optimization (CO) algorithms relies on an exhaustive combinatorial generator for the problem specification, followed by the fusion of thinning or filtering processes into this specification. However, the effectiveness of such fusion transformations critically depends on the structural compatibility between the objective function and the generator, which is highly problem dependent. In practice, when the majority of candidate solutions remain unfiltered or are not eliminated-as is the case for most intractable CO problems-the overall efficiency of the resulting fused program is largely determined by the intrinsic efficiency of the combinatorial generator. Consequently, if the specification itself exhibits suboptimal performance, the fused program will inherit a correspondingly inferior level of efficiency. We argue that a genuine designed process should also account for hardware compatibility and parallelizability-particularly the ability to support efficient parallel execution on modern hardware architectures, including multi-level cache hierarchies and GPUs. However, does achieving formal correctness necessarily conflict with designing algebraically elegant algorithms that support fusion? Can we obtain both simultaneously? In this paper, we show that techniques from functional programming, provide powerful formal tools for the systematic construction of such hardware-compatible and parallelizable combinatorial generators. This paper investigates generators for two of the most fundamental combinatorial structures-combinations and permutations-together with their natural extension to nested generators (e.g., combinations/permutations of combinations/permutations).

cs.DM↗

arXiv2025

QCP: A Practical Separation Logic-based C Program Verification Tool

As software systems increase in size and complexity dramatically, ensuring their correctness, security, and reliability becomes an increasingly formidable challenge. Despite significant advancements in verification techniques and tools, their practical application to complex, real-world systems is often hindered by critical gaps in both automation and expressiveness. To address these difficulties, this paper presents \textbf{Qualified C Programming Verifier (QCP)}, a novel verification tool that integrates annotation-based automatic verification with interactive proving using Rocq. QCP employs symbolic execution and a separation logic entailment solver to automatically discharge many verification obligations, while deferring more complex obligations to Rocq for manual proof. Furthermore, QCP includes a VS Code extension designed to enhance proof efficiency and support a deeper understanding of both the program behavior and verification outcomes.

cs.PL↗

arXiv2025

C*: Unifying Programming and Verification in C

Ensuring the correct functionality of systems software, given its safety-critical and low-level nature, is a primary focus in formal verification research and applications. Despite advances in verification tooling, conventional programmers are rarely involved in the verification of their own code, resulting in higher development and maintenance costs for verified software. A key barrier to programmer participation in verification practices is the disconnect of environments and paradigms between programming and verification practices, which limits accessibility and real-time verification. We introduce C*, a proof-integrated language design for C programming. C* extends C with verification capabilities, powered by a symbolic execution engine and an LCF-style proof kernel. It enables real-time verification by allowing programmers to embed proof-code blocks alongside implementation code, facilitating interactive updates to the current proof state. Its expressive and extensible proof support allows users to build reusable libraries of logical definitions, theorems, and programmable proof automation. Crucially, C* unifies implementation and proof code development by using C as the common language. We implemented a prototype of C* and evaluated it on a representative benchmark of small C programs and a challenging real-world case study: the attach function of pKVM's buddy allocator. Our results demonstrate that C* supports the verification of a broad subset of C programming idioms and effectively handles complex reasoning tasks in real-world scenarios.

cs.PL↗

arXiv2024

LDA-AQU: Adaptive Query-guided Upsampling via Local Deformable Attention

Feature upsampling is an essential operation in constructing deep convolutional neural networks. However, existing upsamplers either lack specific feature guidance or necessitate the utilization of high-resolution feature maps, resulting in a loss of performance and flexibility. In this paper, we find that the local self-attention naturally has the feature guidance capability, and its computational paradigm aligns closely with the essence of feature upsampling (\ie feature reassembly of neighboring points). Therefore, we introduce local self-attention into the upsampling task and demonstrate that the majority of existing upsamplers can be regarded as special cases of upsamplers based on local self-attention. Considering the potential semantic gap between upsampled points and their neighboring points, we further introduce the deformation mechanism into the upsampler based on local self-attention, thereby proposing LDA-AQU. As a novel dynamic kernel-based upsampler, LDA-AQU utilizes the feature of queries to guide the model in adaptively adjusting the position and aggregation weight of neighboring points, thereby meeting the upsampling requirements across various complex scenarios. In addition, LDA-AQU is lightweight and can be easily integrated into various model architectures. We evaluate the effectiveness of LDA-AQU across four dense prediction tasks: object detection, instance segmentation, panoptic segmentation, and semantic segmentation. LDA-AQU consistently outperforms previous state-of-the-art upsamplers, achieving performance enhancements of 1.7 AP, 1.5 AP, 2.0 PQ, and 2.5 mIoU compared to the baseline models in the aforementioned four tasks, respectively. Code is available at \url{https://github.com/duzw9311/LDA-AQU}.

cs.CV↗

arXiv2024

Cross-Layer Feature Pyramid Transformer for Small Object Detection in Aerial Images

Object detection in aerial images has always been a challenging task due to the generally small size of the objects. Most current detectors prioritize the development of new detection frameworks, often overlooking research on fundamental components such as feature pyramid networks. In this paper, we introduce the Cross-Layer Feature Pyramid Transformer (CFPT), a novel upsampler-free feature pyramid network designed specifically for small object detection in aerial images. CFPT incorporates two meticulously designed attention blocks with linear computational complexity: Cross-Layer Channel-Wise Attention (CCA) and Cross-Layer Spatial-Wise Attention (CSA). CCA achieves cross-layer interaction by dividing channel-wise token groups to perceive cross-layer global information along the spatial dimension, while CSA enables cross-layer interaction by dividing spatial-wise token groups to perceive cross-layer global information along the channel dimension. By integrating these modules, CFPT enables efficient cross-layer interaction in a single step, thereby avoiding the semantic gap and information loss associated with element-wise summation and layer-by-layer transmission. In addition, CFPT incorporates global contextual information, which improves detection performance for small objects. To further enhance location awareness during cross-layer interaction, we propose the Cross-Layer Consistent Relative Positional Encoding (CCPE) based on inter-layer mutual receptive fields. We evaluate the effectiveness of CFPT on three challenging object detection datasets in aerial images: VisDrone2019-DET, TinyPerson, and xView. Extensive experiments demonstrate that CFPT outperforms state-of-the-art feature pyramid networks while incurring lower computational costs. The code is available at https://github.com/duzw9311/CFPT.

cs.CV↗

arXiv2024

Decomposition-Based Synthesis for Applying Divide-and-Conquer-Like Algorithmic Paradigms

Algorithmic paradigms such as divide-and-conquer (D&C) are proposed to guide developers in designing efficient algorithms, but it can still be difficult to apply algorithmic paradigms to practical tasks. To ease the usage of paradigms, many research efforts have been devoted to the automatic application of algorithmic paradigms. However, most existing approaches to this problem rely on syntax-based program transformations and thus put significant restrictions on the original program. In this paper, we study the automatic application of D&C and several similar paradigms, denoted as D&C-like algorithmic paradigms, and aim to remove the restrictions from syntax-based transformations. To achieve this goal, we propose an efficient synthesizer, named AutoLifter, which does not depend on syntax-based transformations. Specifically, the main challenge of applying algorithmic paradigms is from the large scale of the synthesized programs, and AutoLifter addresses this challenge by applying two novel decomposition methods that do not depend on the syntax of the input program, component elimination and variable elimination, to soundly divide the whole problem into simpler subtasks, each synthesizing a sub-program of the final program and being tractable with existing synthesizers. We evaluate AutoLifter on 96 programming tasks related to 6 different algorithmic paradigms. AutoLifter solves 82/96 tasks with an average time cost of 20.17 seconds, significantly outperforming existing approaches.

cs.PL↗

arXiv2023

Automating Thinning Theorem: Synthesizing Efficient Dynamic Programming Algorithms

Dynamic programming is an important optimization technique, but designing efficient dynamic programming algorithms can be difficult for even professional programmers. Thinning, a technique developed for systematically deriving efficient dynamic programming algorithms, has received much attention in studies because of its effectiveness for a large class of problems. Despite the success of thinning in theory, its practical usage is still limited because (1) applying thinning requires mathematical and algorithmic background, and (2) applying thinning solely may not be enough to generate algorithms as efficient as proposed by human experts. In this paper, we propose two approaches, MetHyl and MetHyl+, to resolve both problems. First, MetHyl automates the application of thinning via program synthesis and thus eliminates the burden to the user for applying thinning. Second, MetHyl+ integrates three rules into MetHyl that optimize three important factors on the time complexity of dynamic programming algorithms that are ignored by thinning, and thus make it able to automatically generate expert-level dynamic programming algorithms on many tasks. We evaluate our approaches on 37 tasks related to 16 optimization problems collected from Introduction to Algorithm, a popular textbook for algorithm courses. The results show that MetHyl+ achieves exponential speed-ups on 97.3% of tasks with an average time cost of less than one minute. Moreover, MetHyl+ generates algorithms that are as efficient as the reference programs provided by human experts on 70.3% of tasks.

cs.PL↗

arXiv2021

Occam Learning Meets Synthesis Through Unification

The generalizability of PBE solvers is the key to the empirical synthesis performance. Despite the importance of generalizability, related studies on PBE solvers are still limited. In theory, few existing solvers provide theoretical guarantees on generalizability, and in practice, there is a lack of PBE solvers with satisfactory generalizability on important domains such as conditional linear integer arithmetic (CLIA). In this paper, we adopt a concept from the computational learning theory, Occam learning, and perform a comprehensive study on the framework of synthesis through unification (STUN), a state-of-the-art framework for synthesizing programs with nested if-then-else operators. We prove that Eusolver, a state-of-the-art STUN solver, does not satisfy the condition of Occam learning, and then we design a novel STUN solver, PolyGen, of which the generalizability is theoretically guaranteed by Occam learning. We evaluate PolyGen on the domains of CLIA and demonstrate that PolyGen significantly outperforms two state-of-the-art PBE solvers on CLIA, Eusolver and Euphony, on both generalizability and efficiency.

cs.PL↗

arXiv2021

Analytical Differential Calculus with Integration

Differential lambda-calculus was first introduced by Thomas Ehrhard and Laurent Regnier in 2003. Despite more than 15 years of history, little work has been done on a differential calculus with integration. In this paper, we shall propose a differential calculus with integration from programming point of view. We show its good correspondence with mathematics, which is manifested by how we construct these reduction rules and how we preserve important mathematical theorems in our calculus. Moreover, we highlight applications of the calculus in incremental computation, automatic differentiation, and computation approximation.

cs.PL↗

arXiv2020

iPregel: Vertex-centric programmability vs memory efficiency and performance, why choose?

The vertex-centric programming model, designed to improve the programmability in graph processing application writing, has attracted great attention over the years. However, shared memory frameworks that implement the vertex-centric interface all expose a common tradeoff: programmability against memory efficiency and performance. Our approach, iPregel, preserves vertex-centric programmability, while implementing optimisations for performance, and designing these so they are transparent to a user's application code, hence not impacting programmability. In this paper, we evaluate iPregel against FemtoGraph, whose characteristics are identical, an asynchronous counterpart GraphChi and the vertex-subset-centric framework Ligra. Our experiments include three of the most popular vertex-centric benchmark applications over 4 real-world publicly accessible graphs, which cover orders of magnitude between a million to a billion edges, measuring execution time and peak memory usage. Finally, we evaluate the programmability of each framework by comparing against Google's original Pregel framework. Experiments demonstrate that iPregel, like FemtoGraph, does not sacrifice vertex-centric programmability for additional performance and memory efficiency optimisations, which contrasts against GraphChi and Ligra. Sacrificing vertex-centric programmability allowed the latter to benefit from substantial performance and memory efficiency gains. We demonstrate that iPregel is up to 2300 times faster than FemtoGraph, as well as generating a memory footprint up to 100 times smaller. Ligra and GraphChi are up to 17000 and 700 times faster than FemtoGraph but, when comparing against iPregel, this maximum speed-up drops to 10. Furthermore, with PageRank, iPregel is the fastest overall. For memory efficiency, iPregel provides the same memory efficiency as Ligra and 3 to 6 times lighter than GraphChi on average.

cs.DC↗

arXiv2020

Programmable View Update Strategies on Relations

View update is an important mechanism that allows updates on a view by translating them into the corresponding updates on the base relations. The existing literature has shown the ambiguity of translating view updates. To address this ambiguity, we propose a robust language-based approach for making view update strategies programmable and validatable. Specifically, we introduce a novel approach to use Datalog to describe these update strategies. We propose a validation algorithm to check the well-behavedness of the written Datalog programs. We present a fragment of the Datalog language for which our validation is both sound and complete. This fragment not only has good properties in theory but is also useful for solving practical view updates. Furthermore, we develop an algorithm for optimizing user-written programs to efficiently implement updatable views in relational database management systems. We have implemented our proposed approach. The experimental results show that our framework is feasible and efficient in practice.

cs.DB↗

arXiv2020

Early Validation of Cyber-Physical Space Systems via Multi-Concerns Integration

Cyber-physical space systems are engineered systems operating within physical space with design requirements that depend on space, e.g., regarding location or movement behavior. They are built from and depend upon the seamless integration of computation and physical components. Typical examples include systems where software-driven agents such as mobile robots explore space and perform actions to complete particular missions. Design of such a system often depends on multiple concerns expressed by different stakeholders, capturing different aspects of the system. We propose a model-driven approach supporting (a) separation of concerns during design, (b) systematic and semi-automatic integration of separately modeled concerns, and finally (c) early validation via statistical model checking. We evaluate our approach over two different case studies of cyber-physical space systems.

cs.SE↗

arXiv2020

Retentive Lenses

Based on Foster et al.'s lenses, various bidirectional programming languages and systems have been developed for helping the user to write correct data synchronisers. The two well-behavedness laws of lenses, namely Correctness and Hippocraticness, are usually adopted as the guarantee of these systems. While lenses are designed to retain information in the source when the view is modified, well-behavedness says very little about the retaining of information: Hippocraticness only requires that the source be unchanged if the view is not modified, and nothing about information retention is guaranteed when the view is changed. To address the problem, we propose an extension of the original lenses, called retentive lenses, which satisfy a new Retentiveness law guaranteeing that if parts of the view are unchanged, then the corresponding parts of the source are retained as well. As a concrete example of retentive lenses, we present a domain-specific language for writing tree transformations; we prove that the pair of get and put functions generated from a program in our DSL forms a retentive lens. We demonstrate the practical use of retentive lenses and the DSL by presenting case studies on code refactoring, Pombrio and Krishnamurthi's resugaring, and XML synchronisation.

cs.PL↗

arXiv2020

FastSV: A Distributed-Memory Connected Component Algorithm with Fast Convergence

This paper presents a new distributed-memory algorithm called FastSV for finding connected components in an undirected graph. Our algorithm simplifies the classic Shiloach-Vishkin algorithm and employs several novel and efficient hooking strategies for faster convergence. We map different steps of FastSV to linear algebraic operations and implement them with the help of scalable graph libraries. FastSV uses sparse operations to avoid redundant work and optimized MPI communication to avoid bottlenecks. The resultant algorithm shows high-performance and scalability as it can find the connected components of a hyperlink graph with over 134B edges in 30 seconds using 262K cores on a Cray XC40 supercomputer. FastSV outperforms the state-of-the-art algorithm by an average speedup of 2.21x (max 4.27x) on a variety of real-world graphs.

cs.DS↗

arXiv2019

Toward Co-existing Database Schemas based on Bidirectional Transformation

According to strong demands for rapid and reliable software delivery, co-existing database schema versions with multiple application versions are reality to contribute them. Current database management systems do not support co-existing schema versions in one database. Although a design of co-existing schema based on updatable view tables was previously proposed, its flexibility is limited due to pre-defined several restrictions to achieve data synchronization among schemas and handling independent unsynchronized data in each schema. In this preliminary report, we present a new approach for co-existing schemas based on bidirectional transformation. We explain the required properties to realize co-existing schemas, bidirectionality and totality. We show that the co-existing schemas can be implemented systematically by applying putback-based bidirectional transformation to satisfy both the bidirectionality and the totality. While the bidirectionality can be satisfied by applying bidirectional transformation, to satisfy the totality, extra functions need to be introduced. How to derive these extra functions is presented.

cs.DB↗

arXiv2019

Blockchain-based Bidirectional Updates on Fine-grained Medical Data

Electronic medical data sharing between stakeholders, such as patients, doctors, and researchers, can promote more effective medical treatment collaboratively. These sensitive and private data should only be accessed by authorized users. Given a total medical data, users may care about parts of them and other unrelated information might interfere with the user interested data search and increase the risk of exposure. Besides accessing these data, users may want to update them and propagate to other sharing peers so that all peers keep identical data after each update. To satisfy these requirements, in this paper we propose a medical data sharing architecture that addresses the permission control using smart contracts on the blockchain and splits data into fined grained pieces shared with different peers then synchronize full data and these pieces with bidirectional transformations. Medical data reside on each userś local database and permission related data are stored on smart contracts. Only all peers have gained the newest shared data after updates can they start to do next operations on it, which are enforced by smart contracts. Blockchain based immutable shared ledge enables users to trace data updates history. This paper can provide a new perspective to view full medical data as different slices to be shared with various peers but consistency after updates between them are still promised, which can protect the privacy and improve data search efficiency.

cs.SE↗

arXiv2018

Composing Optimization Techniques for Vertex-Centric Graph Processing via Communication Channels

Pregel's vertex-centric model allows us to implement many interesting graph algorithms, where optimization plays an important role in making it practically useful. Although many optimizations have been developed for dealing with different performance issues, it is hard to compose them together to optimize complex algorithms, where we have to deal with multiple performance issues at the same time. In this paper, we propose a new approach to composing optimizations, by making use of the \emph{channel} interface, as a replacement of Pregel's message passing and aggregator mechanism, which can better structure the communication in Pregel algorithms. We demonstrate that it is convenient to optimize a Pregel program by simply using a proper channel from the channel library or composing them to deal with multiple performance issues. We intensively evaluate the approach through many nontrivial examples. By adopting the channel interface, our system achieves an all-around performance gain for various graph algorithms. In particular, the composition of different optimizations makes the S-V algorithm 2.20x faster than the current best implementation.

cs.DC↗