Imagen de Portada

Array-Carrying Symbolic Execution for Function Contract Generation

Fuente: arXiv

Guardado en:

Detalles Bibliográficos
Autores principales:	Lu, Weijie, Ke, Jingyu, Fu, Hongfei, Sun, Zhouyue, Zhou, Yi, Li, Guoqiang, Li, Haokun
Formato:	Preprint
Publicado:	2026
Materias:	Programming Languages Logic in Computer Science Software Engineering 68Q60, 68N30 D.2.4; F.3.1
Acceso en línea:	Acceder al recurso
Etiquetas:	Agregar Etiqueta Sin Etiquetas, Sea el primero en etiquetar este registro!

Ejemplares similares

Multiple Query Satisfiability of Constrained Horn Clauses
por: De Angelis, Emanuele, et al.
Publicado: (2022)

Contract-based Verification of Digital Twins
por: Naeem, Muhammad, et al.
Publicado: (2025)

A Complete Fragment of LTL(EB)
por: Ferrarotti, Flavio, et al.
Publicado: (2024)

Tridirectional Discriminating-Power Formal Verification of Smart Contract Reentrancy Defense Against Production-Deployed Solidity Source
por: Iskander, Ray
Publicado: (2026)

On systematic construction of correct logic programs
por: Drabent, Włodzimierz
Publicado: (2025)

Formal Verification of Imperative First-Class Functions in Move
por: Grieskamp, Wolfgang, et al.
Publicado: (2026)

Monitoring Hyperproperties over Observed and Constructed Traces
por: Chalupa, Marek, et al.
Publicado: (2025)

Imandra CodeLogician: Neuro-Symbolic Reasoning for Precise Analysis of Software Logic
por: Lin, Hongyu, et al.
Publicado: (2026)

Understanding and Improving Automated Proof Synthesis for Interactive Theorem Provers
por: Zhang, Manqing, et al.
Publicado: (2026)

cozy: Comparative Symbolic Execution for Binary Programs
por: Helbling, Caleb, et al.
Publicado: (2025)

Combining Mechanical and Agentic Specification Inference for Move
por: Grieskamp, Wolfgang, et al.
Publicado: (2026)

A Qualitative Analysis of Kernel Extension for Higher Order Proof Checking
por: Wang, Shuai
Publicado: (2024)

Type Inference for Isabelle2Cpp
por: Jiang, Dongchen, et al.
Publicado: (2024)

Truth-Aware Decoding: A Program-Logic Approach to Factual Language Generation
por: Alpay, Faruk, et al.
Publicado: (2025)

Finding a Crab in the C: Assured Translation via Comparative Symbolic Execution
por: Helbling, Caleb, et al.
Publicado: (2026)

Principal Types as Partial Involutions
por: Honsell, Furio, et al.
Publicado: (2024)

Simulating and model checking membrane systems using strategies in Maude
por: Rubio, Rubén, et al.
Publicado: (2024)

Proof-Carrying Certificates for LLM Pipelines: A Trust-Boundary Architecture
por: Koomullil, George
Publicado: (2026)

From CRUD to Autonomous Agents: Formal Validation and Zero-Trust Security for Semantic Gateways in AI-Native Enterprise Systems
por: Peyrano, Ignacio
Publicado: (2026)

Minimalistic System Modelling: Behaviours, Interfaces, and Local Reasoning
por: Galmiche, Didier, et al.
Publicado: (2024)

BRIDGE: Building Representations In Domain Guided Program Synthesis
por: George, Robert Joseph, et al.
Publicado: (2025)

Generalised Möbius Categories and Convolution Kleene Algebras
por: Cranch, James, et al.
Publicado: (2025)

Executable Boundary Contracts for Sound Event Traces
por: Alpay, Faruk, et al.
Publicado: (2026)

Jean-Raymond Abrial: A Scientific Biography of a Formal Methods Pioneer
por: Bowen, Jonathan P., et al.
Publicado: (2026)

NOETHER: A Constructive Framework for Metamorphic Pattern Discovery from Operator Algebras
por: Li, Meng, et al.
Publicado: (2026)

Dynamic Symbolic Execution for Semantic Difference Analysis of Component and Connector Architectures
por: Grahl, Johanna, et al.
Publicado: (2025)

There is a deep 1-generic set
por: Li, Ang
Publicado: (2024)

Proof-Carrying Verification for ReLU Networks via Rational Certificates
por: Gokavarapu, Chandrasekhar
Publicado: (2025)

AI for software engineering: from probable to provable
por: Meyer, Bertrand
Publicado: (2025)

On Woolhouse's Cotton-Spinning Problem
por: Groote, Jan Friso, et al.
Publicado: (2024)

Strategies, model checking and branching-time properties in Maude
por: Rubio, Rubén, et al.
Publicado: (2024)

Model checking strategy-controlled systems in rewriting logic
por: Rubio, Rubén, et al.
Publicado: (2024)

Optimal matching for sharing and linearity analysis
por: Amato, Gianluca, et al.
Publicado: (2024)

ABox Abduction for Inconsistent Knowledge Bases under Repair Semantics
por: Haak, Anselm, et al.
Publicado: (2026)

Compositionality of Lyapunov functions via assume-guarantee reasoning
por: Capucci, Matteo, et al.
Publicado: (2026)

Behavioural Theory of Reflective Algorithms II: Reflective Parallel Algorithms
por: Schewe, Klaus-Dieter, et al.
Publicado: (2025)

Incremental Certificate Learning for Hybrid Neural Network Verification . A Solver Architecture for Piecewise-Linear Safety Queries
por: Gokavarapu, Chandrasekhar
Publicado: (2025)

QSeqSim: A Symbolic Simulator for Qiskit While Loops Using Sequential Quantum Circuits
por: Li, Zihao, et al.
Publicado: (2026)

Flavors of Quantifiers in Hyperlogics
por: Chalupa, Marek, et al.
Publicado: (2025)

Formal Foundations for Controlled Stochastic Activity Networks
por: Movaghar, Ali
Publicado: (2025)