Reusing predicate precision in value analysis

DOI10.1007/978-3-031-07727-2_5MaRDI QIDQ2165503zbMATH OpenOpenAlexFDO

Authors Marie-Christine Jakobs

Publication date 19 August 2022

Full work available at URL https://doi.org/10.1007/978-3-031-07727-2_5

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

• scientific article; zbMATH DE number 1903343
• Reuse of proofs in software verification
• Reuse in Software Verification by Abstract Method Calls
• A framework for combining analysis and verification
• Tools and Algorithms for the Construction and Analysis of Systems

Cites work

• Abstraction-driven concolic testing
• Automatic construction of Hoare proofs from abstract interpretation results.
• Collaborative verification and testing with explicit assumptions
• Compositional may-must program analysis: unleashing the power of alternation
• Counterexample-guided abstraction refinement for symbolic model checking
• Empirical software metrics for benchmarking of verification tools
• From under-approximations to over-approximations and back
• scientific article; zbMATH DE number 1903378 (Why is no real title available?)
• Incremental Abstract Interpretation
• Incremental verification using trace abstraction
• Information reuse for multi-goal reachability analyses
• Lazy abstraction
• Lightweight bytecode verification
• Logic for Programming, Artificial Intelligence, and Reasoning
• MetaVal: witness validation via verification
• Modular demand-driven analysis of semantic difference for program versions
• Orion: High-Precision Methods for Static Error Analysis of C and C++ Programs
• Proof-carrying code from certified abstract interpretation and fixpoint compression
• Proof-Producing Program Analysis
• Structurally defined conditional data-flow static analysis
• Verification: Theory and Practice

Cited in

(1)

• Bias-variance tradeoffs in program analysis

This page was built for publication: Reusing predicate precision in value analysis

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