Oleksandr Letichevskyy
The talk is devoted to using of deductive methods in software development. Symbolic verification of formal specifications is used in requirements gathering. Formal specifications are analyzed on fullness, safety, liveness, etc. This step is based on invariants and specifications abstraction. Deductive techniques are used in software design verification, i.e. properties preserving (from more abstract models), deductive model testing, etc. Speaker also describes deducting testing of programs in C/C++. This technique allows to get maximal behaviour coverage.
Speaker: Oleksandr Letichevskyy (jr.) - Ph.D., Senior Researcher of Glushkov Institute of Cybernetics of NAS of Ukraine (Kyiv). His research interests are symbolic modeling and modeling-by-proofs, invariants technique, specifications testing, automatic proofs, inductive inference, formal specifications verification.
sdat-seminar