3 citations · 6 across the 7 of their papers we have counts for
8 papers
Validating Solidity Code Defects using Symbolic and Concrete Execution powered by Large Language Models
Ştefan-Claudiu Susan, Andrei Arusoaie, Dorel Lucanu
The high rate of false alarms from static analysis tools and Large Language Models (LLMs) complicates vulnerability detection in Solidity Smart Contracts, demanding methods that ca…
Proceedings 9th edition of Working Formal Methods Symposium
Andrei Arusoaie, Horaţiu Cheval, Radu Iosif
This volume contains the proceedings of the 9th Working Formal Methods Symposium, which was held at the Alexandru Ioan Cuza University, Iaşi, Romania on September 17-19, 2025.
Proof-Carrying Parameters in Certified Symbolic Execution: The Case Study of Antiunification
Andrei Arusoaie, Dorel Lucanu
Symbolic execution uses various algorithms (matching, (anti)unification), whose executions are parameters for proof object generation. This paper proposes a generic method for gene…
DApp for Rating
Andreea Buterchi, Andrei Arusoaie
Lots of existing web applications include a component for rating internet resources (e.g., social media platforms include mechanisms for rating videos or posts). Based on the obtai…
Certifying Findel Derivatives for Blockchain
Andrei Arusoaie
Derivatives are a special type of financial contracts used to hedge risks or to speculate on the market fluctuations. In order to avoid ambiguities and misinterpretations, several…
A Formal Semantics of Findel in Coq (Short Paper)
Andrei Arusoaie
We present the first formal semantics of Findel - a DSL for specifying financial derivatives. The semantics is encoded in Coq, and we use it to prove properties of several Findel c…
Using SMT Solvers to Validate Models for AI Problems
Andrei Arusoaie, Ionut Pistol
Artificial Intelligence problems, ranging form planning/scheduling up to game control, include an essential crucial step: describing a model which accurately defines the problem's…
Unification in Matching Logic - Extended Version
Andrei Arusoaie, Dorel Lucanu
Matching Logic is a framework for specifying programming language semantics and reasoning about programs. Its formulas are called patterns and are built with variables, symbols, co…