Verifying numerical programs via iterative abstract testing

DOI10.1007/978-3-030-32304-2_13MaRDI QIDQ6536291zbMATH OpenFDO

Authors Banghu Yin, Liqian Chen, Jiangchao Liu, Ji Wang, Patrick Cousot

Publication date 19 April 2024

Full work available at URL https://doi.org/10.1007/978-3-030-32304-2_13

zbMATH Keywords

abstract interpretationabstract testinginput space partitioningprogram verification

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Automatic verification by abstract interpretation
• Formal Methods at the Crossroads. From Panacea to Foundational Support
• Verification by abstract interpretation
• Software model checking with abstraction refinement
• Formal verification for C program

Cites work

• Automatically Refining Abstract Interpretations
• CIL: Intermediate language and tools for analysis and transformation of C programs
• Counterexample-guided abstraction refinement for symbolic model checking
• Dynamic partitioning in linear relation analysis: application to the verification of reactive systems
• Model checking, testing and verification working together
• On abstraction in software verification
• Programming Languages and Systems
• Static analysis of arithmetical congruences
• The octagon abstract domain

Cited in

(1)

• Parallel program analysis via range splitting

This page was built for publication: Verifying numerical programs via iterative abstract testing

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