Research Interests

  • Logics and their applications to computing
  • Algebraic specification, formal methods for software engineering
  • Algorithms, Programming using logics, Term Rewriting and Rewriting Logic

Professional Experience

Associate Professor

2013 – Present
Faculty of Mathematics and Computer Science
University of Bucharest

Research Consultant

2012 – Present
Designing state-of-art analysis tools based on cutting-edge research

  • Using the K Framework to build a semantics for the C++ language
  • Sound and maximal causal models for predicting concurrency problems in Java and C

Postdoctoral Scientific Researcher

2011 – 2013
University "Alexandru Ioan Cuza", Iași

Project leader for the K semantic framework.

Postdoctoral Research Associate

2011 – 2012
Information Trust Institute
University of Illinois at Urbana-Champaign

Research Assistant

2004 – 2010
Formal Systems Laboratory
University of Illinois at Urbana-Champaign

Summer intern

Summer 2007
Google, New York

Summer intern

Summer 2005
Testing, Verification and Measurement
Microsoft Research, Redmond


Declarative Programming (Fall Semester) - An introductory course on (functional) declarative programming concepts and implementations.
Programming Languages Semantics (Spring Semester) - An introductory course on (operational) semantics of programming languages. Concepts covered: designing interpreters; defining type systems; proving program equivalence and type safety.
Ideas for BSc Thesis Projects (in Romanian) - If you are interested in working for a BSc thesis under my supervision, please checked the linked page for possible ideas.


PhD Thesis

A Rewriting Approach to Concurrent Programming Language Design and Semantics. PhD Thesis, University of Illinois at Urbana-Champaign. December 2010.

Selected Papers

Maximal Causal Models for Sequentially Consistent Systems. Traian Florin Serbanuta, Feng Chen and Grigore Rosu. RV'12, LNCS 7687, pp 136-150. 2012
An Overview of the K Semantic Framework. Grigore Rosu and Traian Florin Serbanuta. J.LAP, Volume 79(6), pp 397-434. 2010
A Rewriting Logic Approach to Operational Semantics. Traian Florin Serbanuta, Grigore Rosu and Jose Meseguer. Information and Computation, Volume 207(2), pp 305-340. 2009
Extending Parikh Matrices. Traian Florin Serbanuta. J. of TCS, Volume 310(1), pp 233-246. 2004