Im Rahmen der deduktiven Programmverifikation ist Ghostcode ein Teil des Programms, der zum Zwecke der Spezifikation hinzugefügt wird. Geistercode darf regulären Code nicht stören, in dem Sinne, dass er ohne erkennbaren Unterschied im Programmergebnis gelöscht werden kann.
