Dartagnan ist ein Bounded Model Checker, der für ein gegebenes nebenläufiges (C-)Programm und ein Speichermodell (X86, AARCH64 v8-A, POWER, C11, etc.) prüft, ob es darin innerhalb einer beschränkten Zahl von Ausführungsschritten zu einem Fehler kommen kann.
Github: hernanponcedeleon/Dat3M