Program analysis is harder than verification: a computability perspective

DOI10.1007/978-3-319-96142-2_8MaRDI QIDQ6039396zbMATH OpenOpenAlexFDO

Authors Patrick Cousot, Roberto Giacobazzi, Francesco Ranzato

Publication date 5 May 2023

Published in Computer Aided Verification (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-319-96142-2_8

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 512849
• Program verification: state of the art, problems, and results. II
• Proof-Producing Program Analysis
• A vindication of program verification
• On the hardness of analyzing probabilistic programs
• A mechanical analysis of program verification strategies
• Program verification: state of the art, problems, and results. I
• Program verification. Fundamental issues in computer science
• Proofs verifying programs and programs producing proofs: a conceptual analysis

Cited in

(7)

• Intensional Kleene and Rice theorems for abstract program semantics
• Approximate bit dependency analysis to identify program synthesis problems as infeasible
• On the strength of “sometimes” and “always” in program verification
• Property-driven code obfuscations reinterpreting Jones-optimality in abstract interpretation
• Decoupling the ascending and descending phases in abstract interpretation
• A correctness and incorrectness program logic
• A Rice's theorem for abstract semantics

This page was built for publication: Program analysis is harder than verification: a computability perspective

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