Curriculum Vitae, Traian Florin Serbanuta
From FSL
(Back to Traian Florin Serbanuta's page)
October 2012
Personal Data
- Place of Birth: Braşov, Romania
- Religion: Orthodox Christian
- Married, two children
Affiliation and Contact Data
- Department of Computer Science
- Address: Academiei 14, sector 1 010014, BUCUREȘTI, ROMANIA
- Tel. +40 21 314 2863
- Fax +40 21 315 6990
- email: traian.serbanuta@gmail.com
- homepage: http://fsl.cs.uiuc.edu/index.php/Traian_Florin_Serbanuta
Research Interests
- - Logics and their applications to computing
- - Algebraic specifications and formal methods for software engineering
- - Algorithms, Programming using logics, Rewriting
Education
- 2004-2010
- Ph.D, Department of Computer Science, University of Illinois at Urbana-Champaign
- Advisor: Grigore Rosu
- Committee: Tom Ball, Darko Marinov, Jose Meseguer, Madhusudan Parthasarathy
- 2002-2004
- Superior Normal School of Bucharest, Department of Informatics
- 2002-2004
- M.S., Foundations of Computer Science, Faculty of Mathematics and Informatics, University of Bucharest.
- M.S. Thesis: "Institutions and Logic Programming Compiling"
- Advisors: Razvan Diaconescu and Virgil Emil Cazanescu
- 1998-2002
- B.A., Computer Science, Faculty of Mathematics and Informatics, University of Bucharest
- B.A. Thesis: "Hiding information in text using LR(k) grammars"
- Thesis Advisor: Professor Adrian Atanasiu
Professional Experience
- 2012-present
- Postdoctoral Scientific Researcher at University Alexandru Ioan Cuza of Iasi
- 2011-2012
- Postdoctoral Research Associate, Information Trust Institute, University of Illinois at Urbana-Champaign
- 2004-2010
- Research Assistant within the Formal Systems Laboratory, Department of Computer Science, University of Illinois at Urbana-Champaign
- 2003-2009
- Research Assistant, at Chair of Foundations of Computer Science, University of Bucharest
- 2000-2001
- IT developer for Popnet-Agentscape Romania, member of the Natural Language Processing Team
- Job Description: research and implementation of text classifiers
- Summer 2007
- Summer intern at Google New York
- Mentor: Bogdan Caprita
- Coauthored (with Bogdan Caprita) a patent related to traffic analysis technology
- Summer 2005
- Summer intern at Microsoft Research Redmond, Testing, Verification and Measurement
- Mentor: Madan Musuvathi
Awards
- 2000
- 15th place at the The 24th ACM International Collegiate Programming Contest World Finals
- 1999
- 1st place at the The SouthEastern European Regional Contest of the ACM ICPC
- 1998
- 3rd prize at the Romanian National Olympiad of Mathematics
Selected Publications
- An Overview of the K Semantic Framework
- Grigore Rosu and Traian Florin Serbanuta
- J.LAP, Volume 79(6), pp 397-434. 2010
- Abstract. K is an executable semantic framework in which programming languages, calculi, as well as type systems or formal analysis tools can be defined, making use of configurations, omputations and rules. Configurations organize the system/program state in units called cells, which are labeled and can be nested. Computations carry "computational meaning" as special nested list structures sequentializing computational tasks, such as fragments of program; in particular, computations extend the original language or calculus syntax. K (rewrite) rules generalize conventional rewrite rules by making explicit which parts of the term they read, write, or do not care about. This distinction makes K a suitable framework for defining truly concurrent languages or calculi, even in the presence of sharing. Since computations can be handled like any other terms in a rewriting environment, that is, they can be matched, moved from one place to another in the original term, modified, or even deleted, K is particularly suitable for defining control-intensive language features such as abrupt termination, exceptions, or call/cc.
This paper gives an overview of the K framework: what it is, how it can be used, and where it has been used so far. It also proposes and discusses the K definition of CHALLENGE, a programming language that aims to challenge and expose the limitations of existing semantic frameworks.
- Abstract. K is an executable semantic framework in which programming languages, calculi, as well as type systems or formal analysis tools can be defined, making use of configurations, omputations and rules. Configurations organize the system/program state in units called cells, which are labeled and can be nested. Computations carry "computational meaning" as special nested list structures sequentializing computational tasks, such as fragments of program; in particular, computations extend the original language or calculus syntax. K (rewrite) rules generalize conventional rewrite rules by making explicit which parts of the term they read, write, or do not care about. This distinction makes K a suitable framework for defining truly concurrent languages or calculi, even in the presence of sharing. Since computations can be handled like any other terms in a rewriting environment, that is, they can be matched, moved from one place to another in the original term, modified, or even deleted, K is particularly suitable for defining control-intensive language features such as abrupt termination, exceptions, or call/cc.
- PDF, Slides(PPTX), Slides(PDF), K Tool, J.LAP, BIB
You can also check The complete list of Traian's publications.
Presentations
- 2010
- WRLA'10 - "K-Maude: A Rewriting Based Tool for Semantics of Programming Languages" (presentation and tool demo)
- 2008
- 2007
- 2006
- WRLA'06 - Co-organizer and co-presenter of the Rewrite Engines Competition
- FOSSACS'06 - A Semantic Approach to Interpolation
- 2005
- MSR Redmond - Interleaving Boolean and theory reasoning in a SAT-based theorem prover (end of internship talk)
- Reviewed papers for
- J. of TCS, LOPSTR'06, WRS'06, ICCGI'06, RTA'07, FMOODS'07, WRLA'08, RTA'08, WADT'08, AMAST'08, FOSSACS'09
