CSharp Verification via DIVINE

Master thesis, offered

University: MU, Faculty: FI, Topic: Distributed Systems

DIVINE supports verification of LLVM bitcode, but the C# compilation to LLVM is still a work in progress. The student will extend the C# to LLVM compilation with basic support for garbage collection and exception handling such that a considerable subset of C# programs could be translated. The usability of the translation will be demonstrated by DIVINE-based verification of selected Y Soft codes.

Thesis detail is available on is.muni.cz

YSoft SAFEQ Breeze Beta
YSoft SAFEQ Breeze Beta

SMB can now lose the IT hassle of supporting print services.