Bei Softwareverifikation geht es darum, zu zeigen, dass ein Programm, auf eine bestimmte Eigenschaft bezogen, korrekt ist oder einen Fehler enthält. Für diese Verifikationsaufgaben gibt es unterschiedliche Verifikationstools, deren Leistung anhand von Benchmarks getestet wird.

ACSL, eine Spezifikationssprache, die vom Frama-C-Framework verwendet wird, fügt Annotationen (insbesondere „function contracts“) in C-Programme ein, um deren Verhalten formal zu spezifizieren und zusätzliche Programmeigenschaften, wie zum Beispiel Schleifeninvarianten, zu dokumentieren. Ziel der BA ist es, die in ACSL geschriebene Spezifikation der erwarteten Eigenschaft (und von der Verifikation zu prüfende Eigenschaft) so umzuschreiben, dass sie auch Verifizierungs-Tools, wie zum Beispiel der CPAchecker, verstehen, die Eigenschaftsspezifikationen in Form von Aufrufen (assumes und asserts) erwarten. Die beiden Hauptaufgaben sind die Definition der einzelnen Schritte, die zur Übersetzung notwendig sind und die anschließende Implementierung eines Übersetzers.