Cilj ovog projektnog zadataka je izrada model checkera za verifikaciju regularnih safety svojstava booleovskih programa po uzoru na bebop (simbolički model checker za booleovske programe koji je integralni dio SLAM-a). Dizajn i osnovni aspekti implementacije bebop-a opisani su u:
U prvoj fazi projekta potrebno je izraditi parser za booleovske programe prema gramatici koja je opisana u članku o bebop-u (preporučuje se upotreba ANTLR parser generatora), te .NET wrappera (napisanog u C# ili C++ CLI) za neku od glavnih biblioteka za rad s binarnim dijagramima odlučivanja (CUDD, BDD Library (CMU), BuDDy).
Naredna faza sastoji se od implementacije adaptirane verzije Sagiv-Reps-Horwitz-ovog algoritma za interproceduralnu analizu toka podataka. Osnovni algoritam je detaljno opisan u:
Opcionalni prijedlog (za kasnije):
Projektni zadatak sastavio: Matko Botinčan.