Researcher profile

Dorel Lucanu

Dorel Lucanu contributes to research discovery and scholarly infrastructure.

ResearcherAffiliation not importedOpen to collaborate

Trust snapshot

Quick read

Trust 13 - UnverifiedVerification L1Unclaimed author
2works
0followers
4topics
4close collaborators

Actions

Decide how to stay connected

Follow researcher0

Identity and collaboration

How to connect with this researcher

Claiming links this public author record to a researcher profile and unlocks direct collaboration workflows.

Log in to claim

Direct collaboration

Open a focused conversation when the fit is right

Claim this author entity first to unlock direct invitations.

Research graph

See the researcher in context

Open full explorer

Inspect adjacent work, topics, institutions and collaborators without jumping out to a separate graph page.

Building this graph slice

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

2 published item(s)

preprint2026arXiv

Benchmarking LLM-Based Static Analysis for Secure Smart Contract Development: Reliability, Limitations, and Potential Hybrid Solutions

The irreversible nature of blockchain transactions makes the identification of smart contract vulnerabilities an essential requirement for secure system development. While Large Language Models (LLMs) are increasingly integrated into developer workflows, their reliability as autonomous security auditors remains unproven. We assess whether current generative models are a viable replacement for, or only a complement to, traditional static-analysis tools. Our findings indicate that LLM efficacy is undermined by both inherent lexical bias and a lack of rigorous validation of external data inputs. This reliance on non-semantic heuristics, such as identifier naming, leads to a high frequency of false positives. Furthermore, prompting techniques reveal a trade-off between precision and recall. These results were derived using our custom automated framework, which achieves 92% accuracy in classifying model outputs.

preprint2020arXiv

Operationally-based Program Equivalence Proofs using LCTRSs

We propose an operationally-based deductive proof method for program equivalence. It is based on encoding the language semantics as logically constrained term rewriting systems (LCTRSs) and the two programs as terms. The main feature of our method is its flexibility. We illustrate this flexibility in two applications, which are novel. For the first application, we show how to encode low-level details such as stack size in the language semantics and how to prove equivalence between two programs operating at different levels of abstraction. For our running example, we show how our method can prove equivalence between a recursive function operating with an unbounded stack and its tail-recursive optimized version operating with a bounded stack. This type of equivalence checking can be used to ensure that new, undesirable behavior is not introduced by a more concrete level of abstraction. For the second application, we show how to formalize read-sets and write-sets of symbolic expressions and statements by extending the operational semantics in a conservative way. This enables the relational verification of program schemas, which we exploit to prove correctness of compiler optimizations, some of which cannot be proven by existing tools. Our method requires an extension of standard LCTRSs with axiomatized symbols. We also present a prototype implementation that proves the feasibility of both applications that we propose.