Cover Image

Correctness Witnesses with Function Contracts

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Heizmann, Matthias, Klumpp, Dominik, Lingsch-Rosenfeld, Marian, Schüssele, Frank
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

SV-LIB 1.0: A Standard Exchange Format for Software-Verification Tasks
by: Beyer, Dirk, et al.
Published: (2025)

Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts (Extended Version)
by: Erhard, Julian, et al.
Published: (2024)

The Ghosts of Empires: Extracting Modularity from Interleaving-Based Proofs (Extended Version)
by: Schüssele, Frank, et al.
Published: (2025)

SoliDiffy: AST Differencing for Solidity Smart Contracts
by: Eshghie, Mojtaba, et al.
Published: (2024)

Contract Based Verification of Non-functional Requirements for Embedded Automotive C Code
by: Amilon, Jesper, et al.
Published: (2026)

Compilation Quotient (CQ): A Metric for the Compilation Hardness of Programming Languages
by: Szabo, Violet, et al.
Published: (2024)

Demystifying Invariant Effectiveness for Securing Smart Contracts
by: Chen, Zhiyang, et al.
Published: (2024)

Detecting Buggy Contracts via Smart Testing
by: Wang, Sally Junsong, et al.
Published: (2024)

KAIJU: An Executive Kernel for Intent-Gated Execution of LLM Agents
by: Guerin, Cormac, et al.
Published: (2026)

Can Large Language Models Help Students Prove Software Correctness? An Experimental Study with Dafny
by: Carreira, Carolina, et al.
Published: (2025)

Is Functional Correctness Enough to Evaluate Code Language Models? Exploring Diversity of Generated Codes
by: Chon, Heejae, et al.
Published: (2024)

SmartInv: Multimodal Learning for Smart Contract Invariant Inference
by: Wang, Sally Junsong, et al.
Published: (2024)

Kernel-FFI: Transparent Foreign Function Interfaces for Interactive Notebooks
by: Li, Hebi, et al.
Published: (2025)

Belobog: Move Language Fuzzing Framework For Real-World Smart Contracts
by: Kong, Ziqiao, et al.
Published: (2025)

Programmable Property-Based Testing
by: Keles, Alperen, et al.
Published: (2026)

On the Anatomy of Real-World R Code for Static Analysis
by: Sihler, Florian, et al.
Published: (2024)

Contract Usage and Evolution in Android Mobile Applications
by: Ferreira, David R., et al.
Published: (2024)

Beyond Postconditions: Can Large Language Models infer Formal Contracts for Automatic Software Verification?
by: Richter, Cedric, et al.
Published: (2025)

OpenTracer: A Dynamic Transaction Trace Analyzer for Smart Contract Invariant Generation and Beyond
by: Chen, Zhiyang, et al.
Published: (2024)

Functional Consistency of LLM Code Embeddings: A Self-Evolving Data Synthesis Framework for Benchmarking
by: Li, Zhuohao, et al.
Published: (2025)

Software Verification with CPAchecker 3.0: Tutorial and User Guide (Extended Version)
by: Baier, Daniel, et al.
Published: (2024)

Correctness-Guaranteed Code Generation via Constrained Decoding
by: Li, Lingxiao, et al.
Published: (2025)

Hydra: Efficient, Correct Code Generation via Checkpoint-and-Rollback Support
by: Du, Alexander, et al.
Published: (2026)

Learning to Guarantee Type Correctness in Code Generation through Type-Guided Program Synthesis
by: Huang, Zhechong, et al.
Published: (2025)

LecPrompt: A Prompt-based Approach for Logical Error Correction with CodeBERT
by: Xu, Zhenyu, et al.
Published: (2024)

Stdlib or Third-Party? Empirical Performance and Correctness of LLM-Assisted Zero-Dependency Python Libraries
by: Ding, Peng, et al.
Published: (2026)

Flexible Correct-by-Construction Programming
by: Runge, Tobias, et al.
Published: (2022)

SACTOR: LLM-Driven Correct and Idiomatic C to Rust Translation with Static Analysis and FFI-Based Verification
by: Zhou, Tianyang, et al.
Published: (2025)

Automatically Testing Functional Properties of Code Translation Models
by: Eniser, Hasan Ferit, et al.
Published: (2023)

Verification Modulo Tested Library Contracts
by: Uppar, Abhishek, et al.
Published: (2026)

From Code to Correctness: Closing the Last Mile of Code Generation with Hierarchical Debugging
by: Shi, Yuling, et al.
Published: (2024)

Getting Python Types Right with RightTyper
by: Pizzorno, Juan Altmayer, et al.
Published: (2025)

The CodeInverter Suite: Control-Flow and Data-Mapping Augmented Binary Decompilation with LLMs
by: Liu, Peipei, et al.
Published: (2025)

An Encoding of Interaction Nets in OCaml
by: Huber, Nikolaus, et al.
Published: (2025)

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

LitmusKt: Concurrency Stress Testing for Kotlin
by: Lochmelis, Denis, et al.
Published: (2025)

Literate Tracing
by: Sotoudeh, Matthew
Published: (2025)

EPSO: A Caching-Based Efficient Superoptimizer for BPF Bytecode
by: Zhu, Qian, et al.
Published: (2025)

Execution-Aware Program Reduction for WebAssembly via Record and Replay
by: Baek, Doehyun, et al.
Published: (2025)

RacerF: Lightweight Static Data Race Detection for C Code
by: Dacík, Tomáš, et al.
Published: (2025)