ENGLISH / MAGYAR
Kövess
minket

Programhelyesség bizonyítás

2021-2022/I.
Izsó Tamás

A kitűzött feladat C nyelven írt függvények parciális helyességének bizonyítására alkalmas program megtervezése és létrehozása. A logikai állítások kiértékeléséhez a Z3 vagy Yices SMT solver, míg a C nyelv AST átalakítására a clang (clang.llvm.org) program kerülne felhasználásra.

Egy megvalósított rendszert a http://theory.stanford.edu/~arbrad/pivc/ honlapon találhatunk.

Irodalom: Zohar Manna, Programozáselmélet; Aaron R. Bradley, Zohar Manna: The Calculus of Computation


1
0