Buchumschlag

Bottoms Up for CHCs: Novel Transformation of Linear Constrained Horn Clauses to Software Verification

Fuente: arXiv

Gespeichert in:

Bibliographische Detailangaben
Hauptverfasser:	Somorjai, Márk, Dobos-Kovács, Mihály, Ádám, Zsófia, Bajczi, Levente, Vörös, András
Format:	Preprint
Veröffentlicht:	2024
Schlagworte:	Logic in Computer Science Software Engineering
Online-Zugang:	Acceder al recurso
Tags:	Tag hinzufügen Keine Tags, Fügen Sie den ersten Tag hinzu!

Ähnliche Einträge

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

Theta as a Horn Solver
von: Bajczi, Levente, et al.
Veröffentlicht: (2025)

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

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)

Vision: An Extensible Methodology for Formal Software Verification in Microservice Systems
von: Wojtak, Connor, et al.
Veröffentlicht: (2025)

ESBMC: A Survey of Its Evolution, Integration, and Future Directions in Formal Software Verification
von: Dantas, Pierre, et al.
Veröffentlicht: (2026)

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

Varanus: Runtime Verification for CSP
von: Luckcuck, Matt, et al.
Veröffentlicht: (2025)

Formalizing UML State Machines for Automated Verification -- A Survey
von: André, Étienne, et al.
Veröffentlicht: (2024)

Smart Contracts Formal Verification: A Systematic Literature Review
von: Davila, Rene, et al.
Veröffentlicht: (2025)

AutoDeduct: A Tool for Automated Deductive Verification of C Code
von: Amilon, Jesper, et al.
Veröffentlicht: (2025)

Parameterized Dynamic Logic -- Towards A Cyclic Logical Framework for General Program Specification and Verification
von: Zhang, Yuanrui
Veröffentlicht: (2024)

Cargo Sherlock: An SMT-Based Checker for Software Trust Costs
von: Hassnain, Muhammad, et al.
Veröffentlicht: (2025)

Quantifying Software Correctness by Combining Architecture Modeling and Formal Program Analysis
von: Lanzinger, Florian, et al.
Veröffentlicht: (2024)

Formal Verification of PLCs as a Service: A CERN-GSI Safety-Critical Case Study (extended version)
von: Lopez-Miguel, Ignacio D., et al.
Veröffentlicht: (2025)

LLMs and Fuzzing in Tandem: A New Approach to Automatically Generating Weakest Preconditions
von: King, Daragh, et al.
Veröffentlicht: (2025)

GNU Aris: a web application for students
von: Attri, Saksham, et al.
Veröffentlicht: (2025)

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

A SCADE Model Verification Method Based on B-Model Transformation
von: Hou, Xili, et al.
Veröffentlicht: (2025)

Automated Verification of Silq Quantum Programs using SMT Solvers
von: Lewis, Marco, et al.
Veröffentlicht: (2024)

StatWhy: Formal Verification Tool for Statistical Hypothesis Testing Programs
von: Kawamoto, Yusuke, et al.
Veröffentlicht: (2024)

Watchdogs and Oracles: Runtime Verification Meets Large Language Models for Autonomous Systems
von: Ferrando, Angelo
Veröffentlicht: (2025)

Neuro-Symbolic Verification of LLM Outputs for Data-Sensitive Domains (extended preprint)
von: Sigloch, Paul, et al.
Veröffentlicht: (2026)

Applying Formal Methods Tools to an Electronic Warfare Codebase (Experience report)
von: Li, Letitia W., et al.
Veröffentlicht: (2026)

FlexFringe: Modeling Software Behavior by Learning Probabilistic Automata
von: Verwer, Sicco, et al.
Veröffentlicht: (2022)

Multi-Threaded Software Model Checking via Parallel Trace Abstraction Refinement
von: Barth, Max, et al.
Veröffentlicht: (2025)

Optimal Circuit Synthesis of Linear Codes for Error Detection and Correction
von: Yang, Xi, et al.
Veröffentlicht: (2026)

Agentic Proving for Program Verification
von: Sosso, Alessandro, et al.
Veröffentlicht: (2026)

Automatic Bottom-Up Taxonomy Construction: A Software Application Domain Study
von: Sas, Cezar, et al.
Veröffentlicht: (2024)

CTL* Verification and Synthesis using Existential Horn Clauses
von: Carelli, Mishel, et al.
Veröffentlicht: (2024)

Verification Modulo Tested Library Contracts
von: Uppar, Abhishek, et al.
Veröffentlicht: (2026)

Towards Automatic Transformations of Coq Proof Scripts
von: Magaud, Nicolas
Veröffentlicht: (2024)

Next Steps in LLM-Supported Java Verification
von: Teuber, Samuel, et al.
Veröffentlicht: (2025)

A Note on Runtime Verification of Concurrent Systems
von: Leucker, Martin
Veröffentlicht: (2025)

Reusable Formal Verification of DAG-based Consensus Protocols
von: Bertrand, Nathalie, et al.
Veröffentlicht: (2024)

Runtime Verification via Rational Monitor with Imperfect Information
von: Ferrando, Angelo, et al.
Veröffentlicht: (2024)

Relevant HAL Interface Requirements for Embedded Systems
von: Bentele, Manuel, et al.
Veröffentlicht: (2025)

A Decision Procedure for a Theory of Finite Sets with Finite Integer Intervals
von: Cristiá, Maximiliano, et al.
Veröffentlicht: (2021)

Combining Logic with Large Language Models for Automatic Debugging and Repair of ASP Programs
von: Brancas, Ricardo, et al.
Veröffentlicht: (2024)

Formal Analysis of the Sigmoid Function and Formal Proof of the Universal Approximation Theorem
von: Bryant, Dustin, et al.
Veröffentlicht: (2025)