Dr. Andrei Tchaltsev (Andrey Chaltsev)
 |
I am a researcher at ITC-IRST
research center (Istituto per la Ricerca Scientifica e Tecnologica),
SRA Division (Sistemi per il
Ragionamento Automatico, i.e. Automated Reasoning Systems
Division). Address: Automated Reasoning Systems (SRA) ITC-irst Via Sommarive 18 38050 Povo (Trento) ITALY Tel. (+39) 0461 314331 email: tchaltsev@itc.it |
Areas of Interest
My primary research interests are concerned with formal methods in general and with automatic reasoning, model checking and automated synthesis in particular. Currently 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 at the Automated Reasoning System Devision
(SRA) of the Center for Scientific and Technological Research
(ITC-IRST), Trento, Italy. Member of the NuSMV model checker development team. Participate 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. |
|
| 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 | MS 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 am doing in cooperation with Alexandre Riazanov, we have developed a highly
reusable TPTP parser in Java.
| Last update 25 Sep, 2006. |
|
