High-level abstractions for optimal checkpointing in inversion problems