Recently, the rise of code-centric Large Language Models (LLMs) has reshaped the software engineering world with low-barrier tools like Copilot that can easily generate code. However, there is no correctness guarantee for the code generated by LLMs, which suffer from the hallucination problem, and their output is fraught with risks. Besides, the end-to-end process from specification to code through LLMs is a non-transparent and uncontrolled black box. This opacity makes it difficult for users to understand and trust the generated code. Addressing these challenges is both necessary and critical. In contrast, program refinement transforms high-level specification statements into executable code while preserving correctness. Traditional tools for program refinement are primarily designed for formal methods experts and lack automation and extensibility. We apply program refinement to guide LLM and validate the LLM-generated code while transforming refinement into a more accessible and flexible framework. To initiate this vision, we propose Refine4LLM, an approach that aims to:(1) Formally refine the specifications, (2) Automatically prompt and guide the LLM using refinement calculus, (3) Interact with the LLM to generate the code, (4) Verify that the generated code satisfies the constraints, thus guaranteeing its correctness, (5) Learn and build more advanced refinement laws to extend the refinement calculus. We evaluated Refine4LLM against the state-of-the-art baselines on program refinement and LLMs benchmarks. The experiment results show that Refine4LLM can efficiently generate more robust code and reduce the time for refinement and verification.

Blockchain technology has been integrated into a wide range of applications in various sectors, such as finance, supply chain, health, and governance. However, the participation of a few actors with malicious intentions challenges law enforcement authorities, regulators and other users. These challenges revolve around dealing with an array of illegal activities such as asset trades in dark markets, receiving payments for cyber-attacks, and facilitating money laundering. Developing an efficient mechanism to identify malicious actors in blockchain networks is a pressing need to build confidence among the stakeholders and ensure regulatory adherence. The raw data of blockchain transactions do not readily reveal the dynamic behavioural changes and their interconnection between transactions and accounts. These behavioural patterns can be useful for identifying malicious actors. Machine Learning (ML)-based models for early warning and/or detection are considered one of the potential approaches. In ML, feature engineering plays a crucial role in enhancing the predictive performance of a model. This study proposes different categories of features and unified feature extraction approaches for raw Bitcoin and Ethereum transaction data and their interconnection information. As far as we are aware, there has been no study that considered a feature engineering approach for identifying malicious activities. The significance of the engineered features was validated against eight classifiers, including Random Forest (RF), XG-boost (XG), Silas, and neural network-based classifiers. The results showed that these features contribute to higher classification accuracy and higher Area Under the Receiver Operating Characteristic Curve (AUC) value for both Bitcoin and Ethereum transactions. This work also analysed the influence of engineered features in classification using the eXplainable Artificial Intelligence (XAI) technique SHapley Additive exPlanations (SHAP) values. The feature importance scores confirmed the significance of the proposed engineered features towards implementing classification models to identify, target and disrupt malicious activities in blockchain networks.

We present a labelled sequent calculus for Boolean bunched implications (BBI), a classical variant of the logic of Bunched Implications (BI). The calculus is simple, sound, complete and enjoys cut-elimination. We show that all the structural rules in the calculus, i.e. those rules that manipulate labels and ternary relations, can be localized around applications of certain logical rules, thereby localizing the handling of these rules in proof search. Based on this, we demonstrate a free variable calculus that deals with the structural rules lazily in a constraint system. We propose a heuristic method to quickly solve certain constraints, and show some experimental results to confirm that our approach is feasible for proof search. Additionally, we show that different semantics for BBI and some axioms in concrete models can be captured modularly simply by adding extra structural rules.