Verification by gambling on program slices

DOI10.1007/978-3-030-88885-5_18MaRDI QIDQ2147204zbMATHOpenAlexFDO

Authors Murad Akhundov, Federico Mora, Nick Feng, Vincent Hui, Marsha Chechik

Publication date 22 June 2022

Full work available at URL https://doi.org/10.1007/978-3-030-88885-5_18

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Cryptography (94A60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Cut branches before looking for bugs: certifiably sound verification on relaxed slices
• Cut branches before looking for bugs: sound verification on relaxed slices
• Slicing software for model construction
• scientific article; zbMATH DE number 1982210
• Slicing Abstractions

Cites work

• scientific article; zbMATH DE number 2087570 (Why is no real title available?)
• Characterizations of Reducible Flow Graphs
• Combining model checking and data-flow analysis
• Depth-First Search and Linear Graph Algorithms
• Model Checking Recursive Programs with Exact Predicate Abstraction
• Predicate abstraction of ANSI-C programs using SAT
• Scaling bounded model checking by transforming programs with arrays
• Semantics-preserving procedure extraction
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(3)

• Cut branches before looking for bugs: sound verification on relaxed slices
• Cut branches before looking for bugs: certifiably sound verification on relaxed slices
• Verification of programs that destructively manipulated data

Describes a project that uses

Uses Software

• SMTInterpol
• Ultimate Automizer
• CBMC
• SymDiff
• CIL

This page was built for publication: Verification by gambling on program slices

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