Verification by gambling on program slices

DOI10.1007/978-3-030-88885-5_18zbMath1497.68282OpenAlexW3206433679MaRDI QIDQ2147204

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

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) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Uses Software

• SMTInterpol
• Ultimate Automizer
• CBMC
• SymDiff
• CIL

Cites Work

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

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