Events Search and Views Navigation

Event Views Navigation

Today

Stephen Wilson (UC Santa Barbara): Materials Science and Engineering Seminar

Wu and Chen Auditorium (Levine Hall) 3330 Walnut Street, Philadelphia, PA, United States

Title: “Kagome Metals and Their Unusual Electronic Properties”

In this talk, I will discuss new inroads in the study of electronic order within classes of metals built from kagome lattices or networks of corner sharing triangles.  The electronic band structures of these compounds are known to host a series of features such as Dirac crossings, saddle points, and flat bands at select carrier fillings.  Tuning the electron filing about these features has the potential to stabilize a variety of exotic electronic states such as orbital magnetism, bond density wave order, and unconventional superconductivity; however experimental realization of these states has been a historical challenge.  Recently, a number of new compounds built from kagome lattices with band fillings near each of these features have been discovered, and I will provide an overview of progress in studying their anomalous properties.  Particular focus will be given to electronic instabilities realized in kagome metals with their Fermi levels close to the saddle points in their band structures.

Ronghui Gu (Columbia University): Computer and Information Science Seminar

Wu and Chen Auditorium (Levine Hall) 3330 Walnut Street, Philadelphia, PA, United States

Title: “Scaling Machine-Checkable Systems Verification in Coq”

System software like operating systems and hypervisors forms the critical backbone of our computing infrastructure. However, due to their size and complexity, these systems often contain vulnerabilities that can compromise security. Formal verification offers a solution by mathematically proving software correctness, but its adoption is hindered by the substantial effort required to create these proofs.

In this talk, I will introduce Spoq, a highly automated verification framework designed to dramatically reduce the proof effort in verifying system software. Spoq leverages LLVM to automatically translate C code—including full C semantics like macros, inline assembly, and compiler directives—into Coq, a proof assistant for formal verification. This automation eliminates the need for manual modification of source code prior to verification. Spoq leverages a layering proof strategy and introduces novel Coq tactics and transformation rules to automatically generate layer specifications and refinement proofs to simplify verification of concurrent system software. Spoq also supports easy integration of manually written layer specifications and refinement proofs. We applied Spoq to verify a multiprocessor KVM hypervisor implementation. Verification using Spoq required 70% less proof effort than the manually written specifications and proofs to verify an older implementation. Furthermore, the proofs using Spoq hold for the unmodified implementation that is directly compiled and executed.

Joe Checkelsky (MIT): Materials Science and Engineering Seminar

Wu and Chen Auditorium (Levine Hall) 3330 Walnut Street, Philadelphia, PA, United States

Title: “Quantum Materials: A View from the Lattice”

Connecting theoretical models for exotic quantum states to real materials is a key goal in quantum materials science. The structure of the crystalline lattice plays a foundational role in this pursuit in the subfield of quantum material synthesis. We here revisit this long-standing perspective in the context low dimensional emergent electronic phases of matter, including the realization of model two-dimensional topological and correlated electronic phenomena. Along the way, we discuss how to define a quantum material, and how this definition has evolved in recent years. Finally, we comment on the perspective for realizing further two-dimensional model systems in complex material structures and connections to new paradigms for programmable quantum matter.