Polycheck: dynamic verification of iteration space transformations on affine programs

DOI10.1145/2837614.2837656zbMATH Open1347.68068MaRDI QIDQ2828296FDOQ2828296

Authors: Wenlei Bao, Sriram Krishnamoorthy, Louis-Noël Pouchet, Fabrice Rastello, P. Sadayappan 

Publication date: 24 October 2016

Published in: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)

Recommendations

• Equivalence Checking of Static Affine Programs Using Widening to Handle Recurrences
• Verifying Array Programs by Transforming Verification Conditions
• scientific article; zbMATH DE number 7364137
• Verification of mutable linear data structures and iterator-based algorithms in Dafny
• scientific article; zbMATH DE number 868107
• Controlling polyvariance for specialization-based verification
• Verifying properties of differentiable programs

zbMATH Keywords

static analysisdynamic verificationiteration space transformation

Mathematics Subject Classification ID

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

Cited In (3)

• Automatic validation of code-improving transformations on low-level program representations
• Equivalence Checking of Static Affine Programs Using Widening to Handle Recurrences
• Translation and run-time validation of loop transformations

This page was built for publication: Polycheck: dynamic verification of iteration space transformations on affine programs

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