Backward symbolic execution with loop folding

DOI10.1007/978-3-030-88806-0_3zbMath1497.68109OpenAlexW3205083328MaRDI QIDQ2145317

Marek Chalupa, Jan Strejček

Publication date: 17 June 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-88806-0_3

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Uses Software

• Unnamed Item
• z3
• LLVM
• CPAchecker
• InvGen
• Snugglebug

Cites Work

• Unnamed Item
• Unnamed Item
• Automatic analysis of DMA races using model checking and \(k\)-induction
• Efficient weakest preconditions
• Property-directed incremental invariant generation
• Affine relationships among variables of a program
• Automatic generation of invariants and intermediate assertions
• Predicate Abstraction for Program Verification
• Guided Static Analysis
• Static Analysis in Disjunctive Numerical Domains
• Characterizations of Reducible Flow Graphs
• Symbolic execution and program testing
• Accelerating Interpolants
• Software Verification with PDR: An Implementation of the State of the Art
• A Calculus for Modular Loop Acceleration
• Compact Symbolic Execution
• Predicate abstraction for software verification
• Compositional may-must program analysis
• Program analysis via satisfiability modulo path programs
• Synthesis of Circular Compositional Program Proofs via Abduction
• Abstract acceleration of general linear loops
• Demand-Driven Compositional Symbolic Execution
• Computer Aided Verification
• Interpolating strong induction

This page was built for publication: Backward symbolic execution with loop folding