ARDiff: scaling program equivalence checking via iterative abstraction and refinement of common code
Sahar Badihi, Faridah Akinotcho, Yi Li, Julia Rubin
Abstract
Equivalence checking techniques help establish whether two versions of a program exhibit the same behavior. The majority of popular techniques for formally proving/refuting equivalence relies on symbolic execution – a static analysis approach that reasons about program behaviors in terms of symbolic input variables. Yet, symbolic execution is difficult to scale in practice due to complex programming constructs, such as loops and non-linear arithmetic.
Topics & Concepts
Equivalence (formal languages)Symbolic executionComputer scienceSymbolic trajectory evaluationAbstractionProgramming languageProgram analysisFormal equivalence checkingAbstraction model checkingModel checkingTheoretical computer scienceSymbolic data analysisStatic analysisAlgorithmMathematicsDiscrete mathematicsSoftwareEpistemologyPhilosophySoftware Testing and Debugging TechniquesSoftware Engineering ResearchFormal Methods in Verification