Cover Image

A Tale of 1001 LoC: Potential Runtime Error-Guided Specification Synthesis for Verifying Large-Scale Programs

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Wang, Zhongyi, Lin, Tengjie, Chen, Mingshuai, Li, Haokun, Yang, Mingqi, Yi, Xiao, Qin, Shengchao, Luo, Yixing, Li, Xiaofeng, Gu, Bin, Lu, Liqiang, Yin, Jianwei
Format:	Preprint
Published:	2025
Subjects:	Software Engineering Logic in Computer Science
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Preguss: It Analyzes, It Specifies, It Verifies
by: Wang, Zhongyi, et al.
Published: (2025)

Parf: Adaptive Parameter Refining for Abstract Interpretation
by: Wang, Zhongyi, et al.
Published: (2024)

Verifying Exact Samplers for Continuous Distributions with a Discrete Program Logic
by: de Medeiros, Markus, et al.
Published: (2026)

Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions
by: Klinkenberg, Lutz, et al.
Published: (2023)

VerifyThis 2019: A Program Verification Competition (Extended Report)
by: Dross, Claire, et al.
Published: (2020)

Verifying Floating-Point Programs in Stainless
by: Gilot, Andrea, et al.
Published: (2026)

Distributionally Robust Predictive Runtime Verification under Spatio-Temporal Logic Specifications
by: Zhao, Yiqi, et al.
Published: (2025)

Verifying Solutions to Semantics-Guided Synthesis Problems
by: Murphy, Charlie, et al.
Published: (2024)

PARF: An Adaptive Abstraction-Strategy Tuner for Static Analysis
by: Wang, Zhongyi, et al.
Published: (2025)

Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs
by: Aguirre, Alejandro, et al.
Published: (2024)

Runtime Verification of Interactions Using Automata
by: Weil-Kennedy, Chana, et al.
Published: (2025)

Runtime Verification for LTL in Stochastic Systems
by: Esparza, Javier, et al.
Published: (2025)

On Deciding Constant Runtime of Linear Loops
by: Frohn, Florian, et al.
Published: (2026)

Separation Logic for Verifying Physical Collisions of CNC Programs
by: Lee, Yeonseok
Published: (2026)

A Weakest Precondition Calculus for Programs and Linear Temporal Specifications
by: Ernst, Gidon
Published: (2026)

Learning Robust Markov Models for Safe Runtime Monitoring
by: Skurka, Antonina, et al.
Published: (2026)

Active Monitoring with RTLola: A Specification-Guided Scheduling Approach
by: Baumeister, Jan, et al.
Published: (2025)

Differentially Private Runtime Monitoring
by: Finkbeiner, Bernd, et al.
Published: (2026)

Varanus: Runtime Verification for CSP
by: Luckcuck, Matt, et al.
Published: (2025)

Bit-Vector Abstractions to Formally Verify Quantum Error Detection & Entanglement
by: Govindankutty, Arun
Published: (2026)

Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs (Extended Version)
by: Li, Kwing Hei, et al.
Published: (2025)

A Fibrational Tale of Operational Logical Relations: Pure, Effectful and Differential
by: Dagnino, Francesco, et al.
Published: (2023)

POLIMON: Checking Temporal Properties over Out-of-order Streams at Runtime
by: Klaedtke, Felix
Published: (2024)

RTAMT -- Runtime Robustness Monitors with Application to CPS and Robotics
by: Yamaguchi, Tomoya, et al.
Published: (2025)

The Shape of $\mathcal{EL}$ Proofs: A Tale of Three Calculi (Extended Version)
by: Alrabbaa, Christian, et al.
Published: (2025)

Verifying Numerical Methods with Isabelle/HOL
by: Bryant, Dustin, et al.
Published: (2025)

Programs as Singularities
by: Murfet, Daniel, et al.
Published: (2025)

Satisfiability Modulo Theories for Verifying MILP Certificates
by: Wood, Kenan, et al.
Published: (2023)

Wait-Only Broadcast Protocols are Easier to Verify
by: Guillou, Lucie, et al.
Published: (2025)

Verified and Optimized Implementation of Orthologic Proof Search
by: Guilloud, Simon, et al.
Published: (2025)

A-IC3: Learning-Guided Adaptive Inductive Generalization for Hardware Model Checking
by: Zhou, Xiaofeng, et al.
Published: (2026)

A Hybrid SMT-NRA Solver: Integrating 2D Cell-Jump-Based Local Search, MCSAT and OpenCAD
by: Ding, Tianyi, et al.
Published: (2025)

Verifying Procedural Programs via Constrained Rewriting Induction
by: Fuhs, Carsten, et al.
Published: (2014)

Dependency Pairs for Expected Innermost Runtime Complexity and Strong Almost-Sure Termination of Probabilistic Term Rewriting
by: Kassing, Jan-Christoph, et al.
Published: (2025)

Risk-Aware MPC for Stochastic Systems with Runtime Temporal Logics
by: Engelaar, Maico H. W., et al.
Published: (2024)

An Imperative Language for Verified Exact Real-Number Computation
by: Bauer, Andrej, et al.
Published: (2024)

Verifying SQL Queries using Theories of Tables and Relations
by: Mohamed, Mudathir, et al.
Published: (2024)

Syntax-Guided Automated Program Repair for Hyperproperties
by: Beutner, Raven, et al.
Published: (2024)

Evaluating the Ability of Large Language Models to Generate Verifiable Specifications in VeriFast
by: Fan, Wen, et al.
Published: (2024)

Proof-theoretic Semantics for the Logic of Bunched Implications
by: Gu, Tao, et al.
Published: (2023)