An official website of the United States government
Automated deductive program synthesis promises to generate executable programs from concise specifications, along with proofs of correctness that can be independently verified using third-party tools. However, an attempt to exercise this promise using existing proof-certification frameworks reveals significant discrepancies in how proof derivations are structured for two different purposes: program synthesis and program verification. These discrepancies make it difficult to use certified verifiers to validate synthesis results, forcing one to write an ad-hoc translation procedure from synthesis proofs to correctness proofs for each verification backend. In this work, we address this challenge in the context of the synthesis and verification of heap-manipulating programs. We present a technique for principled translation of deductive synthesis derivations (a.k.a. source proofs) into deductive target proofs about the synthesised programs in the logics of interactive program verifiers. We showcase our technique by implementing three different certifiers for programs generated via SuSLik, a Separation Logic-based tool for automated synthesis of programs with pointers, in foundational verification frameworks embedded in Coq: Hoare Type Theory (HTT), Iris, and Verified Software Toolchain (VST), producing concise and efficient machine-checkable proofs for characteristic synthesis benchmarks.
more »
« less
Introducing a Concise Formulation of the Jacobian Matrix for Newton-Raphson Power Flow Solution in the Engineering Curriculum
The power flow computer program is fundamentally important for power system analysis and design. Many textbooks teach the Newton-Raphson method of power flow solution. The typical formulation of the Jacobian matrix in the NR method is cumbersome, inelegant, and laborious to program. Recent papers have introduced a method for calculating the Jacobian matrix that is concise, elegant, and simple to program. The concise formulation of the Jacobian matrix makes writing a power flow program more accessible to students. However, its derivation in the research literature involves advanced manipulations using higher dimensional derivatives, which are challenging for dual level students. This paper presents alternative derivations of the concise formulation that are suitable for undergraduate students, where some cases can be presented in lecture while other cases are assigned as exercises. These derivations have been successfully taught in a dual level course on computational methods for power systems for about ten years.
more »
« less
- Award ID(s):
- 1711521
- PAR ID:
- 10253587
- Date Published:
- Journal Name:
- 2021 IEEE Power and Energy Conference at Illinois (PECI)
- Page Range / eLocation ID:
- 1 to 8
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
Optimal Transmission Switching (OTS) problems minimize operational costs while treating both the transmission line energization statuses and generator setpoints as decision variables. The combination of nonlinearities from an AC power flow model and discrete variables associated with line statuses makes AC-OTS a computationally challenging Mixed-Integer Nonlinear Program (MINLP). To address these challenges, the DC power flow approximation is often used to obtain a DC-OTS formulation expressed as a Mixed-Integer Linear Program (MILP). However, this approximation often leads to suboptimal or infeasible switching decisions when evaluated with an AC power flow model. This paper proposes an enhanced DC-OTS formulation that leverages techniques for training machine learning models to optimize the DC power flow model's parameters. By optimally selecting parameter values that align flows in the DC power flow model with apparent power flows—incorporating both real and reactive components—from AC Optimal Power Flow (OPF) solutions, our method more accurately captures line congestion behavior. Integrating these optimized parameters into the DC-OTS formulation significantly improves the accuracy of switching decisions and reduces discrepancies between DC-OTS and AC-OTS solutions. We compare our optimized DC-OTS model against traditional OTS approaches, including DC-OTS, Linear Programming AC (LPAC)-OTS, and Quadratic Convex (QC)-OTS. Numeric results show that switching decisions from our model yield better performance when evaluated using an AC power flow model, with up to 44% cost reductions in some cases.more » « less
-
Symbol-level precoding (SLP) based on the concept of constructive interference (CI) is shown to be superior to traditional block-level precoding (BLP), however at the cost of a symbol-by-symbol optimization during the precoding design. In this paper, we propose a CI-based block-level precoding (CI-BLP) scheme for the downlink transmission of a multi-user multiple-input single-output (MU-MISO) communication system, where we design a constant precoding matrix to a block of symbol slots to exploit CI for each symbol slot simultaneously. A single optimization problem is formulated to maximize the minimum CI effect over the entire block, thus reducing the computational cost of traditional SLP as the optimization problem only needs to be solved once per block. By leveraging the Karush-Kuhn-Tucker (KKT) conditions and the dual problem formulation, the original optimization problem is finally shown to be equivalent to a quadratic programming (QP) over a simplex. Numerical results validate our derivations and exhibit superior performance for the proposed CI-BLP scheme over traditional BLP and SLP methods, thanks to the relaxed block-level power constraint.more » « less
-
Power engineers rely on computer-based simulation tools to assess grid performance and ensure security. At the core of these tools are solvers for sparse linear equations. When transformed into a bordered block-diagonal (BBD) structure, part of the sparse linear equation solving can be parallelized. This work focuses on using the Schur-complement-based method for LU factorization on BBD matrices, specifically, Jacobian matrices from large-scale systems. Our findings show that the natural ordering method outperforms the default ordering method in computational performance for each block of the BBD matrix. This observation is validated using synthetic 25k-bus and 70k-bus cases, showing a speedup of up to 38% when using natural ordering without permutation. Additionally, the impact of the number of partitions is studied, and the result shows that computational performance improves with more, smaller partitions in the BBD matrices.more » « less
-
This paper presents a new method for enhancing Alternating Current Power Flow (ACPF) analysis. The method integrates the Newton-Raphson (NR) method with Enhanced Gradient Descent (GD) and computational graphs. The integration of renewable energy sources in power systems introduces variability and unpredictability, and this method addresses these challenges. It leverages the robustness of NR for accurate approximations and the flexibility of GD for handling variable conditions, all without requiring Jacobian matrix inversion. Furthermore, computational graphs provide a structured and visual framework that simplifies and systematizes the application of these methods. The goal of this fusion is to overcome the limitations of traditional ACPF methods and improve the resilience, adaptability, and efficiency of modern power grid analyses. We validate the effectiveness of our advanced algorithm through comprehensive testing on established IEEE benchmark systems. Our findings demonstrate that our approach not only speeds up the convergence process but also ensures consistent performance across diverse system states, representing a significant advancement in power flow computation.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Conference Paper:
- https://doi.org/10.1109/PECI51586.2021.9435220
