Automatic program instrumentation for automatic verification

DOI10.1007/978-3-031-37709-9_14zbMATH Open1547.68109MaRDI QIDQ6535688FDOQ6535688

Authors: Jesper Amilon, Zafer Esen, Dilian Gurov, Christian Lidström, Philipp Rümmer 

Publication date: 1 February 2024

Recommendations

• Simplifying the Verification of Quantified Array Assertions via Code Transformation
• Quantifiers on demand
• Automatic Verification of Integer Array Programs
• scientific article; zbMATH DE number 1953018
• Automated program verification

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Cites Work

• Dafny: an automatic program verifier for functional correctness
• Automata and Logics for Words and Trees over an Infinite Alphabet
• Title not available (Why is that?)
• Quantified Heap Invariants for Object-Oriented Programs
• Lazy abstraction with interpolants for arrays
• Avoiding exponential explosion: generating compact verification conditions
• Finite state machines for strings over infinite alphabets
• The spirit of ghost code
• Handbook of model checking
• Cell morphing: from array programs to array-free Horn clauses
• Horn clause solvers for program verification
• Quantifiers on demand
• Quantified invariants via syntax-guided synthesis
• RustHorn: CHC-based verification for Rust programs
• Array Folds Logic
• Title not available (Why is that?)
• Aligators for Arrays (Tool Paper)
• Verifying Catamorphism-Based Contracts using Constrained Horn Clauses

This page was built for publication: Automatic program instrumentation for automatic verification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6535688)