Equivalence Checking of Static Affine Programs Using Widening to Handle Recurrences

DOI10.1007/978-3-642-02658-4_44MaRDI QIDQ3636883zbMATH OpenOpenAlexFDO

Authors Sven Verdoolaege, Gerda Janssens, Maurice Bruynooghe

Publication date 30 June 2009

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

Full work available at URL https://lirias.kuleuven.be/handle/123456789/228370

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 2090598
• Polycheck: dynamic verification of iteration space transformations on affine programs
• Effective use of SMT solvers for program equivalence checking through invariant-sketching and query-decomposition
• Equivalence checking of Petri net models of programs using static and dynamic cut-points
• Program equivalence checking by two-tape automata

Cited in

(13)

• Predicate pairing for program verification
• Verifying procedural programs via constrained rewriting induction
• Automating regression verification of pointer programs by predicate abstraction
• Effective use of SMT solvers for program equivalence checking through invariant-sketching and query-decomposition
• Collective assertions
• Polycheck: dynamic verification of iteration space transformations on affine programs
• FEVS: a functional equivalence verification suite for high-performance scientific computing
• Loop invariant symbolic execution for parallel programs
• Relational program reasoning using compiler IR
• An Efficient Equivalence-checking Algorithm for a Model of Programs with Commutative and Absorptive Statements
• PEQtest: testing functional equivalence
• Lockstep composition for unbalanced loops
• scientific article; zbMATH DE number 5173454 (Why is no real title available?)

Describes a project that uses

Uses Software

• isl
• FADAlib
• cvc3

This page was built for publication: Equivalence Checking of Static Affine Programs Using Widening to Handle Recurrences

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