We derive a formula for the adjoint $overline{A}$ of a square-matrix operation of the form $C=f(A)$, where $f$ is holomorphic in the neighborhood of each eigenvalue. We then apply the formula to derive closed-form expressions in particular cases of i
nterest such as the case when we have a spectral decomposition $A=UDU^{-1}$, the spectrum cut-off $C=A_+$ and the Nearest Correlation Matrix routine. Finally, we explain how to simplify the computation of adjoints for regularized linear regression coefficients.
CHC-COMP-21 is the fourth competition of solvers for Constrained Horn Clauses. In this year, 7 solvers participated at the competition, and were evaluated in 7 separate tracks on problems in linear integer arithmetic, linear real arithmetic, arrays,
and algebraic data-types. The competition was run in March 2021 using the StarExec computing cluster. This report gives an overview of the competition design, explains the organisation of the competition, and presents the competition results.
We consider requirements for cyber-physical systems represented in constrained natural language. We present novel automated techniques for aiding in the development of these requirements so that they are consistent and can withstand perceived failure
s. We show how cyber-physical systems requirements can be modeled using the event calculus (EC), a formalism used in AI for representing actions and change. We also show how answer set programming (ASP) and its query-driven implementation s(CASP) can be used to directly realize the event calculus model of the requirements. This event calculus model can be used to automatically validate the requirements. Since ASP is an expressive knowledge representation language, it can also be used to represent contextual knowledge about cyber-physical systems, which, in turn, can be used to find gaps in their requirements specifications. We illustrate our approach through an altitude alerting system from the avionics domain.
Jacobis results on the computation of the order and of the normal forms of a differential system are translated in the formalism of differential algebra. In the quasi-regular case, we give complete proofs according to Jacobis arguments. The main resu
lt is {it Jacobis bound}, still conjectural in the general case: the order of a differential system $P_{1}, ldots, P_{n}$ is not greater than the maximum $cO$ of the sums $sum_{i=1}^{n} a_{i,sigma(i)}$, for all permutations $sigma$ of the indices, where $a_{i,j}:={rm ord}_{x_{j}}P_{i}$, emph{viz.} the emph{tropical determinant of the matrix $(a_{i,j})$}. The order is precisely equal to $cO$ iff Jacobis emph{truncated determinant} does not vanish. Jacobi also gave a polynomial time algorithm to compute $cO$, similar to Kuhns index{Hungarian method}``Hungarian method and some variants of shortest path algorithms, related to the computation of integers $ell_{i}$ such that a normal form may be obtained, in the generic case, by differentiating $ell_{i}$ times equation $P_{i}$. Fundamental results about changes of orderings and the various normal forms a system may have, including differential resolvents, are also provided.
In this note, I develop my personal view on the scope and relevance of symbolic computation in software science. For this, I discuss the interaction and differences between symbolic computation, software science, automatic programming, mathematical k
nowledge management, artificial intelligence, algorithmic intelligence, numerical computation, and machine learning. In the discussion of these notions, I allow myself to refer also to papers (1982, 1985, 2001, 2003, 2013) of mine in which I expressed my views on these areas at early stages of some of these fields.
Let $M=(m_{ij})$ be a symmetric matrix of order $n$ whose elements lie in an arbitrary field $mathbb{F}$, and let $G$ be the graph with vertex set ${1,ldots,n}$ such that distinct vertices $i$ and $j$ are adjacent if and only if $m_{ij} eq 0$. We in
troduce a dynamic programming algorithm that finds a diagonal matrix that is congruent to $M$. If $G$ is given with a tree decomposition $mathcal{T}$ of width $k$, then this can be done in time $O(k|mathcal{T}| + k^2 n)$, where $|mathcal{T}|$ denotes the number of nodes in $mathcal{T}$. Among other things, this allows one to compute the determinant, the rank and the inertia of a symmetric matrix in time $O(k|mathcal{T}| + k^2 n)$.
This volume contains papers presented at the Ninth International Symposium on Symbolic Computation in Software Science, SCSS 2021. Symbolic Computation is the science of computing with symbolic objects (terms, formulae, programs, representations of
algebraic objects, etc.). Powerful algorithms have been developed during the past decades for the major subareas of symbolic computation: computer algebra and computational logic. These algorithms and methods are successfully applied in various fields, including software science, which covers a broad range of topics about software construction and analysis. Meanwhile, artificial intelligence methods and machine learning algorithms are widely used nowadays in various domains and, in particular, combined with symbolic computation. Several approaches mix artificial intelligence and symbolic methods and tools deployed over large corpora to create what is known as cognitive systems. Cognitive computing focuses on building systems that interact with humans naturally by reasoning, aiming at learning at scale. The purpose of SCSS is to promote research on theoretical and practical aspects of symbolic computation in software science, combined with modern artificial intelligence techniques. These proceedings contain the keynote paper by Bruno Buchberger and ten contributed papers. Besides, the conference program included three invited talks, nine short and work-in-progress papers, and a special session on computer algebra and computational logic. Due to the COVID-19 pandemic, the symposium was held completely online. It was organized by the Research Institute for Symbolic Computation (RISC) of the Johannes Kepler University Linz on September 8--10, 2021.
We present OGRe, a modern Mathematica package for tensor calculus, designed to be both powerful and user-friendly. The package can be used in a variety of contexts where tensor calculations are needed, in both mathematics and physics, but it is espec
ially suitable for general relativity. By implementing an object-oriented design paradigm, OGRe allows calculating arbitrarily complicated tensor formulas easily, and automatically transforms between index configurations and coordinate systems behind the scenes as needed, eliminating user errors by making it impossible for the user to combine tensors in inconsistent ways. Other features include displaying tensors in various forms, automatic calculation of curvature tensors and geodesic equations, easy importing and exporting of tensors between sessions, optimized algorithms and parallelization for improved performance, and more.
The previous VPT 2020 workshop was organized in honour of Professor Alberto Pettorossi on the occasion of his academic retirement from Universit`a di Roma Tor Vergata. Due to the pandemic the VPT 2020 meeting was cancelled but its proceeding have alr
eady appeared in the EPTCS 320 volume. The joint VPT-20-21 event has subsumed the original programme of VPT 2020 and provided an opportunity to meet and celebrate the achievements of Professor Alberto Pettorossi; its programme was further expanded with the newly submitted presentations for VPT 2021. The aim of the VPT workshop series is to provide a forum where people from the areas of program transformation and program verification can fruitfully exchange ideas and gain a deeper understanding of the interactions between those two fields.
This paper explores the use of relational symbolic execution to counter timing side channels in WebAssembly programs. We design and implement Vivienne, an open-source tool to automatically analyze WebAssembly cryptographic libraries for constant-time
violations. Our approach features various optimizations that leverage the structure of WebAssembly and automated theorem provers, including support for loops via relational invariants. We evaluate Vivienne on 57 real-world cryptographic implementations, including a previously unverified implementation of the HACL* library in WebAssembly. The results indicate that Vivienne is a practical solution for constant-time analysis of cryptographic libraries in WebAssembly.
