66 citations · 97 across the 11 of their papers we have counts for
16 papers
An Exact Formulation of Phase-Space Electronic Structure Theory in One Dimension by Exploiting the Zero Curvature Condition
Zain Zaidi, Yotam M. Y. Feldman, Linqing Peng +1
We show that, for the unique case of a system of electrons and nuclei in one dimension, the $\hGamma$ operator in phase space electronic structure theory has a zero non-Abelian cur…
Bosonic Condensed Phase Real-time Dynamics from Ring Polymer Molecular Dynamics
Yotam M. Y. Feldman, Sourav Karmakar, Sutirtha Paul +3
We present a method for approximating real-time correlation functions and quantum transport coefficients of bosonic condensed phases. The direct evaluation of quantum real-time cor…
fix pimd/langevin: An Efficient Implementation of Path Integral Molecular Dynamics in LAMMPS
Yifan Li, Axel Gomez, Kehan Cai +10
Path integral molecular dynamics (PIMD), which maps a quantum particle onto a fictitious classical system of ring polymers and propagates the "beads" of this extended classical sys…
Periodic Boundary Conditions for Bosonic Path Integral Molecular Dynamics
Jacob Higer, Yotam M. Y. Feldman, Barak Hirshberg
We develop an algorithm for bosonic path integral molecular dynamics (PIMD) simulations with periodic boundary conditions (PBC) that scales quadratically with the number of particl…
Defect Positioning in Combinatorial Metamaterials
Chaviva Sirote-Katz, Yotam M. Y. Feldman, Guy Cohen +2
Combinatorial mechanical metamaterials are made of anisotropic, flexible blocks, such that multiple metamaterials may be constructed using a single block type, and the system's res…
i-PI 3.0: a flexible and efficient framework for advanced atomistic simulations
Yair Litman, Venkat Kapil, Yotam M. Y. Feldman +13
Atomic-scale simulations have progressed tremendously over the past decade, largely due to the availability of machine-learning interatomic potentials. These potentials combine the…
Optimal Symbolic Bound Synthesis
John Cyphert, Yotam Feldman, Zachary Kincaid +1
The problem of finding a constant bound on a term given a set of assumptions has wide applications in optimization as well as program analysis. However, in many contexts the object…
Quadratic Scaling Bosonic Path Integral Molecular Dynamics
Yotam M. Y. Feldman, Barak Hirshberg
Bosonic exchange symmetry leads to fascinating quantum phenomena, from exciton condensation in quantum materials to the superfluidity of liquid Helium-4. Unfortunately, path integr…
Invariant Inference With Provable Complexity From the Monotone Theory
Yotam M. Y. Feldman, Sharon Shoham
Invariant inference algorithms such as interpolation-based inference and IC3/PDR show that it is feasible, in practice, to find inductive invariants for many interesting systems, b…
Property-Directed Reachability as Abstract Interpretation in the Monotone Theory
Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham +1
Inferring inductive invariants is one of the main challenges of formal verification. The theory of abstract interpretation provides a rich framework to devise invariant inference a…
Proving Highly-Concurrent Traversals Correct
Yotam M. Y. Feldman, Artem Khyzha, Constantin Enea +4
Modern highly-concurrent search data structures, such as search trees, obtain multi-core scalability and performance by having operations traverse the data structure without any sy…
Learning the Boundary of Inductive Invariants
Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham +1
We study the complexity of invariant inference and its connections to exact concept learning. We define a condition on invariants and their geometry, called the fence condition, wh…
Complexity and Information in Invariant Inference
Yotam M. Y. Feldman, Neil Immerman, Mooly Sagiv +1
This paper addresses the complexity of SAT-based invariant inference, a prominent approach to safety verification. We consider the problem of inferring an inductive invariant of po…
Inferring Inductive Invariants from Phase Structures
Yotam M. Y. Feldman, James R. Wilcox, Sharon Shoham +1
Infinite-state systems such as distributed protocols are challenging to verify using interactive theorem provers or automatic verification tools. Of these techniques, deductive ver…
Order out of Chaos: Proving Linearizability Using Local Views
Yotam M. Y. Feldman, Constantin Enea, Adam Morrison +2
Proving the linearizability of highly concurrent data structures, such as those using optimistic concurrency control, is a challenging task. The main difficulty is in reasoning abo…
Bounded Quantifier Instantiation for Checking Inductive Invariants
Yotam M. Y. Feldman, Oded Padon, Neil Immerman +2
We consider the problem of checking whether a proposed invariant expressed in first-order logic with quantifier alternation is inductive, i.e. preserved by a piece of code. Whi…