Cover Image

A Program Instrumentation Framework for Automatic Verification

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Amilon, Jesper, Esen, Zafer, Gurov, Dilian, Lidström, Christian, Rümmer, Philipp, Voorberg, Marten
Format:	Preprint
Published:	2024
Subjects:	Logic in Computer Science
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

AutoDeduct: A Tool for Automated Deductive Verification of C Code
by: Amilon, Jesper, et al.
Published: (2025)

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

Craig Interpolation in Program Verification
by: Rümmer, Philipp
Published: (2026)

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

Sound and Complete Invariant-Based Heap Encodings (Technical Report)
by: Esen, Zafer, et al.
Published: (2025)

Verification of Configurable SRA Systems
by: Cimatti, Alessandro, et al.
Published: (2026)

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

Synthesis and Verification of Transformer Programs (Technical Report)
by: Jiang, Hongjian, et al.
Published: (2026)

Asynchronous Agents with Perfect Recall: Model Reductions, Knowledge-Based Construction, and Model Checking for Coalitional Strategies
by: Gurov, Dilian, et al.
Published: (2024)

Unattainability of Common Knowledge in Asymmetric Games with Imperfect Information
by: Farestam, Fabian, et al.
Published: (2025)

An Encoding for CLP Problems in SMT-LIB
by: Amrollahi, Daneshvar, et al.
Published: (2024)

A Framework for Modelling, Verification and Transformation of Concurrent Imperative Programs
by: Bortin, Maksym
Published: (2020)

The Power of Regular Constraint Propagation (Technical Report)
by: Hague, Matthew, et al.
Published: (2025)

Specification and Automatic Verification of Computational Reductions
by: Grange, Julien, et al.
Published: (2024)

VerifyThis 2019: A Program Verification Competition (Extended Report)
by: Dross, Claire, et al.
Published: (2020)

OSTRICH2: Solver for Complex String Constraints
by: Hague, Matthew, et al.
Published: (2025)

Pseudo-Formalization for Automatic Proof Verification
by: Barkallah, Slim, et al.
Published: (2026)

A Practical Specification Language for Automatic Quantum Program Verification (Technical Report)
by: Tsai, Wei-Lun, et al.
Published: (2026)

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

Automatic Verification of Floating-Point Accumulation Networks
by: Zhang, David K., et al.
Published: (2025)

Model Checking as Program Verification by Abstract Interpretation (Extended Version)
by: Baldan, Paolo, et al.
Published: (2025)

A Denotational Product Construction for Temporal Verification of Effectful Higher-Order Programs
by: Watanabe, Kazuki, et al.
Published: (2025)

Modular Automatic Complexity Analysis of Recursive Integer Programs
by: Lommen, Nils, et al.
Published: (2025)

Simple Classes of Automatic Structures
by: Blumensath, Achim
Published: (2025)

Static and Dynamic Verification of OCaml Programs: The Gospel Ecosystem (Extended Version)
by: Soares, Tiago Lopes, et al.
Published: (2024)

Revisiting Differential Verification: Equivalence Verification with Confidence
by: Teuber, Samuel, et al.
Published: (2024)

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

Deductive Verification of Weak Memory Programs with View-based Protocols (extended version)
by: Şakar, Ömer, et al.
Published: (2026)

Verification of E-Voting Algorithms in Dafny
by: Büttner, Robert, et al.
Published: (2025)

{log}: From a Constraint Logic Programming Language to a Formal Verification Tool
by: Cristiá, Maximiliano, et al.
Published: (2025)

Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type System
by: Kura, Satoshi, et al.
Published: (2024)

Automatic Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops
by: Lommen, Nils, et al.
Published: (2022)

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

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

HornStr: Invariant Synthesis for Regular Model Checking as Constrained Horn Clauses(Technical Report)
by: Jiang, Hongjian, et al.
Published: (2025)

Formal Verification of Quantum Programs: Theory, Tools and Challenges
by: Lewis, Marco, et al.
Published: (2021)

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

A Cobham theorem for scalar multiplication
by: Hieronymi, Philipp, et al.
Published: (2024)

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

A Hierarchy of Supermartingales for $ω$-Regular Verification
by: Kura, Satoshi, et al.
Published: (2025)