Blockchain technology has attracted more and more attention from academia and industry recently. Ethereum, which uses blockchain technology, is a distributed computing platform and operating system. Smart contracts are small programs deployed to the Ethereum blockchain for execution. Errors in smart contracts will lead to huge losses. Formal verification can provide a reliable guarantee for the security of blockchain smart contracts. In this paper, the formal method is applied to inspect the security issues of smart contracts. We summarize five kinds of security issues in smart contracts and present formal verification methods for these issues, thus establishing a formal verification framework that can effectively verify the security vulnerabilities of smart contracts. Furthermore, we present a complete formal verification of the Binance Coin (BNB) contract. It shows how to formally verify the above security issues based on the formal verification framework in a specific smart contract. All the proofs are checked formally using the Coq proof assistant in which contract model and specification are formalized. The formal work of this paper has a variety of essential applications, such as the verification of blockchain smart contracts, program verification, and the formal establishment of mathematical and computer theoretical foundations.

A two-stage algorithm is proposed to compute switching angles for selective harmonic elimination or selective harmonic control. In the first off-line computing stage, the multivariate nonlinear equations are equivalently converted to a group of univariate linear equations by using the theories of symmetric polynomials and Groebner bases, which are then stored into the target microcontrollers (MCUs) and solved on-line; In the second on-line computing stage, the linear equations are solved and their solutions are used to construct a polynomial whose real roots are actually the final solutions, then, an algebraic-numerical hybrid method is developed to solve the constructed polynomial, which uses the Sturm's theorem to bracket each real root into an individual interval and then the bisection method is used to find all the exact real roots. Compared to the traditional numerical methods, the executing efficiency is increased siginificantly. This method is implemented on several commonly-used MCUs and shows very good real-time performance. Experiments verify the correctness of the solved switching angles and demonstrate the feasibility of applying this method in the real control system.

Selective harmonic elimination pulsewidth modulation (SHEPWM) is an effective way to eliminate low-order harmonics in high-power applications. However, one of the biggest challenges of SHEPWM is to solve the selective harmonic elimination (SHE) equations, which are composed of some nonlinear transcendental equations. Over the past few decades, algebraic algorithms have shown a considerable ability to solve SHE equations, specifically for obtaining all exact solutions. Much research has been published about algebraic algorithms, struggling to solve more switching angles, solving different mathematic models of SHEPWM, and so on. This article comprehensively reviews existing algebraic algorithms, including elementary symmetric polynomials, power sums, Newton's identities, resultant elimination method, Wu's method, Gröbner-basis-based method, Chudnovsky algorithm, polynomial homotopy continuation algorithm, and real-time implementation by algebraic algorithms. The principle operation of these methods is summarized, and their performance is analyzed in terms of execution time, solving ability, and applicability for different mathematical models.

Algebraic algorithms are powerful methods in solving the selective harmonic elimination (SHE) problem, which can find all exact solutions without the requirements of choosing initial values. However, the huge computational burden and long solving time limit the solving capability of algebraic algorithms. This article presents a novel Newton’s identifies-based method to simplify the SHE equations including the order reduction and the variable elimination, thereby reducing the computational burden and the solving time of algebraic algorithms or in other words improving the solving capability of the algebraic algorithms. Compared with existing simplification methods, the proposed method significantly improves the efficiency of solving SHE equations. With the proposed method, the degree of reduction is no longer the bottleneck of solving the SHE equations by using algebraic algorithms. By using the proposed method, the SHE equations with ten switching angles are completely solved with the algebraic algorithm for the first time. The simulation and experimental results indicate that the proposed method is effective and correct.

In order to explore the minimum switching frequency required to regulate certain amount of harmonic components, a novel switching frequency minimized harmonic mitigation (SFMHM) model is proposed in this article, which can regulate $ {N}\mathbf{-1}$ harmonics with far less than N switching angles. By flexibly adjusting the threshold values, the proposed model can achieve both harmonic elimination and mitigation objectives. Based on pulsewidth modulation (PWM) discretization and supported by quadratic programming, the switching frequency in the proposed model is expressed as a quadratic objective function of the PWM waveform. The objectives as fundamental control and selected harmonic mitigations are realized by treating the numerical approximations of the Fourier coefficients as constraints, which are finally transformed into an optimization model with binary variables and can be easily solved by some optimization toolboxes, such as YALMIP. Some computing results show that, compared with the conventional selective harmonic elimination/mitigation (SHE/SHM) methods, the number of switching angles required to mitigate the same number of harmonics under the proposed method has been significantly reduced. The switching frequency can be reduced a lot compared with the conventional SHE/SHM methods, e.g., by 40% for some modulation indexes. Simulations and experiments verify the correctness of proposed SFMHM model.

Formal verification technology has been widely applied in the fields of mathematics and computer science. The formalization of fundamental mathematical theories is particularly essential. Axiomatic set theory is a foundational system of mathematics and has important applications in computer science. Most of the basic concepts and theories in computer science are described and demonstrated in terms of set theory. In this paper, we present a formal system of axiomatic set theory based on the Coq proof assistant. The axiomatic system used in the formal system refers to Morse-Kelley set theory which is a relatively complete and concise axiomatic set theory. In this formal system, we complete the formalization of the basic definitions of sets, functions, ordinal numbers, and cardinal numbers and prove the most commonly used theorems in Coq. Moreover, the non-negative integers are defined, and Peano's postulates are proved as theorems. According to the axiom of choice, we also present formal proofs of the Hausdorff maximal principle and Schröeder-Bernstein theorem. The whole formalization of the system includes eight axioms, one axiom schema, 62 definitions, and 148 corollaries or theorems. The “axiomatic set theory” formal system is free from the more apparent paradoxes, and a complete axiomatic system is constructed through it. It is designed to give a foundation for mathematics quickly and naturally. On the basis of the system, we can prove many famous mathematical theorems and quickly formalize the theories of topology, modern algebra, data structure, database, artificial intelligence, and so on. It will become an essential theoretical basis for mathematics, computer science, philosophy, and other disciplines.