Buchumschlag

Automated Verification of Tree-Manipulating Programs Using Constrained Horn Clauses

Fuente: arXiv

Gespeichert in:

Bibliographische Detailangaben
Hauptverfasser:	Faella, Marco, Parlato, Gennaro
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

Verifying Tree-Manipulating Programs via CHCs
von: Faella, Marco, et al.
Veröffentlicht: (2025)

Catamorphic Abstractions for Constrained Horn Clause Satisfiability
von: De Angelis, Emanuele, et al.
Veröffentlicht: (2024)

A Unified Automata-Theoretic Approach to LTLf Modulo Theories (Extended Version)
von: Faella, Marco, et al.
Veröffentlicht: (2024)

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

CHCVerif: A Portfolio-Based Solver for Constrained Horn Clauses
von: Dobos-Kovács, Mihály, et al.
Veröffentlicht: (2025)

Multiple Query Satisfiability of Constrained Horn Clauses
von: De Angelis, Emanuele, et al.
Veröffentlicht: (2022)

Proceedings 18th International Workshop on Logical and Semantic Frameworks, with Applications and 10th Workshop on Horn Clauses for Verification and Synthesis
von: Kutsia, Temur, et al.
Veröffentlicht: (2024)

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

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

Through the Looking Glass, and what Horn Clause Programs Found There
von: Tarau, Paul
Veröffentlicht: (2024)

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

Iso-Recursive Multiparty Sessions and their Automated Verification -- Technical Report
von: Giunti, Marco, et al.
Veröffentlicht: (2025)

HornStr: Invariant Synthesis for Regular Model Checking as Constrained Horn Clauses(Technical Report)
von: Jiang, Hongjian, et al.
Veröffentlicht: (2025)

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

Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language (extended version)
von: Parthasarathy, Gaurav, et al.
Veröffentlicht: (2024)

Automated Verification of Soundness of DNN Certifiers
von: Singh, Avaljot, et al.
Veröffentlicht: (2025)

Hiord#: An Approach to the Specification and Verification of Higher-Order (C)LP Programs
von: Ciccalè, Marco, et al.
Veröffentlicht: (2025)

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

Solvable Tuple Patterns and Their Applications to Program Verification
von: Kobayashi, Naoki, et al.
Veröffentlicht: (2025)

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

Automated Software Verification of Hyperliveness
von: Beutner, Raven
Veröffentlicht: (2024)

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

C*: Unifying Programming and Verification in C
von: Cao, Yiyuan, et al.
Veröffentlicht: (2025)

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

What Challenges Do Developers Face When Using Verification-Aware Programming Languages?
von: Oliveira, Francisco, et al.
Veröffentlicht: (2025)

Automated Theorem Proving for Prolog Verification
von: Mesnard, Fred, et al.
Veröffentlicht: (2026)

Weighted NetKAT: A Programming Language For Quantitative Network Verification
von: Acevedo, Emmanuel Suárez, et al.
Veröffentlicht: (2026)

Automated Expected Cost Analysis for Quantum Programs
von: Moser, Georg, et al.
Veröffentlicht: (2026)

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

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

Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing (Extended Version)
von: Schröer, Philipp, et al.
Veröffentlicht: (2025)

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

Data-driven Verification of Procedural Programs with Integer Arrays
von: Bouajjani, Ahmed, et al.
Veröffentlicht: (2025)

Automated Verification of Monotonic Data Structure Traversals in C
von: Sotoudeh, Matthew
Veröffentlicht: (2025)

Structural Temporal Logic for Mechanized Program Verification
von: Ioannidis, Eleftherios, et al.
Veröffentlicht: (2024)

Ranking LLM-Generated Loop Invariants for Program Verification
von: Chakraborty, Saikat, et al.
Veröffentlicht: (2023)

FO-Complete Program Verification for Heap Logics
von: Murali, Adithya, et al.
Veröffentlicht: (2026)

Sheaf-Cohomological Program Analysis: Unifying Bug Finding, Equivalence, and Verification via Čech Cohomology
von: Young, Halley
Veröffentlicht: (2026)

Towards General Loop Invariant Generation: A Benchmark of Programs with Memory Manipulation
von: Liu, Chang, et al.
Veröffentlicht: (2023)

Quokka: Accelerating Program Verification with LLMs via Invariant Synthesis
von: Wei, Anjiang, et al.
Veröffentlicht: (2025)