Copertina

AutoDeduct: A Tool for Automated Deductive Verification of C Code

Fuente: arXiv

Salvato in:

Dettagli Bibliografici
Autori principali:	Amilon, Jesper, Gurov, Dilian, Lidström, Christian, Nyberg, Mattias, Ung, Gustav, Wingbrant, Ola
Natura:	Preprint
Pubblicazione:	2025
Soggetti:	Logic in Computer Science Software Engineering
Accesso online:	Acceder al recurso
Tags:	Aggiungi Tag Nessun Tag, puoi essere il primo ad aggiungerne!!

Documenti analoghi

A Program Instrumentation Framework for Automatic Verification
di: Amilon, Jesper, et al.
Pubblicazione: (2024)

Contract Based Program Models for Software Model Checking
di: Amilon, Jesper, et al.
Pubblicazione: (2025)

Contract Based Verification of Non-functional Requirements for Embedded Automotive C Code
di: Amilon, Jesper, et al.
Pubblicazione: (2026)

Formalizing UML State Machines for Automated Verification -- A Survey
di: André, Étienne, et al.
Pubblicazione: (2024)

An Expressive Trace Logic for Recursive Programs
di: Gurov, Dilian, et al.
Pubblicazione: (2024)

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

Proceedings 14th International Conference on Automated Deduction in Geometry
di: Quaresma, Pedro, et al.
Pubblicazione: (2024)

Varanus: Runtime Verification for CSP
di: Luckcuck, Matt, et al.
Pubblicazione: (2025)

A Hoare Logic for Domain Specification (Full Version)
di: Kamburjan, Eduard, et al.
Pubblicazione: (2024)

Automated Verification of Silq Quantum Programs using SMT Solvers
di: Lewis, Marco, et al.
Pubblicazione: (2024)

StatWhy: Formal Verification Tool for Statistical Hypothesis Testing Programs
di: Kawamoto, Yusuke, et al.
Pubblicazione: (2024)

Vision: An Extensible Methodology for Formal Software Verification in Microservice Systems
di: Wojtak, Connor, et al.
Pubblicazione: (2025)

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

Bottoms Up for CHCs: Novel Transformation of Linear Constrained Horn Clauses to Software Verification
di: Somorjai, Márk, et al.
Pubblicazione: (2024)

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

Towards Specification-Driven LLM-Based Generation of Embedded Automotive Software
di: Patil, Minal Suresh, et al.
Pubblicazione: (2024)

Parameterized Dynamic Logic -- Towards A Cyclic Logical Framework for General Program Specification and Verification
di: Zhang, Yuanrui
Pubblicazione: (2024)

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

Applying Formal Methods Tools to an Electronic Warfare Codebase (Experience report)
di: Li, Letitia W., et al.
Pubblicazione: (2026)

PROMISE: Proof Automation as Structural Imitation of Human Reasoning
di: Ahn, Youngjoo, et al.
Pubblicazione: (2026)

Automating Semantic Analysis of System Assurance Cases using Goal-directed ASP
di: Murugesan, Anitha, et al.
Pubblicazione: (2024)

Correct-by-Construction G-Code Generation: A Neuro-Symbolic Approach via Separation Logic
di: Lee, Yeonseok
Pubblicazione: (2026)

A shallow dive into the depths of non-termination checking for C programs
di: Metta, Ravindra, et al.
Pubblicazione: (2024)

Practical Deductive Verification of OCaml Programs (Extended Version)
di: Pereira, Mário
Pubblicazione: (2024)

COTS: Connected OpenAPI Test Synthesis for RESTful Applications
di: Burlò, Christian Bartolo, et al.
Pubblicazione: (2024)

A Tale of 1001 LoC: Potential Runtime Error-Guided Specification Synthesis for Verifying Large-Scale Programs
di: Wang, Zhongyi, et al.
Pubblicazione: (2025)

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

Quantifying Software Correctness by Combining Architecture Modeling and Formal Program Analysis
di: Lanzinger, Florian, et al.
Pubblicazione: (2024)

Context, Judgement, Deduction
di: Coraglia, Greta, et al.
Pubblicazione: (2021)

From Proof to Program: Characterizing Tool-Induced Reasoning Hallucinations in Large Language Models
di: Bayat, Farima Fatahi, et al.
Pubblicazione: (2025)

Watchdogs and Oracles: Runtime Verification Meets Large Language Models for Autonomous Systems
di: Ferrando, Angelo
Pubblicazione: (2025)

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

Dafny as Verification-Aware Intermediate Language for Code Generation
di: Li, Yue Chen, et al.
Pubblicazione: (2025)

VeCoGen: Automating Generation of Formally Verified C Code with Large Language Models
di: Sevenhuijsen, Merlijn, et al.
Pubblicazione: (2024)

Optimal Circuit Synthesis of Linear Codes for Error Detection and Correction
di: Yang, Xi, et al.
Pubblicazione: (2026)

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

Cargo Sherlock: An SMT-Based Checker for Software Trust Costs
di: Hassnain, Muhammad, et al.
Pubblicazione: (2025)

Relevant HAL Interface Requirements for Embedded Systems
di: Bentele, Manuel, et al.
Pubblicazione: (2025)

A Decision Procedure for a Theory of Finite Sets with Finite Integer Intervals
di: Cristiá, Maximiliano, et al.
Pubblicazione: (2021)

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