Modular verification of abstract software descriptions