Integrating Bounded Model Checking with KeY

Typ: MA
Datum: 2017-07-14
Betreuer: Mattias Ulbrich
Michael Kirsten
Bearbeiter:
Aushang:

Ziel

Explore and implement a concept to extract bit-vector proof obligations from KeY to bounded model checkers (such as Java Pathfinder or CBMC) that can deal well with them.

Kontakt: