An official website of the United States government
Algorithms for orbit closure separation for invariants and semi-invariants of matrices
More Like this
-
Webs yield an especially important realization of certain Specht modules, irreducible representations of symmetric groups, as they provide a pictorial basis with a convenient diagrammatic calculus. In recent work, the last three authors associated polynomials to noncrossing partitions without singleton blocks, so that the corresponding polynomials form a web basis of the pennant Specht module S(d,d,1n−2d). These polynomials were interpreted as global sections of a line bundle on a 2-step partial flag variety. Here, we both simplify and extend this construction. On the one hand, we show that these polynomials can alternatively be situated in the homogeneous coordinate ring of a Grassmannian, instead of a 2-step partial flag variety, and can be realized as tensor invariants of classical (but highly nonplanar) tensor diagrams. On the other hand, we extend these ideas from the pennant Specht module S(d,d,1n−2d) to more general flamingo Specht modules S(dr,1n−rd). In the hook case r=1, we obtain a spanning set that can be restricted to a basis in various ways. In the case r>2, we obtain a basis of a well-behaved subspace of S(dr,1n−rd), but not of the entire module.more » « less
-
Abstract Spectre class of transient execution security attacks on modern microprocessors rely on speculative execution. Software Controlled Speculation (SCS) was proposed as a microarchitecture‐level defense in the original Spectre paper and has also been adopted by ARM. The idea with SCS is to allow a mode in the microarchitecture, where instructions that read from memory are not allowed to execute speculatively. Errors or malicious fault‐injections in the implementation of SCS can still render the microarchitecture vulnerable to Spectre attacks. A formal verification method is proposed that can check the correctness of the implementation of SCS and detect any faults. The method has been demonstrated to be very efficient on two sets of benchmarks and provides accurate detection of implementation faults in SCS.more » « less
-
One aspect of developing correct code, code that functions as specified, is annotating loops with suitable invariants. Loop invariants are useful for human reasoning and are necessary for tool-assisted automated reasoning. Writing loop invariants can be a difficult task for all students, especially beginning software engineering students. In helping students learn to write adequate invariants, we need to understand not only what errors they make, but also why they make them. This poster discusses the use of a Web IDE backed by the RESOLVE verification engine to aid students in developing loop invariants and to collect performance data. In addition to collecting submitted invariant answers, students are asked to provide their steps or thought processes regarding how they arrived at their answers for each submission. The answers and reasons are then analyzed using a mixed-methods approach. Resulting categories of answers indicate that students are able to use formal method concepts with which they are already familiar, such as, pre and post-conditions as a starting place to develop adequate loop invariants. Additionally, some common trouble spots in learning to write invariants are identified. The results will be useful to guide classroom instruction and automated tutoring.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Journal Article:
- https://doi.org/10.2140/ant.2020.14.2791
