Informatics at SNSB (2002-2011)
General Presentation
The Informatics Department of SNSB started in 2002. Since 2009 it
functions within the Department of Mathematics as a Master programme in
mathematics-informatics, namely Logic and Formal Specification.
A complete cycle of study consists of 3 years, the last
two years being the Master curriculum (certified by the Ministry of
Education and Research of Romania).
During the preliminary year of study
students should pass exams for 3 courses. The duration of each course
is one semester. The Master programme is research rather than study
oriented. For the Master degree the students besides passing several
exams also have to develop a research oriented Master thesis.
The curriculum of the Informatics Department is mainly focused towards
formal methods for software engineering, especially algebraic
specification. A unique combination of mathematical sophistication
with high applicative value is one of the main aspects of this area.
The activity of the department is organized by a director (3 years
mandate; currently Răzvan
Diaconescu (IMAR)) and supervised
by a scientific council consisting of professors from foreign or
domestic universities.
By the power of its international relations, the Informatics Department
arranges doctoral grants for its Master graduates to
prestigious universities from Europe, Japan, and USA.
Admission of Students
SNSB does not ask for student fees. Moreover SNSB offers financial
awards for each exam, the amount being proportional to the student
performance.
Students are provisionally admitted to the preliminary year subject to
only one requirement: they should be students, usually of the 3rd
grade, of an informatics,
mathematics, or physics department of an officially recognized
university in Romania or in another country.
Full admission is achieved by passing the exam for the first semester
course Mathematical Foundations of Algebraic Specification
which is the most basic course offered by the Informatics Department.
Admission to the master programme can be achieved either automatically
as a consequence of graduating the preliminary year or else directly
by passing an examination on category theory
(recommended reading: S. Mac Lane, Categories for the
Working Mathematician, Springer 1998). However, we strongly recommend
the first way since admission directly
to the 2 years Master programme without undertaking the preliminary
year may lead to rather severe difficulties with the lectures.
Courses offered
(past
and present)
- Mathematical Foundations of Algebraic Specification
- Methodologies for Formal Specification and Verification of
Software Systems
- Structuring specifications and programs
- Formal Verification of Software Systems
- Logic Programming
- Algebra of (imperative) Programs
- Heterogenous Multi-Logic Specification
- Category Theory for Computer Science
- Model Theory for Specification and Programming
- From algebra to coalgebra; an exercise in duality
- Algebraic logic
- Logic and Automata
- Algorithmic Model Theory
- Abstract Rewriting
- Logical Foundations for Automated Reasoning
- Theory of Codes
Professors
Courses for the Informatics Department are selected by the director
based
on received proposals. Proposals should contain a summary of the
proposed
course and the cv of the respective professor.
The professors for the academic years 2005-2011 were
- Marc Aiguier (University Evry, France)
- Dietmar Berwanger (ENS Cachan, France)
- Răzvan Diaconescu (IMAR)
- Alexander Lyaletski (University Kiev, Ukraine)
- Radu Iosif (VERIMAG Grenoble, France)
- Barbara Jobstmann (VERIMAG Grenoble, France)
- Kokichi Futatsugi (Japan Advanced Institute of Science and
Technology)
- Kazuhiro Ogata (Japan Advanced Institute of Science and
Technology)
- Manuel-Antonio Martins (University Aveiro, Portugal)
- Till Mossakowski (University Bremen, Germany)
- Masaki Nakamura (Japan Advanced Institute of Science and
Technology)
- Uwe Wolter (University Bergen, Norway)
Students (past and present)
Until now all students came from either Faculty of Mathematics of
University
of Bucharest, or Faculty of Automatics of Technical University
"Politehnica"
Bucharest. Some of the most representative students are briefly
presented
below
- ţuţu, Ionuţ,
graduated 2012, thesis: On the
Instantiation of Multiple Parameterized Specifications;
currently enrolled in a PhD programme at University
of Leicester, England.
- Codruţa Gîrlea,
graduated 2011, thesis: Extended
Modal Logic; currently enrolled in a PhD programme at University
of Illinois at Urbana-Champaign.
- Marius Petria, graduated 2005,
thesis: Abstract Beth definability institutionally;
PhD from the University of Edinburgh.
- Daniel Găină, graduated 2006, thesis: Layered
Completeness; currently research asistant at Japan Advanced
Institute for Science and Technology after completion of a PhD degree
there.
- Mihai Codescu, graduated 2006, thesis: Model theory
for higher order logic with Henkin semantics; currently enrolled in
PhD programme at the University of Bremen
- Denisa Diaconescu, graduated 2009, thesis: Model
theory for multiple valued logc ; currently enrolled in PhD
programme at the University of Bucharest
- Andrei Popescu, currently IMAR member and postdoc at
Munich, PhD from the University of Illinois at Urbana-Champaign
- Traian Şerbănuţă,
Ph.D. from the University of Illinois at Urbana-Champaign
- Cristian Cucu
Some Special Achievements
In terms of the research results of the students, the SNS Master
program in Informatics may be one of the most performant worldwide.
- The research reported in the following publications has been realized
as a direct consequence of the activity at the Informatics Department.
- Răzvan Diaconescu and Ionuţ ţuţu, On the algebra of
structured specifications, Theoretical Computer Science, 412(28),
3145--3174, 2011.
- Răzvan Diaconescu and Marius Petria, Saturated models in
institutions, Arch. Math. Logic, 49(6), 693--723, 2010.
- Mihai Codescu and Daniel Găină, Birkhoff Completeness in
Institutions, Logica Universalis, 2(2), 277-309, 2008.
- Marius Petria and Răzvan Diaconescu, Abstract Beth
definability in institutions, J. Symbolic Logic, 71(3), 1002-1028,
2006.
- Daniel Găină and Andrei Popescu, An institution-independent
generalization
of Tarski's Elementary Chain Theorem, J. Logic and Computation,
16(6), 713-735, 2006.
- Daniel Găină and Andrei Popescu, An institution-independent
proof
of Robinson consistency theorem, Studia Logica, 85(1), 41-73,
2007.
- 1 student gave a presentation at Second Romanian-Japanese
Algebraic Specification Workshop held in Sinaia, Romania, March
2011.
- 2 students attended the
JAIST
Advanced
School on Formal Specification and System Verification,
held in Kanazawa, Japan, March 2010.
- The Informatics Department co-organized
Sinaia
School on Formal
Verification of Software Systems (3-10 March 2008), a
post-graduate
school with international participation from Romania, Japan, Greece,
Great
Britain, Germany.
- 4 students attended the European Summer
School on Logics
for Specification Languages, organized by Dines Bjorner at
Stara Lesna,
Slovakia, June 2004.
One of them (Daniel Găină) received a special award
given by the CASL course.
Răzvan Diaconescu, Informatics
Department, SNSB, January 2012