Augmented Reality. - Andrei Arusoaie; Alexandru Ionut Cristei; Cristian Chircu; Mihai Andrei Livadariu; Vlad Manea; Adrian Iftene (SYNASC, 2010)

Towards a K Semantics for OCL. - Andrei Arusoaie; Dorel Lucanu; Vlad Rusu (K, 2011)

The K Primer (version 3.3). - Traian-Florin Serbanuta; Andrei Arusoaie; David Lazar; Chucky Ellison; Dorel Lucanu; Grigore Rosu (K, 2011)

Executing Formal Semantics with the K Tool. - David Lazar; Andrei Arusoaie; Traian-Florin Serbanuta; Chucky Ellison; Radu Mereuta; Dorel Lucanu; Grigore Rosu (FM, 2012)

Automating Abstract Syntax Tree Construction for Context Free Grammars. - Andrei Arusoaie; Daniel Ionut Vicol (SYNASC, 2012)

Making Maude Definitions More Interactive. - Andrei Arusoaie; Traian-Florin Serbanuta; Chucky Ellison; Grigore Rosu (WRLA, 2012)

A Generic Framework for Symbolic Execution. - Andrei Arusoaie; Dorel Lucanu; Vlad Rusu (SLE, 2013)

Engineering Hoare Logic-Based Program Verification in K Framework. - Andrei Arusoaie (SYNASC, 2013)

A Generic Framework for Symbolic Execution:Theory and Applications : Theory and Applications. (Un cadre générique pour exécution symbolique / Un cadre générique pour exécution symbolique : Theorie et Applications). - Andrei Arusoaie (2014)

Verifying Reachability-Logic Properties on Rewriting-Logic Specifications. - Dorel Lucanu; Vlad Rusu; Andrei Arusoaie; David Nowak (Logic, Rewriting, and Concurrency, 2015)

Symbolic execution based on language transformation. - Andrei Arusoaie; Dorel Lucanu; Vlad Rusu (Comput. Lang. Syst. Struct., 2015)

Proving Reachability-Logic Formulas Incrementally. - Vlad Rusu; Andrei Arusoaie (WRLA, 2016)

Language definitions as rewrite theories. - Vlad Rusu; Dorel Lucanu; Traian-Florin Serbanuta; Andrei Arusoaie; Andrei Stefanescu; Grigore Rosu (J. Log. Algebraic Methods Program., 2016)

A Comparison of Open-Source Static Analysis Tools for Vulnerability Detection in C/C++ Code. - Andrei Arusoaie; Stefan Ciobaca; Vlad Craciun; Dragos Gavrilut; Dorel Lucanu (SYNASC, 2017)

A Certified Procedure for RL Verification. - Andrei Arusoaie; David Nowak; Vlad Rusu; Dorel Lucanu (SYNASC, 2017)

Executing and verifying higher-order functional-imperative programs in Maude. - Vlad Rusu; Andrei Arusoaie (J. Log. Algebraic Methods Program., 2017)

A generic framework for symbolic execution: A coinductive approach. - Dorel Lucanu; Vlad Rusu; Andrei Arusoaie (J. Symb. Comput., 2017)

Unification Modulo Builtins. - Stefan Ciobaca; Andrei Arusoaie; Dorel Lucanu (WoLLIC, 2018)

Unification in Matching Logic - Extended Version. - Andrei Arusoaie; Dorel Lucanu (CoRR, 2018)

Unification in Matching Logic. - Andrei Arusoaie; Dorel Lucanu (FM, 2019)

AIM: Designing a language for AI models. - Ionut Cristian Pistol; Andrei Arusoaie (KES, 2019)

Using SMT Solvers to Validate Models for AI Problems. - Andrei Arusoaie; Ionut Pistol (CoRR, 2019)

A Formal Semantics of Findel in Coq (Short Paper). - Andrei Arusoaie (CoRR, 2019)

DApp for Rating. - Andreea Buterchi; Andrei Arusoaie (CoRR, 2020)

Decentralized Application for Rating Internet Resources. - Andreea Buterchi; Andrei Arusoaie (ICSOFT, 2021)

Analysing State-based Models for AI Problems. - Ionut Cristian Pistol; Andrei Arusoaie (KES, 2021)

Certifying Findel derivatives for blockchain. - Andrei Arusoaie (J. Log. Algebraic Methods Program., 2021)

Proof-Carrying Parameters in Certified Symbolic Execution: The Case Study of Antiunification. - Andrei Arusoaie; Dorel Lucanu (FROM, 2022)

AIM-RL: A New Framework Supporting Reinforcement Learning Experiments. - Ionut Cristian Pistol; Andrei Arusoaie (ICSOFT, 2023)

Identifying Vulnerabilities in Smart Contracts using Interval Analysis. - Stefan-Claudiu Susan; Andrei Arusoaie (FROM, 2023)

Proof-carrying parameters in certified symbolic execution. - Andrei Arusoaie; Dorel Lucanu (Log. J. IGPL, 2024)

Towards Trusted Smart Contracts: A Comprehensive Test Suite For Vulnerability Detection. - Andrei Arusoaie; Stefan-Claudiu Susan (Empir. Softw. Eng., 2024)

Towards Stream-Based Monitoring for EVM Networks. - Emanuel Onica; Claudiu-Nicu Barbieru; Andrei Arusoaie; Oana-Otilia Captarencu; Ciprian Amariei (DEBS, 2025)