AISE v2.0: Combining Loop Transformations - (Competition Contribution)

Abstract

Abstract is a C program verifier that synergizes symbolic execution and abstract interpretation. This year, v2.0 introduces a loop transformation scheme based on recurrence analysis to handle programs involving nonlinear arithmetic. By combining loop transformations, v2.0 achieved a score of 1031 and won first place in the ReachSafety-Loops category, demonstrating the effectiveness of the methods employed in v2.0.