-
Micro-Patterns in Solidity Code
Authors:
Luca Ruschioni,
Robert Shuttleworth,
Rumyana Neykova,
Barbara Re,
Giuseppe Destefanis
Abstract:
Solidity is the predominant programming language for blockchain-based smart contracts, and its characteristics pose significant challenges for code analysis and maintenance. Traditional software analysis approaches, while effective for conventional programming languages, often fail to address Solidity-specific features such as gas optimization and security constraints.
This paper introduces micr…
▽ More
Solidity is the predominant programming language for blockchain-based smart contracts, and its characteristics pose significant challenges for code analysis and maintenance. Traditional software analysis approaches, while effective for conventional programming languages, often fail to address Solidity-specific features such as gas optimization and security constraints.
This paper introduces micro-patterns - recurring, small-scale design structures that capture key behavioral and structural peculiarities specific to a language - for Solidity language and demonstrates their value in understanding smart contract development practices. We identified 18 distinct micro-patterns organized in five categories (Security, Functional, Optimization, Interaction, and Feedback), detailing their characteristics to enable automated detection.
To validate this proposal, we analyzed a dataset of 23258 smart contracts from five popular blockchains (Ethereum, Polygon, Arbitrum, Fantom and Optimism). Our analysis reveals widespread adoption of micro-patterns, with 99% of contracts implementing at least one pattern and an average of 2.76 patterns per contract. The Storage Saver pattern showed the highest adoption (84.62% mean coverage), while security patterns demonstrated platform-specific adoption rates. Statistical analysis revealed significant platform-specific differences in pattern adoption, particularly in Borrower, Implementer, and Storage Optimization patterns.
△ Less
Submitted 2 May, 2025;
originally announced May 2025.
-
Reaching Classicality through Transitive Closure
Authors:
Quentin Blomet,
Bruno Da Ré
Abstract:
Recently, arXiv:2312.16035 showed that all logics based on Boolean Normal monotonic three-valued schemes coincide with classical logic when defined using a strict-tolerant standard ($\mathbf{st}$). Conversely, they proved that under a tolerant-strict standard ($\mathbf{ts}$), the resulting logics are all empty. Building on these results, we show that classical logic can be obtained by closing unde…
▽ More
Recently, arXiv:2312.16035 showed that all logics based on Boolean Normal monotonic three-valued schemes coincide with classical logic when defined using a strict-tolerant standard ($\mathbf{st}$). Conversely, they proved that under a tolerant-strict standard ($\mathbf{ts}$), the resulting logics are all empty. Building on these results, we show that classical logic can be obtained by closing under transitivity the union of two logics defined over (potentially different) Boolean normal monotonic schemes, using a strict-strict standard ($\mathbf{ss}$) for one and a tolerant-tolerant standard ($\mathbf{tt}$) for the other, with the first of these logics being paracomplete and the other being paraconsistent. We then identify a notion dual to transitivity that allows us to characterize the logic $\mathsf{TS}$ as the dual transitive closure of the intersection of any two logics defined over (potentially different) Boolean normal monotonic schemes, using an $\mathbf{ss}$ standard for one and a $\mathbf{tt}$ standard for the other. Finally, we expand on the abstract relations between the transitive closure and dual transitive closure operations, showing that they give rise to lattice operations that precisely capture how the logics discussed relate to one another.
△ Less
Submitted 28 March, 2025;
originally announced March 2025.
-
An Explicit Primitive Conservative Solver for the Euler Equations with Arbitrary Equation of State
Authors:
Giuseppe Sirianni,
Alberto Guardone,
Barbara Re,
Rémi Abgrall
Abstract:
This work presents a procedure to solve the Euler equations by explicitly updating, in a conservative manner, a generic thermodynamic variable such as temperature, pressure or entropy instead of the total energy. The presented procedure is valid for any equation of state and spatial discretization. When using complex equations of state such as Span-Wagner, choosing the temperature as the generic t…
▽ More
This work presents a procedure to solve the Euler equations by explicitly updating, in a conservative manner, a generic thermodynamic variable such as temperature, pressure or entropy instead of the total energy. The presented procedure is valid for any equation of state and spatial discretization. When using complex equations of state such as Span-Wagner, choosing the temperature as the generic thermodynamic variable yields great reductions in the computational costs associated to thermodynamic evaluations. Results computed with a state of the art thermodynamic model are presented, and computational times are analyzed. Particular attention is dedicated to the conservation of total energy, the propagation speed of shock waves and jump conditions. The procedure is thoroughly tested using the Span-Wagner equation of state through the CoolProp thermodynamic library and the Van der Waals equation of state, both in the ideal and non-ideal compressible fluid-dynamics regimes, by comparing it to the standard total energy update and analytical solutions where available.
△ Less
Submitted 21 June, 2024; v1 submitted 11 April, 2024;
originally announced April 2024.
-
On three-valued presentations of classical logic
Authors:
Bruno da Ré,
Damian Szmuc,
Emmanuel Chemla,
Paul Égré
Abstract:
Given a three-valued definition of validity, which choice of three-valued truth tables for the connectives can ensure that the resulting logic coincides exactly with classical logic? We give an answer to this question for the five monotonic consequence relations $st$, $ss$, $tt$, $ss\cap tt$, and $ts$, when the connectives are negation, conjunction, and disjunction. For $ts$ and $ss\cap tt$ the an…
▽ More
Given a three-valued definition of validity, which choice of three-valued truth tables for the connectives can ensure that the resulting logic coincides exactly with classical logic? We give an answer to this question for the five monotonic consequence relations $st$, $ss$, $tt$, $ss\cap tt$, and $ts$, when the connectives are negation, conjunction, and disjunction. For $ts$ and $ss\cap tt$ the answer is trivial (no scheme works), and for $ss$ and $tt$ it is straightforward (they are the collapsible schemes, in which the middle value acts like one of the classical values). For $st$, the schemes in question are the Boolean normal schemes that are either monotonic or collapsible.
△ Less
Submitted 26 December, 2023;
originally announced December 2023.
-
An ALE residual distribution scheme for the unsteady Euler equations over triangular grids with local mesh adaptation
Authors:
Stefano Colombo,
Barbara Re
Abstract:
This work presents a novel interpolation-free mesh adaptation technique for the Euler equations within the arbitrary Lagrangian Eulerian framework. For the spatial discretization, we consider a residual distribution scheme, which provides a pretty simple way to achieve high order accuracy on unstructured grids. Thanks to a special interpretation of the mesh connectivity changes as a series of fict…
▽ More
This work presents a novel interpolation-free mesh adaptation technique for the Euler equations within the arbitrary Lagrangian Eulerian framework. For the spatial discretization, we consider a residual distribution scheme, which provides a pretty simple way to achieve high order accuracy on unstructured grids. Thanks to a special interpretation of the mesh connectivity changes as a series of fictitious continuous deformations, we can enforce by construction the so-called geometric conservation law, which helps to avoid spurious oscillations while solving the governing equations over dynamic domains. This strategy preserves the numerical properties of the underlying, fixed-connectivity scheme, such as conservativeness and stability, as it avoids an explicit interpolation of the solution between different grids. The proposed approach is validated through the two-dimensional simulations of steady and unsteady flow problems over unstructured grids.
△ Less
Submitted 25 April, 2022;
originally announced April 2022.
-
A pressure-based method for weakly compressible two-phase flows under a Baer-Nunziato type model with generic equations of state and pressure and velocity disequilibrium
Authors:
Barbara Re,
Rémi Abgrall
Abstract:
Within the framework of diffuse interface methods, we derive a pressure-based Baer-Nunziato type model well-suited to weakly compressible multiphase flows. The model can easily deal with different equation of states and it includes relaxation terms characterized by user-defined finite parameters, which drive the pressure and velocity of each phase toward the equilibrium. There is no clear notion o…
▽ More
Within the framework of diffuse interface methods, we derive a pressure-based Baer-Nunziato type model well-suited to weakly compressible multiphase flows. The model can easily deal with different equation of states and it includes relaxation terms characterized by user-defined finite parameters, which drive the pressure and velocity of each phase toward the equilibrium. There is no clear notion of speed of sound, and thus, most of the classical low Mach approximation cannot easily be cast in this context. The proposed solution strategy consists of two operators: a semi-implicit finite-volume solver for the hyperbolic part and an ODE integrator for the relaxation processes. Being the acoustic terms in the hyperbolic part integrated implicitly, the stability condition on the time step is lessened. The discretization of non-conservative terms involving the gradient of the volume fraction fulfills by construction the non-disturbance condition on pressure and velocity to avoid oscillations across the multimaterial interfaces. The developed simulation tool is validated through one-dimensional simulations of shock-tube and Riemann-problems, involving water-aluminum and water-air mixtures, vapor-liquid mixture of water and of carbon dioxide, and almost pure flows. The numerical results match analytical and reference ones, except some expected discrepancies across shocks, which however remain acceptable (errors within some percentage points). All tests were performed with acoustic CFL numbers greater than one, and no stability issues arose, even for CFL greater than 10. The effects of different values of relaxation parameters and of different amount equations of state -- stiffened gas and Peng-Robinson -- were investigated.
△ Less
Submitted 23 May, 2022; v1 submitted 26 July, 2021;
originally announced July 2021.
-
On the simulation of multicomponent and multiphase compressible flows
Authors:
Rémi Abgrall,
Paola Bacigaluppi,
Barbara Re
Abstract:
The following paper presents two simulation strategies for compressible two-phase or multicomponent flows. One is a full non-equilibrium model in which the pressure and velocity are driven towards the equilibrium at interfaces by numerical relaxation processes, the second is a four-equation model that assumes stiff mechanical and thermal equilibrium between phases or components. In both approaches…
▽ More
The following paper presents two simulation strategies for compressible two-phase or multicomponent flows. One is a full non-equilibrium model in which the pressure and velocity are driven towards the equilibrium at interfaces by numerical relaxation processes, the second is a four-equation model that assumes stiff mechanical and thermal equilibrium between phases or components. In both approaches, the thermodynamic behaviour of each fluid is modelled independently according to the stiffened-gas equations of state. The presented methods are used to simulate the de-pressurization of a pipe containing pure CO$_2$ liquid and vapour under the one-dimensional approximation.
△ Less
Submitted 12 August, 2021; v1 submitted 2 June, 2020;
originally announced June 2020.
-
Collaboration vs. choreography conformance in BPMN
Authors:
Flavio Corradini,
Andrea Morichetta,
Andrea Polini,
Barbara Re,
Francesco Tiezzi
Abstract:
The BPMN 2.0 standard is a widely used semi-formal notation to model distributed information systems from different perspectives. The standard makes available a set of diagrams to represent such perspectives. Choreography diagrams represent global constraints concerning the interactions among system components without exposing their internal structure. Collaboration diagrams instead permit to depi…
▽ More
The BPMN 2.0 standard is a widely used semi-formal notation to model distributed information systems from different perspectives. The standard makes available a set of diagrams to represent such perspectives. Choreography diagrams represent global constraints concerning the interactions among system components without exposing their internal structure. Collaboration diagrams instead permit to depict the internal behaviour of a component, also referred as process, when integrated with others so to represent a possible implementation of the distributed system.
This paper proposes a design methodology and a formal framework for checking conformance of choreographies against collaborations. In particular, the paper presents a direct formal operational semantics for both BPMN choreography and collaboration diagrams. Conformance aspects are proposed through two relations defined on top of the defined semantics. The approach benefits from the availability of a tool we have developed, named C4, that permits to experiment the theoretical framework in practical contexts. The objective here is to make the exploited formal methods transparent to system designers, thus fostering a wider adoption by practitioners.
△ Less
Submitted 26 October, 2020; v1 submitted 6 February, 2020;
originally announced February 2020.
-
Non-equilibrium Model for Weakly Compressible Multi-component Flows: the Hyperbolic Operator
Authors:
Barbara Re,
Rémi Abgrall
Abstract:
We present a novel pressure-based method for weakly compressible multiphase flows, based on a non-equilibrium Baer and Nunziato-type model. In this work, we describe the hyperbolic operator, thus we do not consider relaxation terms. The acoustic part of the governing equations is treated implicitly to avoid the severe restriction on the time step imposed by the CFL condition at low-Mach. Particula…
▽ More
We present a novel pressure-based method for weakly compressible multiphase flows, based on a non-equilibrium Baer and Nunziato-type model. In this work, we describe the hyperbolic operator, thus we do not consider relaxation terms. The acoustic part of the governing equations is treated implicitly to avoid the severe restriction on the time step imposed by the CFL condition at low-Mach. Particular care is taken to discretize the non-conservative terms to avoid spurious oscillations across multi-material interfaces. The absence of oscillations and the agreement with analytical or published solutions is demonstrated in simplified test cases, which confirm the validity of the proposed approach as a building block on which developing more accurate and comprehensive methods.
△ Less
Submitted 1 November, 2019;
originally announced November 2019.
-
An Adaptive ALE Scheme for Non-Ideal Compressible-Fluid Dynamics over Dynamic Unstructured Meshes
Authors:
Barbara Re,
Alberto Guardone
Abstract:
This paper investigates the application of mesh adaptation techniques in the Non-Ideal Compressible Fluid Dynamic (NICFD) regime, a region near the vapor-liquid saturation curve where the flow behavior significantly departs from the ideal gas model, as indicated by a value of the fundamental derivative of gasdynamics less than one. A recent interpolation-free finite-volume adaptive scheme is explo…
▽ More
This paper investigates the application of mesh adaptation techniques in the Non-Ideal Compressible Fluid Dynamic (NICFD) regime, a region near the vapor-liquid saturation curve where the flow behavior significantly departs from the ideal gas model, as indicated by a value of the fundamental derivative of gasdynamics less than one. A recent interpolation-free finite-volume adaptive scheme is exploited to modify the grid connectivity in a conservative way, and the governing equations for compressible inviscid flows are solved within the Arbitrary Lagrangian Eulerian framework by including special fictitious fluxes representing volume modifications due to mesh adaptation.The absence of interpolation of the solution to the new grid prevents spurious oscillations that may make the solution of the flow field in the NICFD regime more difficult and less robust.Non-ideal gas effects are taken into account by adopting the polytropic Peng-Robinson thermodynamic model. The numerical results focus on the problem of a piston moving in a tube filled with siloxane $\mathrm{MD_4M}$, a simple configuration which can be the core of experimental research activities aiming at investigating the thermodynamic behavior of NICFD flows. Several numerical tests involving different piston movements and initial states in 2D and 3D assess the capability of the proposed adaption technique to correctly capture compression and expansion waves, as well as the generation and propagation of shock waves, in the NICFD and in the non-classical regime.
△ Less
Submitted 9 August, 2019;
originally announced August 2019.
-
A Classification of BPMN Collaborations based on Safeness and Soundness Notions
Authors:
Flavio Corradini,
Chiara Muzi,
Barbara Re,
Francesco Tiezzi
Abstract:
BPMN 2.0 standard has a huge uptake in modelling business processes within the same organisation or collaborations involving multiple interacting participants. It results that providing a solid foundation to enable BPMN designers to understand their models in a consistent way is becoming more and more important. In our investigation we define and exploit a formal characterisation of the collaborat…
▽ More
BPMN 2.0 standard has a huge uptake in modelling business processes within the same organisation or collaborations involving multiple interacting participants. It results that providing a solid foundation to enable BPMN designers to understand their models in a consistent way is becoming more and more important. In our investigation we define and exploit a formal characterisation of the collaborations' semantics, specifically and directly given for BPMN models, to provide a classification of BPMN collaborations. In particular, we refer to collaborations involving processes with arbitrary topology, thus overcoming the well-structuredness limitations. The proposed classification is based on some of the most important correctness properties in the business process domain, namely safeness and soundness. We prove, with a uniform formal framework, some conjectured and expected results and, most of all, we achieve novel results for BPMN collaborations concerning the relationships between safeness and soundness, and their compositionality, that represent major advances in the state-of-the-art.
△ Less
Submitted 26 August, 2018;
originally announced September 2018.
