Because the reduction from IMP- to SAS+ would need something like bit blasting, we want to start by reducing a subset of IMP- called IMP-- to SAS+. While in IMP-, general additions and subtractions are included, IMP-- only has statements for incrementing or decrementing the value of variable by a constant. Hence, given a running time for an IMP-- program, we can derive polynomial bounds on how much the values of the registers can deviate during any point of the execution from the initial values of the registers.
maxhaslbeck
commented
3 years ago
Because the reduction from IMP- to SAS+ would need something like bit blasting, we want to start by reducing a subset of IMP- called IMP-- to SAS+. While in IMP-, general additions and subtractions are included, IMP-- only has statements for incrementing or decrementing the value of variable by a constant. Hence, given a running time for an IMP-- program, we can derive polynomial bounds on how much the values of the registers can deviate during any point of the execution from the initial values of the registers.