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.

Yoshi Krockenberger (NTT Basic Research Laboratories): LRSM Seminar

LRSM Reading Room 3231 Walnut St, Philadelphia, PA, United States

Title: “Molecular beam epitaxy of functional complex 4d & 5d transition metal oxides”

The discovery of high-temperature superconductivity in cuprates in 1986 ignited significant research into complex transition metal oxides. While 3d oxides have been extensively studied, 4d and 5d systems have been less explored due to challenges in achieving high-quality growth and controlling volatile oxide formation.

We have developed an electron-beam molecular beam epitaxy (EB-MBE) system equipped with electron impact emission spectrometry (EIES) for precise real-time control of elemental fluxes. This approach enables the synthesis of complex 4d and 5d transition metal oxides with tailored stoichiometries. To address the issue of volatile oxide formation, we employ a rate control system that compensates for element loss during oxidation.

To optimize the growth process, we have implemented a Bayesian optimization-based machine learning method. This approach allows for efficient exploration of the parameter space, enabling us to identify optimal growth conditions. By combining machine learning with EB-MBE, we can accelerate the discovery and synthesis of new materials with intriguing physical properties, such as palladates like Nd2−xCexPdO4.

A notable achievement is the synthesis of the first gold oxide, Sr5Au3O8, using molecular beam epitaxy. We will also discuss our recent progress in synthesizing complex osmates, a class of materials known for their high volatility and challenging growth conditions. Sr3OsO6, a double-perovskite related structure, exhibits the highest Curie temperature discovered so far among insulators. Our approach demonstrates the potential of EB-MBE and machine learning for exploring the frontiers of complex transition metal oxide materials science.