Dorel Lucanu

Dorel Lucanu, Grigore Rosu, Eugen Goriac et al.

The Circularity Principle was successfully applied for developing a coinductive proving technique, known as circular coinduction. In this paper, we show that the same principle can be used to develop an inductive proving technique. A main advantage of this uniform approach is that the two proving techniques can be easily combined during the verification process. Circular induction is simple, flexible, generic, and therefore it is a good candidate framework for combining different proving schemes into a competitive tool. We exhibit this potential by presenting how the circular induction is implemented in CIRC, a prover built around the Circularity Principle. Disclaimer. This paper was written in 2010, at the time the CIRC prover was developed, and the main body reflects the state of the work and of the prover as of that date. For this arXiv technical report, only the related-work discussion (Section 6) and the concluding section have been revised: Section 6 has been extended to situate circular induction within the cyclic-proof and infinite-descent literature that has appeared or matured since 2010. No other part of the paper-its definitions, results, proofs, examples, or implementation description-has been modified, and the technical content should be read as a 2010 contribution. References to developments after 2010 appear only in the updated related-work section.

Stefan-Claudiu Susan, Andrei Arusoaie, Dorel Lucanu

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.

Ş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 can formally or empirically prove the presence of defects. This paper introduces a novel detection pipeline that integrates custom Slither-based detectors, LLMs, Kontrol, and Forge. Our approach is designed to reliably detect defects and generate proofs. We currently perform experiments with promising results for seven types of critical defects. We demonstrate the pipeline's efficacy by presenting our findings for three vulnerabilities -- Reentrancy, Complex Fallback, and Faulty Access Control Policies -- that are challenging for current verification solutions, which often generate false alarms or fail to detect them entirely. We highlight the potential of either symbolic or concrete execution in correctly classifying such code faults. By chaining these instruments, our method effectively validates true positives, significantly reducing the manual verification burden. Although we identify potential limitations, such as the inconsistency and the cost of LLMs, our findings establish a robust framework for combining heuristic analysis with formal verification to achieve more reliable and automated smart contract auditing.