arXiv subjects

Shengyi Wang

Publications and source records attributed to Shengyi Wang.

10 recordsLinked to original sources

arXiv2026

Seismic P-wave attenuation estimation based on frequency-dependent AVO using Kramers-Kronig relations for gas reservoir prediction

Estimation of seismic attenuation (inverse quality factor) is important for gas reservoir prediction. Two key issues in seismic attenuation estimation are the development of a physically consistent reflection coefficient equation and stable estimation of seismic attenuation from seismic data. To address these issues, this study, within the framework of isotropic linear viscoelastic media, starts from the Kramers-Kronig relations and expresses the viscoelastic stiffness matrix as a function of seismic attenuation. Under the assumptions of weak attenuation and small elastic and attenuation contrasts across the interface, a frequency-dependent PP-wave reflection coefficient equation explicitly containing seismic attenuation terms is derived using scattering theory. The derived reflection coefficient equation not only satisfies the causality constraint, but also preserves a compact mathematical form. Based on this reflection coefficient equation, seismic attenuation is estimated within the framework of frequency-dependent AVO inversion. Synthetic seismic data tests show that the estimated P-wave attenuation attribute is sensitive to variations in reservoir gas saturation, with reservoirs of higher gas saturation exhibiting stronger P-wave attenuation anomalies. Application to field seismic data further demonstrates that the P-wave attenuation anomalies agree well with the gas saturation log and effectively identify high gas saturation reservoirs. This study provides a new approach for extracting P-wave attenuation information from seismic data and achieving high resolution prediction of gas reservoirs.

physics.geo-ph↗

arXiv2026

FilmBench: A Film-Grade Benchmark for Cinematic Video Generation

Progress in video generation keeps narrowing the visual gap between AI-generated and professionally produced footage, yet most benchmarks still draw prompts from web sources or LLM templates and score them with untrained, generic multimodal models. More fundamentally, their evaluation taxonomies remain rudimentary (overall visual quality, coarse text alignment and temporal smoothness) rather than the professional Cinematic Language criteria by which films are actually made and judged, so they assess basic video plausibility rather than film-grade craft. We introduce FilmBench, a text-to-video (T2V) and reference-to-video (R2V) benchmark grounded in the professional Cinematic Language of the film- academy tradition and co-developed with directors and faculty from the Beijing Film Academy and the Hujing Digital Media & Entertainment Group film studio. It rests on three choices. First, prompts are reverse-engineered from clips of award-winning films spanning 20 cinematic genres and chosen by professional directors, so every prompt is anchored to a verified live-action reference; the prompts follow real shot lists, and most script multiple shots (1,056 of the 1,169 prompts are multi-shot), unlike prior single-clip benchmarks. Second, evaluation follows a three-level Cinematic taxonomy of 3 axes, 12 components and 35 (T2V) +3 (R2V-only) sub-metrics. Third, we develop an in-house expert-grade automatic evaluation agent and open-source its core suite of Cinematic Language operators (FilmOps). Benchmarking leading video generation models (9 for T2V, 7 for R2V), the evaluator reproduces the human model ranking at model-level Spearman \r{ho} = 0.95 (T2V) and 0.96 (R2V). Scores fall well below prior web-style benchmarks, with two consistent gaps in dynamic aesthetics and a marked single- to multi-shot performance drop that widens for weaker models.

cs.CV↗

arXiv2026

From Patterns to Maze Structures: SMT-Based Path Synthesis and 2D/3D Construction

We present a pipeline for constructing maze structures from input patterns such as text or shapes. The central path-synthesis problem is encoded in Satisfiability Modulo Theories as global constraints on adjacency, continuity, and pattern-constrained coverage, allowing each fixed-bound instance to be solved in one call. The resulting path is either a planar, self-avoiding route or a layered traversal with prescribed over--under crossings, and it serves as a scaffold for constructing planar mazes and three-dimensional realizations of woven mazes. This report extends the published Bridges 2026 conference paper with more representative SMT-LIB examples and a fuller account of how synthesized paths become concrete maze constructions in planar and three-dimensional form.

cs.AI↗

arXiv2026

AI-Assisted Completion of CertiGC Proofs: An Experience Report

This experience report describes the Codex-assisted completion and stabilization of a substantial Rocq (formerly Coq) proof development for CertiGC, the verified generational garbage collector in the CertiGraph project. The development extends the collector from an effectively immutable setting to a mutable one by adding remembered-set forwarding to the collection path and re-establishing the top-level graph-isomorphism correctness theorem. The central technical issue was not low-level proof scripting alone: mutable updates invalidate the old global no-backward-edge assumption, so the proof had to be reorganized around a recorded-backward-edge invariant stating that every backward edge is recorded in the appropriate remembered-set component. This case differs from recent AI-assisted formal-proof accounts: unlike the adaptation of a nearby compilerproof architecture or a fresh metatheory formalization, it completes a long-running verification in a mature codebase built on the Verified Software Toolchain (VST) and CertiGraph, both mechanized in Rocq. The Rocq kernel remained the arbiter of correctness, while our role shifted toward adjudicating invariant proposals, constraining specification changes, reviewing theorem statements, and deciding when proof cleanup was justified. The Codex-assisted phase repaired the VST relation proofs first, then restored the mathematical graph-isomorphism theorem, and only then audited the premise path from the VST specification to the theorem. That audit found and removed a stale no-backward-edge condition from the VST-facing proof path. This report presents the workflow, resulting proof artifact, and lessons for agentic proof maintenance.

cs.PL↗

arXiv2024

Comprehensive Verification of Packet Processing

To prove the functional correctness of a P4 program running in a programmable network switch or smart NIC, prior works have focused mainly on verifiers for the "control block" (match-action pipeline). But to verify that a switch handles packets according to a desired specification, proving the control block is not enough. We demonstrate a new comprehensive framework for formally specifying and proving the additional components of the switch that handle each packet: P4 parsers and deparsers, as well as non-P4 components such as multicast engines, packet generators, and resubmission paths. These are generally triggered by having the P4 program set header or metadata fields, which prompt other switch components -- fixed-function or configurable -- to execute the corresponding actions. Overall behavior is correct only if the "configurable" components are, indeed, configured properly; and we show how to prove that. We demonstrate our framework by verifying the correctness of packet-stream behavior in two classic P4 applications. Our framework is the first to allow the correctness proof of a P4 program to be composed with the correctness proof for these other switch components to verify that the switch programming as a whole accomplishes a specified behavior.

cs.PL↗

arXiv2023

Proving Logical Atomicity using Lock Invariants

Logical atomicity has been widely accepted as a specification format for data structures in concurrent separation logic. While both lock-free and lock-based data structures have been verified against logically atomic specifications, most of the latter start with atomic specifications for the locks as well. In this paper, we compare this approach with one based on older lock-invariant-based specifications for locks. We show that we can still prove logically atomic specifications for data structures with fine-grained locking using these older specs, but the proofs are significantly more complicated than those that use atomic lock specifications. Our proof technique is implemented in the Verified Software Toolchain, which relies on older lock specifications for its soundness proof, and applied to C implementations of lock-based concurrent data structures.

cs.PL↗

arXiv2023

GeoGauss: Strongly Consistent and Light-Coordinated OLTP for Geo-Replicated SQL Database

Multinational enterprises conduct global business that has a demand for geo-distributed transactional databases. Existing state-of-the-art databases adopt a sharded master-follower replication architecture. However, the single-master serving mode incurs massive cross-region writes from clients, and the sharded architecture requires multiple round-trip acknowledgments (e.g., 2PC) to ensure atomicity for cross-shard transactions. These limitations drive us to seek yet another design choice. In this paper, we propose a strongly consistent OLTP database GeoGauss with full replica multi-master architecture. To efficiently merge the updates from different master nodes, we propose a multi-master OCC that unifies data replication and concurrent transaction processing. By leveraging an epoch-based delta state merge rule and the optimistic asynchronous execution, GeoGauss ensures strong consistency with light-coordinated protocol and allows more concurrency with weak isolation, which are sufficient to meet our needs. Our geo-distributed experimental results show that GeoGauss achieves 7.06X higher throughput and 17.41X lower latency than the state-of-the-art geo-distributed database CockroachDB on the TPC-C benchmark.

cs.DB↗

arXiv2023

A Novel Efficient Signcryption Scheme for Resource-Constrained Smart Terminals in Cyber-Physical Power Systems

Most of the existing signcryption schemes generate pseudonym by key generation center (KGC) and usually choose bilinear pairing to construct authentication schemes. The drawback is that these schemes not only consume heavy computation and communication costs during information exchange, but also can not eliminate security risks due to not updating pseudonym, which do not work well for resource-constrained smart terminals in cyber-physical power systems (CPPSs). The main objective of this paper is to propose a novel efficient signcryption scheme for resource-constrained smart terminals. First, a dynamical pseudonym self-generation mechanism (DPSGM) is explored to achieve privacy preservation and avoid the source being linked. Second, combined with DPSGM, an efficient signcryption scheme based on certificateless cryptography (CLC) and elliptic curve cryptography (ECC) is designed, which reduces importantly computation and communication burden. Furthermore, under random oracle model (ROM), the confidentiality and non-repudiation of the proposed signcryption scheme are transformed into elliptic curve discrete logarithm and computational Diffie-Hellman problems that cannot be solved in polynomial time, which guarantees the security. Finally, the effectiveness and feasibility of the proposed signcryption scheme are confirmed by experimental analyses.

cs.CR↗

arXiv2019

BesFS: A POSIX Filesystem for Enclaves with a Mechanized Safety Proof

New trusted computing primitives such as Intel SGX have shown the feasibility of running user-level applications in enclaves on a commodity trusted processor without trusting a large OS. However, the OS can still compromise the integrity of an enclave by tampering with the system call return values. In fact, it has been shown that a subclass of these attacks, called Iago attacks, enables arbitrary logic execution in enclave programs. Existing enclave systems have very large TCB and they implement ad-hoc checks at the system call interface which are hard to verify for completeness. To this end, we present BesFS--the first filesystem interface which provably protects the enclave integrity against a completely malicious OS. We prove 167 lemmas and 2 key theorems in 4625 lines of Coq proof scripts, which directly proves the safety properties of the BesFS specification. BesFS comprises of 15 APIs with compositional safety and is expressive enough to support 31 real applications we test. BesFS integrates into existing SGX-enabled applications with minimal impact to TCB. BesFS can serve as a reference implementation for hand-coded API checks.

cs.CR↗

arXiv2019

Proof Pearl: Magic Wand as Frame

Separation logic adds two connectives to assertion languages: separating conjunction * ("star") and its adjoint, separating implication -* ("magic wand"). Comparatively, separating implication is less widely used. This paper demonstrates that by using magic wand to express frames that relate mutable local portions of data structures to global portions, we can exploit its power while proofs are still easily understandable. Many useful separation logic theorems about partial data structures can now be proved by simple automated tactics, which were usually proved by induction. This magic-wand-as-frame technique is especially useful when formalizing the proofs by a high order logic. We verify binary search tree insert in Coq as an example to demonstrate this proof technique.

cs.PL↗