Some embodiments of the present invention provide techniques and systems for optimizing bounds-checking During operation, the system can receive one or more instructions which when executed evaluate a first expression whose value is required to be between a lower bound expression's value and an upper bound expression's value, such that at least one of the following three values is not determinable before execution: the first expression's value, the lower bound expression's value, and the upper bound expression's value. Next, the system can use computer algebra to determine whether the first expression's value is guaranteed to be between the lower bound expression's value and the upper bound expression's value. If the system determines that the first expression's value is not guaranteed to be between the lower bound expression's value and the upper bound expression's value, the system can add bounds-checking instructions to the one or more instructions.