Equivalence Checking of Static Affine Programs Using Widening to Handle Recurrences

DOI10.1007/978-3-642-02658-4_44zbMath1242.68076OpenAlexW2151828216MaRDI QIDQ3636883

Maurice Bruynooghe, Sven Verdoolaege, Gerda Janssens

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

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

Related Items (7)

Verifying Procedural Programs via Constrained Rewriting Induction ⋮ Loop Invariant Symbolic Execution for Parallel Programs ⋮ Automating regression verification of pointer programs by predicate abstraction ⋮ Relational program reasoning using compiler IR ⋮ FEVS: a functional equivalence verification suite for high-performance scientific computing ⋮ Predicate Pairing for program verification ⋮ Collective Assertions

Uses Software

• cvc3
• FADAlib
• isl

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