Dr. Andrei Tchaltsev (Andrey Chaltsev)


I am a researcher in the Embedded Systems Research Unit of Fondazione Bruno Kessler (FBK), a scientific research center in northen Italy.

Address:
  Embedded Systems Unit
  Fondazione Bruno Kessler
  Via Sommarive 18
  38123 Povo (Trento)
  ITALY

Tel. (+39) 0461 314343
email: andrei.tchaltsev@gmail.com 


Areas of Interest

My primary research interests are concerned with formal methods in general and with automatic reasoning, model checking, realizability checking and automated synthesis in particular.
I am a member of the NuSMV model checker development team.
During my PhD study in The University of Manchester I was doing research on practical semantics of programming languages and self-validating compilation.

Short CV

2004 - to date   
Researcher in the Embedded Systems Research Unit of Fondazione Bruno Kessler (FBK) scientific research center, Trento, Italy. Member of the NuSMV model checker development team.
Participated in the development of RATSY, Requirements Analysis Tool with Synthesis. Took part in PROSYD project in research on property realizability.
Participated in development of NuSMV extension to deal with QF_UFBV32 problems of Satisfiability Modulo Theories Library (SMT-LIB). Our tool took the third place in the corresponding division of SMT-COMP 2006.
Took part in several joint projects, aimed at verification of industrial-size safety critical software. In particular, in joint project with ALES (Italy, Rome) and Hamilton (USA) on verification of aircraft controlling systems, and in project with Ansaldo, a technology company operating in Italian Railway and Transportation Systems, on verification of signaling and automation software.
2000 - 2004   
PhD study in the Computer Science Department, The University of Manchester, UK, superwised by Prof. Andrei Voronkov.
Thesis: "Self-Validating Compilation based on Phase Semantics" (PS and PDF versions).
The source code of the self-validating C compiler described in the thesis can be found here.
1996 - 2000   
BSc Degree in Physics with specialization in Engineering Physics and Computational Support for Experimental Physics, Novosibirsk State University, Russia.


Software

The NuSMV symbolic model checker official site.

Source code for the prototype self-validating C compiler that I developed as a part of my PhD study.

For some experiments I've done in cooperation with Alexandre Riazanov, we have developed a highly
reusable TPTP parser in Java.
Last update Nov, 2011.