Dynamic Semantics of Programming Languages and Applications to Testing

November 30, 2004
Rostislav Yavorskiy and Andrey Novikov | Steklov Mathematical Institute

In my talk I will report on the work in progress. The initial idea of the project was to test available compilers of C-like languages. Our plan is the following:

Choose a reasonable subset of the language to be tested.
Formalize the semantics of the sub-language in AsmL.
Produce tons of different programs.
Using the AsmL Test tool, build test sequences for all these programs to check the correctness of the executable binary produced by the compiler.

We started with a very simple fragment of the language (if, while, break, goto, simple function call). The next reasonable step is to add exceptions handling, arithmetical expressions, classes.

(Joint work with Andrey Novikov.)

Speaker Details

I was graduated from Moscow University in 1994. In 1998 I’ve got Ph.D. degree in mathematics from the same university. Since 1999 I am a researcher at the Steklov Mathematical Institute, Russian Academy of Sciences; since 2003 – senior researcher. The area of my scientific interests includes proof theory, model theory, formal verification, mathematical foundations of testing. In September 2002 until August 2003 I visited MSR, Foundations of Software Engineering group. During the last three months of the visit I worked on modeling and testing of distributed file system protocol. That collaboration with a product group made a strong impact on my research goals. Now, together with my students at the Moscow University, we are working on several research projects related to semantics based testing of software.My home page is http://www.mi.ras.ru/~rey

Andrey Novikov is a fifth-year student of Moscow University, Department of Mathematical Logic and Theory of Algorithms.Home page of Andrey Novikov is http://lpcs.math.msu.su/~novikov