Raster drawing algorithms are algorithms that render continuous geometric shapes (lines, circles, curves) in a discrete 2D pixel space. Examples include Bresenham’s line drawing and circle drawing algorithms. These algorithms are intricate, and have non-trivial termination arguments that makes them a nice challenge for formalisation and verification.
Correctness conditions to be verified could include proving that the raster drawing is a sound approximation of the continuous geometric shape, and proving that the raster drawing produced is a contiguous drawing that does not have more points than necessary or holes.
Required skills: proof assistants (e.g. Isabelle/HOL), discrete mathematics.