Cover Image

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

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Wu, Xiwei, Feng, Yueyang, Lu, Xiaoyang, Lin, Tianchuan, Liu, Kan, Wang, Zhiyi, Wu, Shushu, Xie, Lihan, Yang, Chengxi, Zhong, Hongyi, Zhang, Zihan, Li, Juanru, Zhan, Naijun, Hu, Zhenjiang, Cao, Qinxiang
Format:	Preprint
Published:	2025
Subjects:	Programming Languages Software Engineering
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

artifact-57-QCP: A Practical Separation Logic-based C Program Verification Tool
by: Wu, Xiwei
Published: (2025)

Stellis: A Strategy Language for Purifying Separation Logic Entailments
by: Wang, Zhiyi, et al.
Published: (2025)

Encode the $\forall\exists$ Relational Hoare Logic into Standard Hoare Logic
by: Wu, Shushu, et al.
Published: (2025)

A Formal Framework for Naturally Specifying and Verifying Sequential Algorithms
by: Yang, Chengxi, et al.
Published: (2025)

A Coq Library of Sets for Teaching Denotational Semantics
by: Cao, Qinxiang, et al.
Published: (2024)

C*: Unifying Programming and Verification in C
by: Cao, Yiyuan, et al.
Published: (2025)

Towards General Loop Invariant Generation: A Benchmark of Programs with Memory Manipulation
by: Liu, Chang, et al.
Published: (2023)

A Natural Formalized Proof Language
by: Xie, Lihan, et al.
Published: (2024)

Integrating Symbolic Execution with LLMs for Automated Generation of Program Specifications
by: Yang, Fanpeng, et al.
Published: (2025)

Denotation-based Compositional Compiler Verification
by: Cheng, Zhang, et al.
Published: (2024)

A Generalized Hybrid Hoare Logic
by: Zhan, Naijun, et al.
Published: (2023)

Synthesizing Invariants for Polynomial Programs by Semidefinite Programming
by: Wu, Hao, et al.
Published: (2023)

Nonlinear Craig Interpolant Generation over Unbounded Domains by Separating Semialgebraic Sets
by: Wu, Hao, et al.
Published: (2024)

Piecewise Analysis of Probabilistic Programs via $k$-Induction
by: Yang, Tengshun, et al.
Published: (2024)

Runtime Enforcement of CPS against Signal Temporal Logic
by: Su, Han, et al.
Published: (2025)

Neuro-Symbolic Generation and Validation of Memory-Aware Formal Function Specifications
by: Zhang, Liao, et al.
Published: (2026)

Verification Algorithms for Automated Separation Logic Verifiers
by: Eilers, Marco, et al.
Published: (2024)

RESTL: Reinforcement Learning Guided by Multi-Aspect Rewards for Signal Temporal Logic Transformation
by: Fang, Yue, et al.
Published: (2025)

Mars 2.0: A Toolchain for Modeling, Analysis, Verification and Code Generation of Cyber-Physical Systems
by: Zhan, Bohua, et al.
Published: (2024)

Accounting for Expected Cost Savings and Synergy Gains: The Role of Lenders’ Risk Preferences
by: Shushu Jiang
Published: (2026)

{log}: From a Constraint Logic Programming Language to a Formal Verification Tool
by: Cristiá, Maximiliano, et al.
Published: (2025)

Enhancing Transformation from Natural Language to Signal Temporal Logic Using LLMs with Diverse External Knowledge
by: Fang, Yue, et al.
Published: (2025)

THE U/RI-INDUSTRY LINKAGE AND THE DEVELOPMENT OF THE COMPUTER INDUSTRY IN CHINA
by: Xiwei Zhong
Published: (2006)

La reforma del Sistema de Ciencia y Tecnología y su impacto en el Sistema Nacional de Innovación de China
by: Zhong Xiwei
Published: (2007)

Compositional Verification in Concurrent Separation Logic with Permissions Regions
by: Le, Quang Loc
Published: (2025)

CRFU: Compressive Representation Forgetting Against Privacy Leakage on Machine Unlearning
by: Wang, Weiqi, et al.
Published: (2025)

Bayesian Separation Logic
by: Ho, Shing Hin, et al.
Published: (2025)

Solving Stochastic Constraints by Oracle-based Gradient Descent and Interval Arithmetic
by: Li, Xiakun, et al.
Published: (2026)

Sound State Encodings in Translational Separation Logic Verifiers (Extended Version)
by: Ling, Hongyi, et al.
Published: (2026)

Switching Controller Synthesis for Hybrid Systems Against STL Formulas
by: Su, Han, et al.
Published: (2024)

HHLPar: Automated Theorem Prover for Parallel Hybrid Communicating Sequential Processes
by: Jin, Xiangyu, et al.
Published: (2024)

Adaptive Mesh Generation and Numerical Verification for Complex Rock Structures Based on Optimization and Iteration Algorithms
by: Huaiguang Xiao, et al.
Published: (2024)

Learner and Instructor Needs in AI-Supported Programming Learning Tools: Design Implications for Features and Adaptive Control
by: Wu, Zihan, et al.
Published: (2025)

Quantitative Verification of Fairness in Tree Ensembles
by: Zhao, Zhenjiang, et al.
Published: (2025)

Structural Temporal Logic for Mechanized Program Verification
by: Ioannidis, Eleftherios, et al.
Published: (2024)

FO-Complete Program Verification for Heap Logics
by: Murali, Adithya, et al.
Published: (2026)

Exact Moment Estimation of Stochastic Differential Dynamics
by: Feng, Shenghua, et al.
Published: (2026)

SENTIL: A Runtime Verification Tool for Probabilistic Temporal Logic
by: Quansah, Paapa Kwesi, et al.
Published: (2026)

Practical Formal Verification for MLIR Programs
by: Tucker, Emily, et al.
Published: (2026)

Environmental scanning, resource orchestration, and disruptive innovation
by: Shumo Jin, et al.
Published: (2024)