Verification by gambling on program slices

DOI10.1007/978-3-030-88885-5_18zbMATH Open1497.68282OpenAlexW3206433679MaRDI QIDQ2147204FDOQ2147204

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

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

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)

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: certifiably sound verification on relaxed slices
• Cut branches before looking for bugs: sound verification on relaxed slices
• Verification of programs that destructively manipulated data

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)