Szoftverellenőrzési technológiák

Napjainkban egyre elterjedtebbek a szoftver ellenőrző alkalmazások és keretrendszerek. Ezek már nem csak alacsonyszintű nyelveket, hanem akár Java vagy .Net programok ellenőrzésére, verifikációjára is képesek.

A hallgató feladata, hogy egy tetszőleges eszközt megismerjen, egy alkalmazási példán keresztül bemutassa a működését, majd alkalmazási vagy algoritmikus irányba fejlesztéseket eszközöljön.

Egy pár eszköz, amelyek érdekesek, de természetesen nem csak ezek választhatóak:

• a NASA által fejlesztett Java Path Finder eszköz: http://ti.arc.nasa.gov/tech/rse/vandv/jpf/
• A Berkley egyetemen fejlesztett C programok ellenőrzésére alkalmas BLAST eszköz ( Berkeley Lazy Abstraction Software Verification Tool): http://mtc.epfl.ch/software-tools/blast/index-epfl.php
• C programok ellenőrzésére alkalmas CBMC eszköz: http://www.cprover.org/cbmc/

Ezek mellett még sok különböző algoritmus és eszköz létezik, érdemes itt is körülnézni: http://research.microsoft.com/en-us/groups/rise/default.aspx

Lehetőség van akár egy korábban, a hallgató által elkészített alkalmazás vizsgálatára, ellenőrzésére is, továbbá a hallgató elmélyülhet az eszközök által használt algoritmusokban is.

Aki érdeklődik a szoftverfejlesztés tudományosabb megközelítése iránt, annak javaslom a témát!