Imagen de Portada

Gradual C0: Symbolic Execution for Gradual Verification

Fuente: arXiv

Guardado en:

Detalles Bibliográficos
Autores principales:	DiVincenzo, Jenna, McCormack, Ian, Gouni, Hemant, Gorenburg, Jacob, Ramos-Dávila, Jan-Paul, Zhang, Mona, Zimmerman, Conrad, Sunshine, Joshua, Tanter, Éric, Aldrich, Jonathan
Formato:	Preprint
Publicado:	2022
Materias:	Logic in Computer Science F.3.1
Acceso en línea:	Acceder al recurso
Etiquetas:	Agregar Etiqueta Sin Etiquetas, Sea el primero en etiquetar este registro!

Ejemplares similares

Gradual Exact Logic: Unifying Hoare Logic and Incorrectness Logic via Gradual Verification
por: Zimmerman, Conrad, et al.
Publicado: (2024)

Gradual Verification for Smart Contracts
por: Sun, Haojia, et al.
Publicado: (2023)

A Study of Undefined Behavior Across Foreign Function Boundaries in Rust Libraries
por: McCormack, Ian, et al.
Publicado: (2024)

Gradual Sensitivity Typing
por: Arquez, Damian, et al.
Publicado: (2023)

A Mixed-Methods Study on the Implications of Unsafe Rust for Interoperation, Encapsulation, and Tooling
por: McCormack, Ian, et al.
Publicado: (2024)

Guard Analysis and Safe Erasure Gradual Typing: a Type System for Elixir
por: Castagna, Giuseppe, et al.
Publicado: (2024)

Compiling Gradual Types with Evidence
por: Romero, José Luis, et al.
Publicado: (2025)

Trustworthy Verification of RISC-V Binaries Using Symbolic Execution in HolBA
por: Palmskog, Karl, et al.
Publicado: (2025)

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

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

Unifying Model Execution and Deductive Verification with Interaction Trees in Isabelle/HOL
por: Foster, Simon, et al.
Publicado: (2024)

Quantitative Linear Logic for Neuro-Symbolic Learning and Verification
por: Flinkow, Thomas, et al.
Publicado: (2026)

Compositional Symbolic Execution for Correctness and Incorrectness Reasoning (Extended Version)
por: Lööw, Andreas, et al.
Publicado: (2024)

Smart Contracts Formal Verification: A Systematic Literature Review
por: Davila, Rene, et al.
Publicado: (2025)

Eidoku: A Neuro-Symbolic Verification Gate for LLM Reasoning via Structural Constraint Satisfaction
por: Miya, Shinobu
Publicado: (2025)

COBALT-TLA: A Neuro-Symbolic Verification Loop for Cross-Chain Bridge Vulnerability Discovery
por: Blain, Dominik
Publicado: (2026)

Formal Verification of the Sumcheck Protocol
por: Bosshard, Azucena Garvía, et al.
Publicado: (2024)

On Improving Deep Active Learning with Formal Verification
por: Spiegelman, Jonathan, et al.
Publicado: (2025)

Neuro-Symbolic Verification of LLM Outputs for Data-Sensitive Domains (extended preprint)
por: Sigloch, Paul, et al.
Publicado: (2026)

Tools at the Frontiers of Quantitative Verification
por: Andriushchenko, Roman, et al.
Publicado: (2024)

Pitts and Intuitionistic Multi-Succedent: Uniform Interpolation for KM
por: Férée, Hugo, et al.
Publicado: (2026)

Monotonicity and a Taylor approximation theorem for transseries
por: Mantova, Vincenzo
Publicado: (2026)

Practical Rely/Guarantee Verification of an Efficient Lock for seL4 on Multicore Architectures
por: Colvin, Robert J., et al.
Publicado: (2024)

Periods in Families and Derivatives of Period Maps
por: Bakker, Ben, et al.
Publicado: (2024)

The $λ$-PSP at $λ$-coanalytic sets
por: Barrera, Fernando, et al.
Publicado: (2025)

The Baire and perfect set properties at singulars cardinals
por: Dimonte, Vincenzo, et al.
Publicado: (2024)

Uniform interpolation with constructive diamond
por: van der Giessen, Iris, et al.
Publicado: (2026)

Taking Bi-Intuitionistic Logic First-Order: A Proof-Theoretic Investigation via Polytree Sequents
por: Lyon, Tim S., et al.
Publicado: (2024)

Cardinalities of Ultraproducts of Finite Sets in ZF + DC
por: Kowalczyk, Jacob
Publicado: (2025)

Recomposition: A New Technique for Efficient Compositional Verification
por: Dardik, Ian, et al.
Publicado: (2024)

Symbolic Computation for All the Fun
por: Brown, Chad E., et al.
Publicado: (2024)

Duality for Constructive Modal Logics: from Sahqlvist to Goldblatt-Thomason
por: de Groot, Jim, et al.
Publicado: (2026)

Semantical Analysis of Intuitionistic Modal Logics between CK and IK
por: de Groot, Jim, et al.
Publicado: (2024)

Proofs as Execution Trees for the π-Calculus
por: Acclavio, Matteo, et al.
Publicado: (2024)

Tarski's least fixed point theorem: A predicative type theoretic formulation
por: Ray, Ian
Publicado: (2024)

An Optimal 14-Symbol Hybrid Basis for BCH-Algebras
por: Ramani, Mahesh, et al.
Publicado: (2026)

Hyperproperty Verification as CHC Satisfiability
por: Itzhaky, Shachar, et al.
Publicado: (2023)

Craig Interpolation in Program Verification
por: Rümmer, Philipp
Publicado: (2026)

Verification of Configurable SRA Systems
por: Cimatti, Alessandro, et al.
Publicado: (2026)

Reflexive graph lenses in univalent foundations
por: Sterling, Jonathan
Publicado: (2024)