Buchumschlag

Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language (extended version)

Fuente: arXiv

Gespeichert in:

Bibliographische Detailangaben
Hauptverfasser:	Parthasarathy, Gaurav, Dardinier, Thibault, Bonneau, Benjamin, Müller, Peter, Summers, Alexander J.
Format:	Preprint
Veröffentlicht:	2024
Schlagworte:	Programming Languages
Online-Zugang:	Acceder al recurso
Tags:	Tag hinzufügen Keine Tags, Fügen Sie den ersten Tag hinzu!

Ähnliche Einträge

Formal Foundations for Translational Separation Logic Verifiers (extended version)
von: Dardinier, Thibault, et al.
Veröffentlicht: (2024)

Hyper Separation Logic (extended version)
von: Gospodinov, Trayan, et al.
Veröffentlicht: (2026)

Sound State Encodings in Translational Separation Logic Verifiers (Extended Version)
von: Ling, Hongyi, et al.
Veröffentlicht: (2026)

Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (extended version)
von: Dardinier, Thibault, et al.
Veröffentlicht: (2023)

Verification Algorithms for Automated Separation Logic Verifiers
von: Eilers, Marco, et al.
Veröffentlicht: (2024)

Minuska: Towards a Formally Verified Programming Language Framework
von: Tušil, Jan, et al.
Veröffentlicht: (2024)

Towards Automated Verification of LLM-Synthesized C Programs
von: Mukherjee, Prasita, et al.
Veröffentlicht: (2024)

Towards Formal Verification of Hybrid Synchronous Programs with Refinement Types
von: Dane, Serra Z., et al.
Veröffentlicht: (2026)

Practical Formal Verification for MLIR Programs
von: Tucker, Emily, et al.
Veröffentlicht: (2026)

The Secrets Must Not Flow: Scaling Security Verification to Large Codebases (extended version)
von: Arquint, Linard, et al.
Veröffentlicht: (2025)

End-to-end Compositional Verification of Program Safety through Verified and Verifying Compilation
von: Wu, Jinhua, et al.
Veröffentlicht: (2025)

Resource Specifications for Resource-Manipulating Programs
von: Grannan, Zachary, et al.
Veröffentlicht: (2023)

Tunable Automation in Automated Program Verification
von: Bai, Alexander Y., et al.
Veröffentlicht: (2025)

Efficient Formal Verification of Quantum Error Correcting Programs
von: Huang, Qifan, et al.
Veröffentlicht: (2025)

Towards Formal Verification of LLM-Generated Code from Natural Language Prompts
von: Councilman, Aaron, et al.
Veröffentlicht: (2025)

Automated Formal Verification of a Software Fault Isolation System
von: Sotoudeh, Matthew, et al.
Veröffentlicht: (2025)

Forward Symbolic Execution for Trustworthy Automation of Binary Code Verification
von: Lindner, Andreas, et al.
Veröffentlicht: (2023)

From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs
von: Cao, Jialun, et al.
Veröffentlicht: (2025)

Toward Verified Library-Level Choreographic Programming with Algebraic Effects
von: Shen, Gan, et al.
Veröffentlicht: (2024)

Automated Verification of Tree-Manipulating Programs Using Constrained Horn Clauses
von: Faella, Marco, et al.
Veröffentlicht: (2024)

Program Skeletons for Automated Program Translation
von: Wang, Bo, et al.
Veröffentlicht: (2025)

Caesar: A Deductive Verifier for Probabilistic Programs
von: Schröer, Philipp, et al.
Veröffentlicht: (2026)

Pragmatics of Formally Verified Yet Efficient Static Analysis, in particular for Formally Verified Compilers
von: Monniaux, David
Veröffentlicht: (2024)

Towards Verified Compilation of Floating-point Optimization in Scientific Computing Programs
von: Tekriwal, Mohit, et al.
Veröffentlicht: (2025)

Formally Verified Linear-Time Invertible Lexing
von: Chassot, Samuel, et al.
Veröffentlicht: (2025)

Reasoning about Interior Mutability in Rust using Library-Defined Capabilities
von: Poli, Federico, et al.
Veröffentlicht: (2024)

SECOMP: Formally Secure Compilation of Compartmentalized C Programs
von: Thibault, Jérémy, et al.
Veröffentlicht: (2024)

Cobblestone: A Divide-and-Conquer Approach for Automating Formal Verification
von: Kasibatla, Saketh Ram, et al.
Veröffentlicht: (2024)

Reactive graphs in action (extended version)
von: Tinoco, David, et al.
Veröffentlicht: (2024)

VyZX: Formal Verification of a Graphical Quantum Language
von: Lehmann, Adrian, et al.
Veröffentlicht: (2023)

QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning
von: Sanchez-Stern, Alex, et al.
Veröffentlicht: (2024)

Dafny as Verification-Aware Intermediate Language for Code Generation
von: Li, Yue Chen, et al.
Veröffentlicht: (2025)

A Formal Framework for Naturally Specifying and Verifying Sequential Algorithms
von: Yang, Chengxi, et al.
Veröffentlicht: (2025)

Towards Repository-Level Program Verification with Large Language Models
von: Zhong, Si Cheng, et al.
Veröffentlicht: (2025)

KestRel: Relational Verification Using E-Graphs for Program Alignment
von: Dickerson, Robert, et al.
Veröffentlicht: (2024)

Advancing Automated In-Isolation Validation in Repository-Level Code Translation
von: Ke, Kaiyao, et al.
Veröffentlicht: (2025)

Relaxed exception semantics for Arm-A (extended version)
von: Simner, Ben, et al.
Veröffentlicht: (2024)

A Formalization of the Yul Language and Some Verified Yul Code Transformations
von: Coglio, Alessandro, et al.
Veröffentlicht: (2025)

Qafny: A Quantum-Program Verifier
von: Li, Liyi, et al.
Veröffentlicht: (2022)

Certified Program Synthesis with a Multi-Modal Verifier
von: Feng, Yueyang, et al.
Veröffentlicht: (2026)