Image de couverture de livre

Automated Verification of Tree-Manipulating Programs Using Constrained Horn Clauses

Fuente: arXiv

Enregistré dans:

Détails bibliographiques
Auteurs principaux:	Faella, Marco, Parlato, Gennaro
Format:	Preprint
Publié:	2024
Sujets:	Programming Languages
Accès en ligne:	Acceder al recurso
Tags:	Ajouter un tag Pas de tags, Soyez le premier à ajouter un tag!

Documents similaires

Verifying Tree-Manipulating Programs via CHCs
par: Faella, Marco, et autres
Publié: (2025)

Catamorphic Abstractions for Constrained Horn Clause Satisfiability
par: De Angelis, Emanuele, et autres
Publié: (2024)

A Unified Automata-Theoretic Approach to LTLf Modulo Theories (Extended Version)
par: Faella, Marco, et autres
Publié: (2024)

Proceedings of the 12th Workshop on Horn Clauses for Verification and Synthesis
par: De Angelis, Emanuele, et autres
Publié: (2025)

CHCVerif: A Portfolio-Based Solver for Constrained Horn Clauses
par: Dobos-Kovács, Mihály, et autres
Publié: (2025)

Multiple Query Satisfiability of Constrained Horn Clauses
par: De Angelis, Emanuele, et autres
Publié: (2022)

Proceedings 18th International Workshop on Logical and Semantic Frameworks, with Applications and 10th Workshop on Horn Clauses for Verification and Synthesis
par: Kutsia, Temur, et autres
Publié: (2024)

Towards Automated Verification of LLM-Synthesized C Programs
par: Mukherjee, Prasita, et autres
Publié: (2024)

Verification Algorithms for Automated Separation Logic Verifiers
par: Eilers, Marco, et autres
Publié: (2024)

Through the Looking Glass, and what Horn Clause Programs Found There
par: Tarau, Paul
Publié: (2024)

Tunable Automation in Automated Program Verification
par: Bai, Alexander Y., et autres
Publié: (2025)

Iso-Recursive Multiparty Sessions and their Automated Verification -- Technical Report
par: Giunti, Marco, et autres
Publié: (2025)

HornStr: Invariant Synthesis for Regular Model Checking as Constrained Horn Clauses(Technical Report)
par: Jiang, Hongjian, et autres
Publié: (2025)

KestRel: Relational Verification Using E-Graphs for Program Alignment
par: Dickerson, Robert, et autres
Publié: (2024)

Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language (extended version)
par: Parthasarathy, Gaurav, et autres
Publié: (2024)

Automated Verification of Soundness of DNN Certifiers
par: Singh, Avaljot, et autres
Publié: (2025)

Hiord#: An Approach to the Specification and Verification of Higher-Order (C)LP Programs
par: Ciccalè, Marco, et autres
Publié: (2025)

Practical Formal Verification for MLIR Programs
par: Tucker, Emily, et autres
Publié: (2026)

Solvable Tuple Patterns and Their Applications to Program Verification
par: Kobayashi, Naoki, et autres
Publié: (2025)

Resource Specifications for Resource-Manipulating Programs
par: Grannan, Zachary, et autres
Publié: (2023)

Automated Software Verification of Hyperliveness
par: Beutner, Raven
Publié: (2024)

Towards Formal Verification of Hybrid Synchronous Programs with Refinement Types
par: Dane, Serra Z., et autres
Publié: (2026)

C*: Unifying Programming and Verification in C
par: Cao, Yiyuan, et autres
Publié: (2025)

QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning
par: Sanchez-Stern, Alex, et autres
Publié: (2024)

What Challenges Do Developers Face When Using Verification-Aware Programming Languages?
par: Oliveira, Francisco, et autres
Publié: (2025)

Automated Theorem Proving for Prolog Verification
par: Mesnard, Fred, et autres
Publié: (2026)

Weighted NetKAT: A Programming Language For Quantitative Network Verification
par: Acevedo, Emmanuel Suárez, et autres
Publié: (2026)

Automated Expected Cost Analysis for Quantum Programs
par: Moser, Georg, et autres
Publié: (2026)

End-to-end Compositional Verification of Program Safety through Verified and Verifying Compilation
par: Wu, Jinhua, et autres
Publié: (2025)

Automated Formal Verification of a Software Fault Isolation System
par: Sotoudeh, Matthew, et autres
Publié: (2025)

Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing (Extended Version)
par: Schröer, Philipp, et autres
Publié: (2025)

Efficient Formal Verification of Quantum Error Correcting Programs
par: Huang, Qifan, et autres
Publié: (2025)

Data-driven Verification of Procedural Programs with Integer Arrays
par: Bouajjani, Ahmed, et autres
Publié: (2025)

Automated Verification of Monotonic Data Structure Traversals in C
par: Sotoudeh, Matthew
Publié: (2025)

Structural Temporal Logic for Mechanized Program Verification
par: Ioannidis, Eleftherios, et autres
Publié: (2024)

FO-Complete Program Verification for Heap Logics
par: Murali, Adithya, et autres
Publié: (2026)

Ranking LLM-Generated Loop Invariants for Program Verification
par: Chakraborty, Saikat, et autres
Publié: (2023)

Sheaf-Cohomological Program Analysis: Unifying Bug Finding, Equivalence, and Verification via Čech Cohomology
par: Young, Halley
Publié: (2026)

Towards General Loop Invariant Generation: A Benchmark of Programs with Memory Manipulation
par: Liu, Chang, et autres
Publié: (2023)

Quokka: Accelerating Program Verification with LLMs via Invariant Synthesis
par: Wei, Anjiang, et autres
Publié: (2025)