Imagen de Portada

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

Fuente: arXiv

Guardado en:

Detalles Bibliográficos
Autores principales:	Parthasarathy, Gaurav, Dardinier, Thibault, Bonneau, Benjamin, Müller, Peter, Summers, Alexander J.
Formato:	Preprint
Publicado:	2024
Materias:	Programming Languages
Acceso en línea:	Acceder al recurso
Etiquetas:	Agregar Etiqueta Sin Etiquetas, Sea el primero en etiquetar este registro!

Ejemplares similares

Formal Foundations for Translational Separation Logic Verifiers (extended version)
por: Dardinier, Thibault, et al.
Publicado: (2024)

Hyper Separation Logic (extended version)
por: Gospodinov, Trayan, et al.
Publicado: (2026)

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

Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (extended version)
por: Dardinier, Thibault, et al.
Publicado: (2023)

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

Minuska: Towards a Formally Verified Programming Language Framework
por: Tušil, Jan, et al.
Publicado: (2024)

Towards Automated Verification of LLM-Synthesized C Programs
por: Mukherjee, Prasita, et al.
Publicado: (2024)

Towards Formal Verification of Hybrid Synchronous Programs with Refinement Types
por: Dane, Serra Z., et al.
Publicado: (2026)

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

The Secrets Must Not Flow: Scaling Security Verification to Large Codebases (extended version)
por: Arquint, Linard, et al.
Publicado: (2025)

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

Resource Specifications for Resource-Manipulating Programs
por: Grannan, Zachary, et al.
Publicado: (2023)

Tunable Automation in Automated Program Verification
por: Bai, Alexander Y., et al.
Publicado: (2025)

Efficient Formal Verification of Quantum Error Correcting Programs
por: Huang, Qifan, et al.
Publicado: (2025)

Towards Formal Verification of LLM-Generated Code from Natural Language Prompts
por: Councilman, Aaron, et al.
Publicado: (2025)

Automated Formal Verification of a Software Fault Isolation System
por: Sotoudeh, Matthew, et al.
Publicado: (2025)

Forward Symbolic Execution for Trustworthy Automation of Binary Code Verification
por: Lindner, Andreas, et al.
Publicado: (2023)

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

Toward Verified Library-Level Choreographic Programming with Algebraic Effects
por: Shen, Gan, et al.
Publicado: (2024)

Automated Verification of Tree-Manipulating Programs Using Constrained Horn Clauses
por: Faella, Marco, et al.
Publicado: (2024)

Program Skeletons for Automated Program Translation
por: Wang, Bo, et al.
Publicado: (2025)

Caesar: A Deductive Verifier for Probabilistic Programs
por: Schröer, Philipp, et al.
Publicado: (2026)

Pragmatics of Formally Verified Yet Efficient Static Analysis, in particular for Formally Verified Compilers
por: Monniaux, David
Publicado: (2024)

Towards Verified Compilation of Floating-point Optimization in Scientific Computing Programs
por: Tekriwal, Mohit, et al.
Publicado: (2025)

Formally Verified Linear-Time Invertible Lexing
por: Chassot, Samuel, et al.
Publicado: (2025)

Reasoning about Interior Mutability in Rust using Library-Defined Capabilities
por: Poli, Federico, et al.
Publicado: (2024)

SECOMP: Formally Secure Compilation of Compartmentalized C Programs
por: Thibault, Jérémy, et al.
Publicado: (2024)

Cobblestone: A Divide-and-Conquer Approach for Automating Formal Verification
por: Kasibatla, Saketh Ram, et al.
Publicado: (2024)

Reactive graphs in action (extended version)
por: Tinoco, David, et al.
Publicado: (2024)

VyZX: Formal Verification of a Graphical Quantum Language
por: Lehmann, Adrian, et al.
Publicado: (2023)

QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning
por: Sanchez-Stern, Alex, et al.
Publicado: (2024)

Dafny as Verification-Aware Intermediate Language for Code Generation
por: Li, Yue Chen, et al.
Publicado: (2025)

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

Towards Repository-Level Program Verification with Large Language Models
por: Zhong, Si Cheng, et al.
Publicado: (2025)

KestRel: Relational Verification Using E-Graphs for Program Alignment
por: Dickerson, Robert, et al.
Publicado: (2024)

Advancing Automated In-Isolation Validation in Repository-Level Code Translation
por: Ke, Kaiyao, et al.
Publicado: (2025)

Relaxed exception semantics for Arm-A (extended version)
por: Simner, Ben, et al.
Publicado: (2024)

A Formalization of the Yul Language and Some Verified Yul Code Transformations
por: Coglio, Alessandro, et al.
Publicado: (2025)

Qafny: A Quantum-Program Verifier
por: Li, Liyi, et al.
Publicado: (2022)

Certified Program Synthesis with a Multi-Modal Verifier
por: Feng, Yueyang, et al.
Publicado: (2026)