Copertina

Predictable Verification using Intrinsic Definitions

Fuente: arXiv

Salvato in:

Dettagli Bibliografici
Autori principali:	Murali, Adithya, Rivera, Cody, Madhusudan, P.
Natura:	Preprint
Pubblicazione:	2024
Soggetti:	Programming Languages Logic in Computer Science
Accesso online:	Acceder al recurso
Tags:	Aggiungi Tag Nessun Tag, puoi essere il primo ad aggiungerne!!

Documenti analoghi

FO-Complete Program Verification for Heap Logics
di: Murali, Adithya, et al.
Pubblicazione: (2026)

Complete first-order reasoning for functional programs
di: Murali, Adithya, et al.
Pubblicazione: (2026)

Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions
di: Elad, Neta, et al.
Pubblicazione: (2025)

Verification Modulo Tested Library Contracts
di: Uppar, Abhishek, et al.
Pubblicazione: (2026)

Intrinsically Correct Algorithms and Recursive Coalgebras
di: Alexandru, Cass, et al.
Pubblicazione: (2025)

Automated Software Verification of Hyperliveness
di: Beutner, Raven
Pubblicazione: (2024)

Automated Theorem Proving for Prolog Verification
di: Mesnard, Fred, et al.
Pubblicazione: (2026)

Structural Temporal Logic for Mechanized Program Verification
di: Ioannidis, Eleftherios, et al.
Pubblicazione: (2024)

Compositional Verification in Concurrent Separation Logic with Permissions Regions
di: Le, Quang Loc
Pubblicazione: (2025)

Products of Recursive Programs for Hypersafety Verification (Extended Version)
di: Cheng, Ruotong, et al.
Pubblicazione: (2025)

Automated Verification of Monotonic Data Structure Traversals in C
di: Sotoudeh, Matthew
Pubblicazione: (2025)

HaliVer: Deductive Verification and Scheduling Languages Join Forces
di: Haak, Lars B. van den, et al.
Pubblicazione: (2024)

Unfolding Iterators: Specification and Verification of Higher-Order Iterators, in OCaml
di: Chirica, Ion, et al.
Pubblicazione: (2025)

A Primal-Dual Perspective on Program Verification Algorithms (Extended Version)
di: Tsukada, Takeshi, et al.
Pubblicazione: (2025)

Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs
di: Chatterjee, Krishnendu, et al.
Pubblicazione: (2024)

Formal Verification of a Token Sale Launchpad: A Compositional Approach in Dafny
di: Ukhanov, Evgeny
Pubblicazione: (2025)

Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back
di: Batz, Kevin, et al.
Pubblicazione: (2025)

Combining Type Checking and Set Constraint Solving to Improve Automated Software Verification
di: Cristiá, Maximiliano, et al.
Pubblicazione: (2022)

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

An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification
di: Elad, Neta, et al.
Pubblicazione: (2023)

Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic (Extended Version)
di: Haselwarter, Philipp G., et al.
Pubblicazione: (2026)

Boosting Few-Pixel Robustness Verification via Covering Verification Designs
di: Shapira, Yuval, et al.
Pubblicazione: (2024)

VeriThoughts: Enabling Automated Verilog Code Generation using Reasoning and Formal Verification
di: Yubeaton, Patrick, et al.
Pubblicazione: (2025)

Gradual Verification for Smart Contracts
di: Sun, Haojia, et al.
Pubblicazione: (2023)

Verification of Recursively Defined Quantum Circuits
di: Ying, Mingsheng, et al.
Pubblicazione: (2024)

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

Mini-Batch Robustness Verification of Deep Neural Networks
di: Tzour-Shaday, Saar, et al.
Pubblicazione: (2025)

Neural Network Verification is a Programming Language Challenge
di: Cordeiro, Lucas C., et al.
Pubblicazione: (2025)

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

Proceedings of the 12th Workshop on Horn Clauses for Verification and Synthesis
di: De Angelis, Emanuele, et al.
Pubblicazione: (2025)

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

Compositional Program Verification with Polynomial Functors in Dependent Type Theory
di: Aberlé, C. B.
Pubblicazione: (2026)

A Certified Proof Checker for Deep Neural Network Verification in Imandra
di: Desmartin, Remi, et al.
Pubblicazione: (2024)

Relating Answer Set Programming and Many-sorted Logics for Formal Verification
di: Hansen, Zachary
Pubblicazione: (2025)

Towards a Certified Proof Checker for Deep Neural Network Verification
di: Desmartin, Remi, et al.
Pubblicazione: (2023)

Causal Past Logic for Runtime Verification of Distributed LLM Agent Workflows
di: Bollig, Benedikt
Pubblicazione: (2026)

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

Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions
di: Klinkenberg, Lutz, et al.
Pubblicazione: (2023)

Expressivity of AuDaLa: Turing Completeness and Possible Extensions
di: Franken, Tom T. P., et al.
Pubblicazione: (2024)

A Taxonomy of Hoare-Like Logics: Towards a Holistic View using Predicate Transformers and Kleene Algebras with Top and Tests
di: Verscht, Lena, et al.
Pubblicazione: (2024)