Automatic program instrumentation for automatic verification

DOI10.1007/978-3-031-37709-9_14MaRDI QIDQ6535688zbMATH OpenFDO

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

Publication date 1 February 2024

Copyright license Creative Commons Attribution 4.0 International

Mathematics Subject Classification ID

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

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

Cites work

• scientific article; zbMATH DE number 5539366 (Why is no real title available?)
• scientific article; zbMATH DE number 1512563 (Why is no real title available?)
• Aligators for Arrays (Tool Paper)
• Array Folds Logic
• Automata and Logics for Words and Trees over an Infinite Alphabet
• Avoiding exponential explosion: generating compact verification conditions
• Cell morphing: from array programs to array-free Horn clauses
• Dafny: an automatic program verifier for functional correctness
• Finite state machines for strings over infinite alphabets
• Handbook of model checking
• Horn clause solvers for program verification
• Lazy abstraction with interpolants for arrays
• Quantified Heap Invariants for Object-Oriented Programs
• Quantified invariants via syntax-guided synthesis
• Quantifiers on demand
• RustHorn: CHC-based verification for Rust programs
• The spirit of ghost code
• 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)