traiansf.github.io

Traian Florin Șerbănuță

Associate Professor · Researcher in Formal Methods · Software Engineer

Download PDF

Education

PhD in Computer Science

University of Illinois, Urbana-Champaign
2010

Dissertation: A Rewriting Approach to Concurrent Programming Language Design and Semantics

Advisor: Grigore Roșu

Committee: Thomas Ball, Darko Marinov, José Meseguer, Madhusudan Parthasarathy

Master in Computer Science

University of Bucharest
2004

Dissertation: Institutional Concepts in First-Order Logic, Parameterized Specification Theory, and Logic Programming

Advisors: Răzvan Diaconescu, Virgil Emil Căzănescu

Bachelor in Computer Science

University of Bucharest
2002

Dissertation: Information Hiding in Text Using LR(k) Grammars

Advisor: Adrian Atanasiu

Experience

Associate Professor of Computer Science

University of Bucharest, Faculty of Mathematics and Informatics
2013–Present

Courses developed and taught, with all materials openly published:

Supervise graduate students and serve on departmental committees.

Co-founder and Vice-President

Institute for Logic and Data Science
2022–Present

Non-profit research institute (ilds.ro) bringing together academic and industry researchers in logic and data science, with an active program of conferences, workshops, weekly seminars, and hosted research projects. Most involved in the Working Formal Methods Symposium (FROM 2024, 2026), the Deep Blockchain Fundamentals workshop, the weekly Logic seminar, and matching-logic research.

Consultant and Researcher

Asymptotic
2026–Present

Prototyping AI-assisted, Lean-based provers for programming languages. Lead author of Rust-Prover, a Lean 4–backed verifier for Rust: specifications and Rust code are translated into Lean theorems that LLM agents prove, with Lean’s kernel as the final check. It proved all 1325 theorems of the 1007-problem VeriContest benchmark.

Consultant and Researcher

Pi Squared, Inc.
2024–2026

Core Rust engineer on Pi Squared’s verifiable-computing and universal-settlement infrastructure (“Proof of Proof”). Work spans five phases of the platform’s evolution:

  • Pi² research prototype (2024) — Metamath proof checkers compiled to five zkVM backends (RISC Zero, SP1, Nexus, Lurk, Delphinus), with driver tooling and cross-backend benchmarking.
  • Blocks to Circom ZK pipeline (2025) — Rust toolchain compiling the Blocks DSL into Circom subcircuits and generating end-to-end ZK certificates for block instantiations.
  • Verifiable Settlement Layer (2025) — claim-based settlement layer where submitted claims reach quorum and are recorded as signed settlements.
  • FastSet validator and proxy (2025–2026) — validator and client-facing proxy for the FastSet protocol.
  • Fast Shop / agentic AI commerce (2026) — Universal Commerce Protocol integration with region-aware multi-region delivery, a Shopify backend, and an MCP-exposed commerce surface.

Consultant and Researcher

Runtime Verification, Inc.
2012–2023

Long-running principal contributor across four projects:

  • K Framework — Java implementation (2012–2015) — executor/debugger internals for the Maude and Java backends: LTL model-checking, search-graph extraction, and AC matching.
  • RV-Predict — race & deadlock detector (2012–2017) — maximal-causal-model predictive race detection for Java and C/C++ (via an LLVM instrumentation pass), scaled to a 1M-variable cap.
  • K Haskell Backend — symbolic-execution prover (2017–2022) — all-path/one-path reachability-logic prover with SMT integration, applied to the formal semantics of the EVM, WebAssembly, and IELE.
  • CBC-Casper / VLSM consensus in Coq (2022–2023) — Coq modelling and verification of blockchain protocols, including one of the first safety formalizations of CBC Casper.

Postdoctoral Research Fellow

Alexandru Ioan Cuza University, Iași (FMSE Laboratory)
2011–2013

Formal methods research in software engineering. Coordinated the team developing the K Framework.

Postdoctoral Research Associate

University of Illinois, Urbana-Champaign (Information Trust Institute)
2011–2012

Formal systems and verification research.

Research Assistant

University of Illinois, Urbana-Champaign (FSL Laboratory)
2004–2010

Assisted in research on formal semantics, rewriting logic, and programming language design. Designed and prototyped (in Maude) the K semantic framework.

Teaching Assistant

University of Bucharest, Department of Computer Science Fundamentals
2003–2004

Supported undergraduate courses in programming, discrete mathematics, and computer science theory.

Summer Intern

Google, New York
2007

Co-authored a patent application on web traffic analysis methods (with Bogdan Căpriță).

Summer Intern

Microsoft Research, Redmond (Testing, Verification, and Measurement Group)
2005

Contributed an equality theory propagation core for the Zap automated theorem prover.

Programmer

Popnet-Agentscape Romania, Natural Language Processing Team
2000–2001

Implemented classification algorithms for one of the first AI agents.

Open-source Projects

Personal research and tooling outside employer-affiliated work; full list at https://github.com/traiansf.

Skills

  • Formal methods and verification
  • Programming language semantics
  • AI-assisted software development
  • LLM agents for theorem proving
  • Rewriting logic
  • K Framework
  • Temporal logics
  • Model checking
  • Specification and verification techniques

Programming Languages

  • Rust
  • Haskell
  • Coq / Rocq
  • Java
  • C / C++
  • K / Maude
  • Python
  • Lean 4
  • Prolog
  • JavaScript / TypeScript
  • PHP

Languages

  • Romanian (native)
  • English (fluent)
  • French (basic)

Publications

55 articles · h-index 22 · 2178 citations (Google Scholar, as of October 2026)

Top 20 by citations (Google Scholar, October 2026). Full record: Google Scholar · DBLP.

  1. Roșu, Grigore and Traian Florin Șerbănuță. “An Overview of the K Semantic Framework.” Journal of Logic and Algebraic Programming, Vol. 79, No. 6, pp. 397-434, 2010. 673

  2. Chen, Feng, Traian Florin Șerbănuță, and Grigore Roșu. “jPredictor: a predictive runtime analysis tool for Java.” ICSE ’08: Proceedings of the 30th International Conference on Software Engineering, pp. 221-230, 2008. 155

  3. Șerbănuță, Traian Florin, Grigore Roșu, and José Meseguer. “A Rewriting Logic Approach to Operational Semantics.” Information and Computation, Vol. 207, No. 2, pp. 305-340, 2009. 129

  4. Ștefănescu, Andrei, Ștefan Ciobâcă, Radu Mereuta, Brandon M Moore, Traian Florin Șerbănuță, and Grigore Roșu. “All-Path Reachability Logic.” Logical Methods in Computer Science, Vol. 15, Issue 2, 2019. 117

  5. Luo, Qingzhou, Yi Zhang, Choonghwan Lee, Dongyun Jin, Patrick O’Neil Meredith, Traian Florin Șerbănuță, and Grigore Roșu. “RV-Monitor: Efficient Parametric Runtime Verification with Simultaneous Properties.” Runtime Verification (RV’14), LNCS Vol. 8734, pp. 285-300, 2014. 108

  6. Șerbănuță, Traian Florin, Feng Chen, and Grigore Roșu. “Maximal Causal Models for Sequentially Consistent Systems.” Runtime Verification (RV’12), LNCS Vol. 7687, pp. 136-150, 2013. 105

  7. Șerbănuță, Traian Florin and Grigore Roșu. “K-Maude: A Rewriting Based Tool for Semantics of Programming Languages.” Rewriting Logic and Its Applications (WRLA’10), LNCS Vol. 6381, pp. 104-122, 2010. 74

  8. Șerbănuță, Traian Florin. “Extending Parikh matrices.” Theoretical Computer Science, Vol. 310, No. 1-3, pp. 233-246, 2004. 66

  9. Roșu, Grigore and Traian Florin Șerbănuță. “K Overview and SIMPLE Case Study.” Proceedings of K’11, ENTCS Vol. 304, pp. 3-56, 2014. 64

  10. Roșu, Grigore, Wolfram Schulte, and Traian Florin Șerbănuță. “Runtime Verification of C Memory Safety.” Runtime Verification (RV’09), LNCS Vol. 5779, pp. 132-151, 2009. 64

  11. Șerbănuță, Virgil Nicolae and Traian Florin Șerbănuță. “Injectivity of the Parikh matrix mappings revisited.” Fundamenta Informaticae, Vol. 73, No. 1-2, pp. 265-283, 2006. 63

  12. Șerbănuță, Traian Florin, Andrei Arusoaie, David Lazar, Chucky Ellison, Dorel Lucanu, and Grigore Roșu. “The K Primer (version 3.3).” Proceedings of K’11, ENTCS Vol. 304, pp. 57-80, 2014. 54

  13. Kasampalis, Theodoros, Dwight Guth, Brandon Moore, Traian Florin Șerbănuță, Yi Zhang, Daniele Filaretti, Virgil Șerbănuță, Ralph Johnson, and Grigore Roșu. “IELE: A Rigorously Designed Language and Tool Ecosystem for the Blockchain.” Formal Methods (FM’19), pp. 593-610, 2019. 46

  14. Șerbănuță, Traian Florin and Grigore Roșu. “Computationally Equivalent Elimination of Conditions.” Rewriting Techniques and Applications (RTA’06), LNCS Vol. 4098, pp. 19-34, 2006. 41

  15. Rusu, Vlad, Dorel Lucanu, Traian-Florin Șerbănuță, Andrei Arusoaie, Andrei Ștefănescu, and Grigore Roșu. “Language Definitions as Rewrite Theories.” Journal of Logical and Algebraic Methods in Programming, Vol. 85, No. 1, pp. 98-120, 2016. 34

  16. Daian, Philip, Ylies Falcone, Patrick Meredith, Traian Florin Șerbănuță, Akihito Iwai, Shin’ichi Shiriashi, and Grigore Roșu. “RV-Android: Efficient Parametric Android Runtime Verification, a Brief Tutorial.” Runtime Verification (RV’15), LNCS Vol. 9333, pp. 342-357, 2015. 31

  17. Hills, Mark, Traian Florin Șerbănuță, and Grigore Roșu. “A Rewrite Framework for Language Definitions and for Generation of Efficient Interpreters.” Rewriting Logic and Its Applications (WRLA’06), ENTCS Vol. 176, No. 4, pp. 215-231, 2007. 31

  18. Lucanu, Dorel, Traian Florin Șerbănuță, and Grigore Roșu. “K Framework Distilled.” Rewriting Logic and Its Applications (WRLA’12), LNCS Vol. 7571, pp. 31-53, 2012. 29

  19. Ellison, Chucky, Traian Florin Șerbănuță, and Grigore Roșu. “A Rewriting Logic Approach to Type Inference.” Recent Trends in Algebraic Development Techniques (WADT’08), LNCS Vol. 5486, pp. 135-151, 2009. 28

  20. Șerbănuță, Traian Florin, Gheorghe Ștefănescu, and Grigore Roșu. “Defining and Executing P Systems with Structured Data in K.” Membrane Computing (WMC’08), LNCS Vol. 5391, pp. 374-393, 2009. 28

Formal Methods for Software Correctness · Verification Engineer · Associate Professor

Download PDF

Education

PhD in Computer Science

University of Illinois, Urbana-Champaign
2010

Master in Computer Science

University of Bucharest
2004

Bachelor in Computer Science

University of Bucharest
2002

Experience

Associate Professor of Computer Science

University of Bucharest, Faculty of Mathematics and Informatics
2013–Present

Designed and taught courses across software modelling, declarative & concurrent programming, programming-language semantics, program verification, and machine learning — all course materials openly published.

Supervise graduate students and serve on departmental committees.

Consultant and Researcher

Asymptotic
2026–Present

Prototyping AI-assisted, Lean-based provers for programming languages. Lead author of Rust-Prover, a Lean 4–backed verifier for Rust: specifications and Rust code are translated into Lean theorems that LLM agents prove, with Lean’s kernel as the final check. It proved all 1325 theorems of the 1007-problem VeriContest benchmark.

Consultant and Researcher

Pi Squared, Inc.
2024–2026

Core Rust engineer on Pi Squared’s verifiable-computing and universal-settlement infrastructure (“Proof of Proof”). Work spans five phases of the platform’s evolution:

  • Pi² research prototype (2024) — Metamath proof checkers compiled to five zkVM backends (RISC Zero, SP1, Nexus, Lurk, Delphinus), with driver tooling and cross-backend benchmarking.
  • Blocks to Circom ZK pipeline (2025) — Rust toolchain compiling the Blocks DSL into Circom subcircuits and generating end-to-end ZK certificates for block instantiations.
  • Verifiable Settlement Layer (2025) — claim-based settlement layer where submitted claims reach quorum and are recorded as signed settlements.
  • FastSet validator and proxy (2025–2026) — validator and client-facing proxy for the FastSet protocol.
  • Fast Shop / agentic AI commerce (2026) — Universal Commerce Protocol integration with region-aware multi-region delivery, a Shopify backend, and an MCP-exposed commerce surface.

Consultant and Researcher

Runtime Verification, Inc.
2012–2023

Long-running principal contributor across four projects:

  • K Framework — Java implementation (2012–2015) — executor/debugger internals for the Maude and Java backends: LTL model-checking, search-graph extraction, and AC matching.
  • RV-Predict — race & deadlock detector (2012–2017) — maximal-causal-model predictive race detection for Java and C/C++ (via an LLVM instrumentation pass), scaled to a 1M-variable cap.
  • K Haskell Backend — symbolic-execution prover (2017–2022) — all-path/one-path reachability-logic prover with SMT integration, applied to the formal semantics of the EVM, WebAssembly, and IELE.
  • CBC-Casper / VLSM consensus in Coq (2022–2023) — Coq modelling and verification of blockchain protocols, including one of the first safety formalizations of CBC Casper.

Postdoctoral Research Fellow

Alexandru Ioan Cuza University, Iași (FMSE Laboratory)
2011–2013

Postdoctoral Research Associate

University of Illinois, Urbana-Champaign (Information Trust Institute)
2011–2012

Research Assistant

University of Illinois, Urbana-Champaign (FSL Laboratory)
2004–2010

Teaching Assistant

University of Bucharest, Department of Computer Science Fundamentals
2003–2004

Summer Intern

Google, New York
2007

Summer Intern

Microsoft Research, Redmond (Testing, Verification, and Measurement Group)
2005

Programmer

Popnet-Agentscape Romania, Natural Language Processing Team
2000–2001

Open-source Projects

Personal research and tooling outside employer-affiliated work; full list at https://github.com/traiansf.

Skills

  • Formal methods and verification
  • Programming language semantics
  • AI-assisted software development
  • LLM agents for theorem proving
  • Rewriting logic
  • K Framework
  • Temporal logics
  • Model checking
  • Specification and verification techniques

Programming Languages

  • Rust
  • Haskell
  • Coq / Rocq
  • Java
  • C / C++
  • K / Maude
  • Python
  • Lean 4
  • Prolog
  • JavaScript / TypeScript
  • PHP

Languages

  • Romanian (native)
  • English (fluent)
  • French (basic)

Publications

55 articles · h-index 22 · 2178 citations (Google Scholar, as of October 2026)

Associate Professor · Researcher in Formal Methods · Software Engineer

Download PDF

Education

PhD in Computer Science

University of Illinois, Urbana-Champaign
2010

Master in Computer Science

University of Bucharest
2004

Bachelor in Computer Science

University of Bucharest
2002

Experience

Associate Professor of Computer Science

University of Bucharest, Faculty of Mathematics and Informatics
2013–Present

Co-founder and Vice-President

Institute for Logic and Data Science
2022–Present

Consultant and Researcher

Asymptotic
2026–Present

Consultant and Researcher

Pi Squared, Inc.
2024–2026

Consultant and Researcher

Runtime Verification, Inc.
2012–2023

Postdoctoral Research Associate

University of Illinois, Urbana-Champaign (Information Trust Institute)
2011–2012

Research Assistant

University of Illinois, Urbana-Champaign (FSL Laboratory)
2004–2010

Summer Intern

Google, New York
2007

Summer Intern

Microsoft Research, Redmond (Testing, Verification, and Measurement Group)
2005

Skills

  • Formal methods and verification
  • Programming language semantics
  • AI-assisted software development

Programming Languages

  • Rust
  • Haskell
  • Coq / Rocq
  • Java
  • C / C++

Languages

  • Romanian (native)
  • English (fluent)
  • French (basic)

Publications

55 articles · h-index 22 · 2178 citations (Google Scholar, as of October 2026)

List of Publications

Download PDF

Publications

55 articles · h-index 22 · 2178 citations (Google Scholar, as of October 2026)

Reverse chronological within each category. Citation counts are from Google Scholar (October 2026); see also DBLP.

Journal Articles

  1. Leuștean, Ioana, Natalia Moangă, and Traian Florin Șerbănuță. “Many-sorted hybrid modal languages.” Journal of Logical and Algebraic Methods in Programming, Vol. 120, 100644, 2021. 3

  2. Leuștean, Ioana, Natalia Moangă, and Traian Florin Șerbănuță. “A many-sorted polyadic modal logic.” Fundamenta Informaticae, Vol. 173, No. 2-3, pp. 191-215, 2020. 12

  3. Ștefănescu, Andrei, Ștefan Ciobâcă, Radu Mereuta, Brandon M Moore, Traian Florin Șerbănuță, and Grigore Roșu. “All-Path Reachability Logic.” Logical Methods in Computer Science, Vol. 15, Issue 2, 2019. 117

  4. Arusoaie, Andrei, Ștefan Ciobâcă, Dorel Lucanu, Grigore Roșu, Vlad Rusu, and Traian-Florin Șerbănuță. “Program Logics and Their Applications.” Revue Roumaine de Mathématiques Pures et Appliquées, Vol. 62, No. 1, pp. 137-154, 2017.

  5. Rusu, Vlad, Dorel Lucanu, Traian-Florin Șerbănuță, Andrei Arusoaie, Andrei Ștefănescu, and Grigore Roșu. “Language Definitions as Rewrite Theories.” Journal of Logical and Algebraic Methods in Programming, Vol. 85, No. 1, pp. 98-120, 2016. 34

  6. Frei, Regina, Traian Florin Șerbănuță, and Giovanna Di Marzo Serugendo. “Self-organising assembly systems formally specified in Maude.” Journal of Ambient Intelligence and Humanized Computing, Vol. 5, No. 4, pp. 491-510, 2014. 12

  7. Frei, Regina, Giovanna Di Marzo Serugendo, and Traian Florin Șerbănuță. “Ambient intelligence in self-organising assembly systems using the chemical reaction model.” Journal of Ambient Intelligence and Humanized Computing, Vol. 1, No. 3, pp. 163-184, 2010. 26

  8. Roșu, Grigore and Traian Florin Șerbănuță. “An Overview of the K Semantic Framework.” Journal of Logic and Algebraic Programming, Vol. 79, No. 6, pp. 397-434, 2010. 673

  9. Chira, Camelia, Traian Florin Șerbănuță, and Gheorghe Ștefănescu. “P systems with control nuclei: The concept.” Journal of Logic and Algebraic Programming, Vol. 79, No. 6, pp. 326-333, 2010. 9

  10. Popescu, Andrei, Traian Florin Șerbănuță, and Grigore Roșu. “A Semantic Approach to Interpolation.” Theoretical Computer Science, Vol. 410, No. 12-13, pp. 1109-1128, 2009. 20

  11. Șerbănuță, Traian Florin, Grigore Roșu, and José Meseguer. “A Rewriting Logic Approach to Operational Semantics.” Information and Computation, Vol. 207, No. 2, pp. 305-340, 2009. 129

  12. Șerbănuță, Virgil Nicolae and Traian Florin Șerbănuță. “Injectivity of the Parikh matrix mappings revisited.” Fundamenta Informaticae, Vol. 73, No. 1-2, pp. 265-283, 2006. 63

  13. Șerbănuță, Traian Florin. “Extending Parikh matrices.” Theoretical Computer Science, Vol. 310, No. 1-3, pp. 233-246, 2004. 66

Conference and Workshop Papers

  1. Tušil, Jan, Traian Florin Șerbănuță, and Jan Obdržálek. “Cartesian Reachability Logic: A Language-parametric Logic for Verifying k-Safety Properties.” Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2023), pp. 405-456, 2023. 1

  2. Trufaș, Dafina, Ioan Teodorescu, Denisa Diaconescu, Traian Florin Șerbănuță, and Vlad Zamfir. “Asynchronous Muddy Children Puzzle (work in progress).” Working Formal Methods Symposium (FROM 2023), EPTCS Vol. 389, pp. 152-166, 2023.

  3. Li, Elaine, Traian Florin Șerbănuță, Denisa Diaconescu, Vlad Zamfir, and Grigore Roșu. “Formalizing Correct-by-Construction Casper in Coq.” IEEE International Conference on Blockchain and Cryptocurrency (ICBC 2020), pp. 1-3, 2020. 19

  4. Leuștean, Ioana, Natalia Moangă, and Traian Florin Șerbănuță. “From Hybrid Modal Logic to Matching Logic and Back.” Working Formal Methods Symposium (FROM 2019), EPTCS Vol. 303, pp. 16-31, 2019. 3

  5. Leuștean, Ioana, Natalia Moangă, and Traian Florin Șerbănuță. “Operational Semantics and Program Verification Using Many-Sorted Hybrid Modal Logic.” Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX’19), 2019. 10

  6. Kasampalis, Theodoros, Dwight Guth, Brandon Moore, Traian Florin Șerbănuță, Yi Zhang, Daniele Filaretti, Virgil Șerbănuță, Ralph Johnson, and Grigore Roșu. “IELE: A Rigorously Designed Language and Tool Ecosystem for the Blockchain.” Formal Methods (FM’19), pp. 593-610, 2019. 46

  7. Roșu, Grigore and Traian Florin Șerbănuță. “Matching Logic: Syntax and Semantics.” Working Formal Methods Symposium (FROM 2017), 2017.

  8. Daian, Philip, Dwight Guth, Chris Hathhorn, Yilong Li, Edgar Pek, Manasvi Saxena, Traian Florin Șerbănuță, and Grigore Roșu. “Runtime Verification at Work: A Tutorial.” Runtime Verification (RV’16), pp. 46-67, 2016. 12

  9. Șerbănuță, Traian Florin and Liviu P. Dinu. “Maximally Parallel Contextual String Rewriting.” Rewriting Logic and Its Applications (WRLA’16), pp. 152-166, 2016.

  10. Daian, Philip, Ylies Falcone, Patrick Meredith, Traian Florin Șerbănuță, Akihito Iwai, Shin’ichi Shiriashi, and Grigore Roșu. “RV-Android: Efficient Parametric Android Runtime Verification, a Brief Tutorial.” Runtime Verification (RV’15), LNCS Vol. 9333, pp. 342-357, 2015. 31

  11. Chiriță, Claudia Elena and Traian Florin Șerbănuță. “An Institutional Foundation for the K Semantic Framework.” Recent Trends in Algebraic Development Techniques (WADT’14), LNCS Vol. 9463, pp. 9-29, 2015. 4

  12. Luo, Qingzhou, Yi Zhang, Choonghwan Lee, Dongyun Jin, Patrick O’Neil Meredith, Traian Florin Șerbănuță, and Grigore Roșu. “RV-Monitor: Efficient Parametric Runtime Verification with Simultaneous Properties.” Runtime Verification (RV’14), LNCS Vol. 8734, pp. 285-300, 2014. 108

  13. Ștefănescu, Andrei, Ștefan Ciobâcă, Radu Mereuta, Brandon M Moore, Traian Florin Șerbănuță, and Grigore Roșu. “All-Path Reachability Logic.” Rewriting and Typed Lambda Calculi (RTA-TLCA’14), LNCS Vol. 8560, pp. 425-440, 2014.

  14. Arusoaie, Andrei, Dorel Lucanu, Vlad Rusu, Traian-Florin Șerbănuță, Andrei Ștefănescu, and Grigore Roșu. “Language Definitions as Rewrite Theories.” Rewriting Logic and Its Applications (WRLA’14), LNCS, pp. 97-112, 2014.

  15. Roșu, Grigore and Traian Florin Șerbănuță. “K Overview and SIMPLE Case Study.” Proceedings of K’11, ENTCS Vol. 304, pp. 3-56, 2014. 64

  16. Șerbănuță, Traian Florin, Andrei Arusoaie, David Lazar, Chucky Ellison, Dorel Lucanu, and Grigore Roșu. “The K Primer (version 3.3).” Proceedings of K’11, ENTCS Vol. 304, pp. 57-80, 2014. 54

  17. Șerbănuță, Traian Florin. “Rewriting Semantics and Analysis of Concurrency Features for a C-like Language.” Proceedings of K’11, ENTCS Vol. 304, pp. 167-182, 2014. 2

  18. Șerbănuță, Traian Florin, Feng Chen, and Grigore Roșu. “Maximal Causal Models for Sequentially Consistent Systems.” Runtime Verification (RV’12), LNCS Vol. 7687, pp. 136-150, 2013. 105

  19. Șerbănuță, Traian Florin. “Programming Language Semantics using K — true concurrency through term graph rewriting.” EPTCS Vol. 110, p. 2, 2013.

  20. Șerbănuță, Traian Florin and Grigore Roșu. “A Truly Concurrent Semantics for the K Framework Based on Graph Transformations.” Graph Transformations (ICGT’12), LNCS Vol. 7562, pp. 294-310, 2012. 16

  21. Lazar, David, Andrei Arusoaie, Traian Florin Șerbănuță, Chucky Ellison, Radu Mereuta, Dorel Lucanu, and Grigore Roșu. “Executing Formal Semantics with the K Tool.” Formal Methods (FM’12), LNCS Vol. 7436, pp. 267-271, 2012. 21

  22. Lucanu, Dorel, Traian Florin Șerbănuță, and Grigore Roșu. “K Framework Distilled.” Rewriting Logic and Its Applications (WRLA’12), LNCS Vol. 7571, pp. 31-53, 2012. 29

  23. Arusoaie, Andrei, Traian Florin Șerbănuță, Chucky Ellison, and Grigore Roșu. “Making Maude Definitions More Interactive.” Rewriting Logic and Its Applications (WRLA’12), LNCS Vol. 7571, pp. 83-98, 2012. 4

  24. Șerbănuță, Traian Florin and Grigore Roșu. “K-Maude: A Rewriting Based Tool for Semantics of Programming Languages.” Rewriting Logic and Its Applications (WRLA’10), LNCS Vol. 6381, pp. 104-122, 2010. 74

  25. Ellison, Chucky, Traian Florin Șerbănuță, and Grigore Roșu. “A Rewriting Logic Approach to Type Inference.” Recent Trends in Algebraic Development Techniques (WADT’08), LNCS Vol. 5486, pp. 135-151, 2009. 28

  26. Roșu, Grigore, Wolfram Schulte, and Traian Florin Șerbănuță. “Runtime Verification of C Memory Safety.” Runtime Verification (RV’09), LNCS Vol. 5779, pp. 132-151, 2009. 64

  27. Șerbănuță, Traian Florin, Gheorghe Ștefănescu, and Grigore Roșu. “Defining and Executing P Systems with Structured Data in K.” Membrane Computing (WMC’08), LNCS Vol. 5391, pp. 374-393, 2009. 28

  28. Chen, Feng, Traian Florin Șerbănuță, and Grigore Roșu. “jPredictor: a predictive runtime analysis tool for Java.” ICSE ’08: Proceedings of the 30th International Conference on Software Engineering, pp. 221-230, 2008. 155

  29. Ghoshal, Sudipto, Solaiappan Manimaran, Grigore Roșu, Traian Florin Șerbănuță, and Gheorghe Ștefănescu. “Monitoring IVHM Systems using a Monitor-Oriented Programming Framework.” Sixth NASA Langley Formal Methods Workshop (LFM 2008), 2008. 5

  30. Șerbănuță, Traian Florin, Grigore Roșu, and José Meseguer. “A Rewriting Logic Approach to Operational Semantics (Extended Abstract).” Structural Operational Semantics (SOS’07), ENTCS Vol. 192, No. 1, pp. 125-141, 2007.

  31. Hills, Mark, Traian Florin Șerbănuță, and Grigore Roșu. “A Rewrite Framework for Language Definitions and for Generation of Efficient Interpreters.” Rewriting Logic and Its Applications (WRLA’06), ENTCS Vol. 176, No. 4, pp. 215-231, 2007. 31

  32. Denker, Grit, et al. “Rewriting Logic Systems.” Rewriting Logic and Its Applications (WRLA’06), ENTCS Vol. 176, No. 4, 2007. 7

  33. Șerbănuță, Traian Florin and Grigore Roșu. “Computationally Equivalent Elimination of Conditions.” Rewriting Techniques and Applications (RTA’06), LNCS Vol. 4098, pp. 19-34, 2006. 41

  34. Popescu, Andrei, Traian Florin Șerbănuță, and Grigore Roșu. “A Semantic Approach to Interpolation.” Foundations of Software Science and Computation Structures (FoSSaCS’06), LNCS Vol. 3921, pp. 307-321, 2006.

  35. Reitter, David, Ștefan Covaci, Florin Oltean, Cătălin Băcanu, and Traian Florin Șerbănuță. “Hybrid Natural Language Processing in a Customer-Care Environment.” 11th Student Conference on Computational Linguistics (TaCoS’01), 2001. 7

Books, Book Chapters, and Theses

  1. Lucanu, Dorel, Traian-Florin Șerbănuță, and Grigore Roșu. “Towards a Kool Future.” In Theory and Practice of Formal Methods, LNCS, Springer, pp. 325-343, 2016. 1

  2. Șerbănuță, Traian Florin. Programming Language Design and Analysis: A Rewriting Approach. Editura Universității „Alexandru Ioan Cuza”, Iași, 2012. Revised edition of the PhD thesis.

  3. Șerbănuță, Traian Florin. A Rewriting Approach to Concurrent Programming Language Design and Semantics. PhD thesis, University of Illinois at Urbana-Champaign, 2010. 24

  4. Șerbănuță, Traian Florin. Institutional Concepts in First-Order Logic, Parameterized Specifications, and Logic Programming. Master’s dissertation, University of Bucharest, 2004. 5

  5. Șerbănuță, Traian Florin. Ascunderea informației în text folosind gramatici de tip LR(k) (Information Hiding in Text Using LR(k) Grammars). BSc thesis, University of Bucharest, 2002.

Preprints

  1. Șerbănuță, Traian Florin, Jun Xu, Andrei Ștefănescu, and Cosmin Radoi. “Solving VeriContest with a Lean-Backed Rust Verifier.” arXiv:2610.03994, 2026.

  2. Zamfir, Vlad, Mihai Calancea, Denisa Diaconescu, Wojciech Kołowski, Brandon Moore, Karl Palmskog, Traian Florin Șerbănuță, Michael Stay, Dafina Trufaș, and Jan Tušil. “Validating Labelled State Transition and Message Production Systems: A Theory for Modelling Faulty Distributed Systems.” arXiv:2202.12662, 2022. 1

Technical Reports

  1. Arusoaie, Andrei and Traian Florin Șerbănuță. “Contextual Transformation in K Framework.” 2011. 3

  2. Șerbănuță, Traian Florin, Feng Chen, and Grigore Roșu. “Maximal Causal Models for Sequentially Consistent Systems.” University of Illinois, 2011.

  3. Șerbănuță, Traian Florin, Feng Chen, and Grigore Roșu. “Maximal Causal Models for Sequentially Consistent Multithreaded Systems.” University of Illinois, 2010.

  4. Șerbănuță, Traian Florin and Grigore Roșu. “KRAM — Extended Report.” University of Illinois, 2010.

  5. Roșu, Grigore, Wolfram Schulte, and Traian Florin Șerbănuță. “Runtime Verification of C Memory Safety.” UIUCDCS-R-2009-3048, University of Illinois, 2009.

  6. Șerbănuță, Traian Florin, Feng Chen, and Grigore Roșu. “Maximal Causal Models for Multithreaded Systems.” UIUCDCS-R-2008-3017, University of Illinois, 2008.

  7. Ellison, Chucky, Traian Florin Șerbănuță, and Grigore Roșu. “A Rewriting Logic Approach to Type Inference.” UIUCDCS-R-2008-2934, University of Illinois, 2008.

  8. Chen, Feng, Traian Florin Șerbănuță, and Grigore Roșu. “Effective Predictive Runtime Analysis Using Sliced Causality and Atomicity.” UIUCDCS-R-2007-2905, University of Illinois, 2007. 3

  9. Șerbănuță, Traian Florin and Grigore Roșu. “A Rewriting Logic Approach to Operational Semantics.” UIUCDCS-R-2006-2780, University of Illinois, 2006.

  10. Șerbănuță, Traian Florin and Grigore Roșu. “Computationally Equivalent Elimination of Conditions.” UIUCDCS-R-2006-2693, University of Illinois, 2006.

  11. Popescu, Andrei, Traian Florin Șerbănuță, and Grigore Roșu. “A Semantic Approach to Interpolation.” UIUCDCS-R-2005-2643, University of Illinois, 2005.

  12. Șerbănuță, Traian Florin. “Report on an Envelope Invariance Checker Tool for Specifications in PMEL.” 2005.

  13. Șerbănuță, Traian Florin and Grigore Roșu. “Towards Effectively Eliminating Conditional Rewrite Rules.” UIUCDCS-R-2004-2494, University of Illinois, 2004.