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

• Depth-First Search and Linear Graph Algorithms
• Characterizations of Reducible Flow Graphs
• Tools and Algorithms for the Construction and Analysis of Systems
• Title not available (Why is that?)
• Model Checking Recursive Programs with Exact Predicate Abstraction
• Scaling bounded model checking by transforming programs with arrays
• Predicate abstraction of ANSI-C programs using SAT
• Semantics-preserving procedure extraction
• Combining Model Checking and Data-Flow Analysis

Cited In (1)

• 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)