Showing 1–20 of 20 results for author: Wolf, F A

Protocols to Code: Formal Verification of a Next-Generation Internet Router

Authors: João C. Pereira, Tobias Klenze, Sofia Giampietro, Markus Limbeck, Dionysios Spiliopoulos, Felix A. Wolf, Marco Eilers, Christoph Sprenger, David Basin, Peter Müller, Adrian Perrig

Abstract: We present the first formally-verified Internet router, which is part of the SCION Internet architecture. SCION routers run a cryptographic protocol for secure packet forwarding in an adversarial environment. We verify both the protocol's network-wide security properties and low-level properties of its implementation. More precisely, we develop a series of protocol models by refinement in Isabelle… ▽ More We present the first formally-verified Internet router, which is part of the SCION Internet architecture. SCION routers run a cryptographic protocol for secure packet forwarding in an adversarial environment. We verify both the protocol's network-wide security properties and low-level properties of its implementation. More precisely, we develop a series of protocol models by refinement in Isabelle/HOL and we use an automated program verifier to prove that the router's Go code satisfies memory safety, crash freedom, freedom from data races, and adheres to the protocol model. Both verification efforts are soundly linked together. Our work demonstrates the feasibility of coherently verifying a critical network component from high-level protocol models down to performance-optimized production code, developed by an independent team. In the process, we uncovered critical bugs in both the protocol and its implementation, which were confirmed by the code developers, and we strengthened the protocol's security properties. This paper explains our approach, summarizes the main results, and distills lessons for the design and implementation of verifiable systems, for the handling of continuous changes, and for the verification techniques and tools employed. △ Less

Submitted 9 May, 2024; originally announced May 2024.

Sound Verification of Security Protocols: From Design to Interoperable Implementations (extended version)

Authors: Linard Arquint, Felix A. Wolf, Joseph Lallemand, Ralf Sasse, Christoph Sprenger, Sven N. Wiesner, David Basin, Peter Müller

Abstract: We provide a framework consisting of tools and metatheorems for the end-to-end verification of security protocols, which bridges the gap between automated protocol verification and code-level proofs. We automatically translate a Tamarin protocol model into a set of I/O specifications expressed in separation logic. Each such specification describes a protocol role's intended I/O behavior against wh… ▽ More We provide a framework consisting of tools and metatheorems for the end-to-end verification of security protocols, which bridges the gap between automated protocol verification and code-level proofs. We automatically translate a Tamarin protocol model into a set of I/O specifications expressed in separation logic. Each such specification describes a protocol role's intended I/O behavior against which the role's implementation is then verified. Our soundness result guarantees that the verified implementation inherits all security (trace) properties proved for the Tamarin model. Our framework thus enables us to leverage the substantial body of prior verification work in Tamarin to verify new and existing implementations. The possibility to use any separation logic code verifier provides flexibility regarding the target language. To validate our approach and show that it scales to real-world protocols, we verify a substantial part of the official Go implementation of the WireGuard VPN key exchange protocol. △ Less

Submitted 8 December, 2022; originally announced December 2022.

Gobra: Modular Specification and Verification of Go Programs (extended version)

Authors: Felix A. Wolf, Linard Arquint, Martin Clochard, Wytse Oortwijn, João C. Pereira, Peter Müller

Abstract: Go is an increasingly-popular systems programming language targeting, especially, concurrent and distributed systems. Go differentiates itself from other imperative languages by offering structural subty** and lightweight concurrency through goroutines with message-passing communication. This combination of features poses interesting challenges for static verification, most prominently the combi… ▽ More Go is an increasingly-popular systems programming language targeting, especially, concurrent and distributed systems. Go differentiates itself from other imperative languages by offering structural subty** and lightweight concurrency through goroutines with message-passing communication. This combination of features poses interesting challenges for static verification, most prominently the combination of a mutable heap and advanced concurrency primitives. We present Gobra, a modular, deductive program verifier for Go that proves memory safety, crash safety, data-race freedom, and user-provided specifications. Gobra is based on separation logic and supports a large subset of Go. Its implementation translates an annotated Go program into the Viper intermediate verification language and uses an existing SMT-based verification backend to compute and discharge proof obligations. △ Less

Submitted 28 May, 2021; originally announced May 2021.

Concise Outlines for a Complex Logic: A Proof Outline Checker for TaDA (Full Paper)

Authors: Felix A. Wolf, Malte Schwerhoff, Peter Müller

Abstract: Modern separation logics allow one to prove rich properties of intricate code, e.g. functional correctness and linearizability of non-blocking concurrent code. However, this expressiveness leads to a complexity that makes these logics difficult to apply. Manual proofs or proofs in interactive theorem provers consist of a large number of steps, often with subtle side conditions. On the other hand,… ▽ More Modern separation logics allow one to prove rich properties of intricate code, e.g. functional correctness and linearizability of non-blocking concurrent code. However, this expressiveness leads to a complexity that makes these logics difficult to apply. Manual proofs or proofs in interactive theorem provers consist of a large number of steps, often with subtle side conditions. On the other hand, automation with dedicated verifiers typically requires sophisticated proof search algorithms that are specific to the given program logic, resulting in limited tool support that makes it difficult to experiment with program logics, e.g. when learning, improving, or comparing them. Proof outline checkers fill this gap. Their input is a program annotated with the most essential proof steps, just like the proof outlines typically presented in papers. The tool then checks automatically that this outline represents a valid proof in the program logic. In this paper, we systematically develop a proof outline checker for the TaDA logic, which reduces the checking to a simpler verification problem, for which automated tools exist. Our approach leads to proof outline checkers that provide substantially more automation than interactive provers, but are much simpler to develop than custom automatic verifiers. △ Less

Submitted 13 August, 2021; v1 submitted 14 October, 2020; originally announced October 2020.

Igloo: Soundly Linking Compositional Refinement and Separation Logic for Distributed System Verification

Authors: Christoph Sprenger, Tobias Klenze, Marco Eilers, Felix A. Wolf, Peter Müller, Martin Clochard, David Basin

Abstract: Lighthouse projects such as CompCert, seL4, IronFleet, and DeepSpec have demonstrated that full verification of entire systems is feasible by establishing a refinement relation between an abstract system specification and an executable implementation. Existing approaches however impose severe restrictions on either the abstract system specifications due to their limited expressiveness or versatili… ▽ More Lighthouse projects such as CompCert, seL4, IronFleet, and DeepSpec have demonstrated that full verification of entire systems is feasible by establishing a refinement relation between an abstract system specification and an executable implementation. Existing approaches however impose severe restrictions on either the abstract system specifications due to their limited expressiveness or versatility, or on the executable code due to their reliance on suboptimal code extraction or inexpressive program logics. We propose a novel methodology that combines the compositional refinement of abstract, event-based models of distributed systems with the verification of full-fledged program code using expressive separation logics, which support features of realistic programming languages like mutable heap data structures and concurrency. The main technical contribution of our work is a formal framework that soundly relates event-based system models to program specifications in separation logics, such that successful verification establishes a refinement relation between the model and the code. We formalized our framework, Igloo, in Isabelle/HOL. Our framework enables the sound combination of tools for protocol development with existing program verifiers. We report on three case studies, a leader election protocol, a replication protocol, and a security protocol, for which we refine formal requirements into program specifications (in Isabelle/HOL) that we implement in Java and Python and prove correct using the VeriFast and Nagini tools. △ Less

Submitted 9 October, 2020; originally announced October 2020.

Conditional out-of-sample generation for unpaired data using trVAE

Authors: Mohammad Lotfollahi, Mohsen Naghipourfar, Fabian J. Theis, F. Alexander Wolf

Abstract: While generative models have shown great success in generating high-dimensional samples conditional on low-dimensional descriptors (learning e.g. stroke thickness in MNIST, hair color in CelebA, or speaker identity in Wavenet), their generation out-of-sample poses fundamental problems. The conditional variational autoencoder (CVAE) as a simple conditional generative model does not explicitly relat… ▽ More While generative models have shown great success in generating high-dimensional samples conditional on low-dimensional descriptors (learning e.g. stroke thickness in MNIST, hair color in CelebA, or speaker identity in Wavenet), their generation out-of-sample poses fundamental problems. The conditional variational autoencoder (CVAE) as a simple conditional generative model does not explicitly relate conditions during training and, hence, has no incentive of learning a compact joint distribution across conditions. We overcome this limitation by matching their distributions using maximum mean discrepancy (MMD) in the decoder layer that follows the bottleneck. This introduces a strong regularization both for reconstructing samples within the same condition and for transforming samples across conditions, resulting in much improved generalization. We refer to the architecture as \emph{transformer} VAE (trVAE). Benchmarking trVAE on high-dimensional image and tabular data, we demonstrate higher robustness and higher accuracy than existing approaches. In particular, we show qualitatively improved predictions for cellular perturbation response to treatment and disease based on high-dimensional single-cell gene expression data, by tackling previously problematic minority classes and multiple conditions. For generic tasks, we improve Pearson correlations of high-dimensional estimated means and variances with their ground truths from 0.89 to 0.97 and 0.75 to 0.87, respectively. △ Less

Submitted 30 October, 2019; v1 submitted 3 October, 2019; originally announced October 2019.

Comments: Added reference to Johansson et al. (2016) and removed sentences from Lopez et al. (2018) in the background section (see acknowledgements)

Imaginary-time matrix product state impurity solver for dynamical mean-field theory

Authors: F. Alexander Wolf, Ara Go, Ian P. McCulloch, Andrew J. Millis, Ulrich Schollwöck

Abstract: We present a new impurity solver for dynamical mean-field theory based on imaginary-time evolution of matrix product states. This converges the self-consistency loop on the imaginary-frequency axis and obtains real-frequency information in a final real-time evolution. Relative to computations on the real-frequency axis, required bath sizes are much smaller and less entanglement is generated, so mu… ▽ More We present a new impurity solver for dynamical mean-field theory based on imaginary-time evolution of matrix product states. This converges the self-consistency loop on the imaginary-frequency axis and obtains real-frequency information in a final real-time evolution. Relative to computations on the real-frequency axis, required bath sizes are much smaller and less entanglement is generated, so much larger systems can be studied. The power of the method is demonstrated by solutions of a three band model in the single and two-site dynamical mean-field approximation. Technical issues are discussed, including details of the method, efficiency as compared to other matrix product state based impurity solvers, bath construction and its relation to real-frequency computations and the analytic continuation problem of quantum Monte Carlo, the choice of basis in dynamical cluster approximation, and perspectives for off-diagonal hybridization functions. △ Less

Submitted 30 July, 2015; originally announced July 2015.

Comments: 8 pages + 4 pages appendix, 9 figures

Journal ref: Phys. Rev. X 5, 041032 (2015)

How to discretize a quantum bath for real-time evolution

Authors: Ines de Vega, Ulrich Schollwöck, F. Alexander Wolf

Abstract: Many numerical techniques for the description of quantum systems that are coupled to a continuous bath require the discretization of the latter. To this end, a wealth of methods has been developed in the literature, which we classify as (i) direct discretization, (ii) orthogonal polynomial, and (iii) numerical optimization strategies. We recapitulate strategies (i) and (ii) to clarify their relati… ▽ More Many numerical techniques for the description of quantum systems that are coupled to a continuous bath require the discretization of the latter. To this end, a wealth of methods has been developed in the literature, which we classify as (i) direct discretization, (ii) orthogonal polynomial, and (iii) numerical optimization strategies. We recapitulate strategies (i) and (ii) to clarify their relation. For quadratic Hamiltonians, we show that (ii) is the best strategy in the sense that it gives the numerically exact time evolution up to a maximum time $t_\text{max}$, for which we give a simple expression. For non-quadratic Hamiltonians, we show that no such best strategy exists. We present numerical examples relevant to open quantum systems and strongly correlated systems, as treated by dynamical mean-field theory (DMFT). △ Less

Submitted 21 October, 2015; v1 submitted 27 July, 2015; originally announced July 2015.

Journal ref: Phys. Rev. B 92, 155126 (2015)

Non-thermal melting of Neel order in the Hubbard model

Authors: Karsten Balzer, F. Alexander Wolf, Ian P. McCulloch, Philipp Werner, Martin Eckstein

Abstract: We study the unitary time evolution of antiferromagnetic order in the Hubbard model after a quench starting from the perfect Néel state. In this setup, which is well suited for experiments with cold atoms, one can distinguish fundamentally different pathways for melting of long-range order at weak and strong interaction. In the Mott insulating regime, melting of long-range order occurs due to the… ▽ More We study the unitary time evolution of antiferromagnetic order in the Hubbard model after a quench starting from the perfect Néel state. In this setup, which is well suited for experiments with cold atoms, one can distinguish fundamentally different pathways for melting of long-range order at weak and strong interaction. In the Mott insulating regime, melting of long-range order occurs due to the ultra-fast transfer of energy from charge excitations to the spin background, while local magnetic moments and their exchange coupling persist during the process. The latter can be demonstrated by a local spin-precession experiment. At weak interaction, local moments decay along with the long-range order. The dynamics is governed by residual quasiparticles, which are reflected in oscillations of the off-diagonal components of the momentum distribution. Such oscillations provide an alternative route to study the prethermalization phenomenon and its influence on the dynamics away from the integrable (noninteracting) limit. The Hubbard model is solved within nonequilibrium dynamical mean-field theory, using the density matrix-renormalization group as an impurity solver. △ Less

Submitted 9 April, 2015; originally announced April 2015.

Comments: 11 pages

Journal ref: Phys. Rev. X 5, 031039 (2015)

Spectral functions and time evolution from the Chebyshev recursion

Authors: F. Alexander Wolf, Jorge A. Justiniano, Ian P. McCulloch, Ulrich Schollwöck

Abstract: We link linear prediction of Chebyshev and Fourier expansions to analytic continuation. We push the resolution in the Chebyshev-based computation of $T=0$ many-body spectral functions to a much higher precision by deriving a modified Chebyshev series expansion that allows to reduce the expansion order by a factor $\sim\frac{1}{6}$. We show that in a certain limit the Chebyshev technique becomes eq… ▽ More We link linear prediction of Chebyshev and Fourier expansions to analytic continuation. We push the resolution in the Chebyshev-based computation of $T=0$ many-body spectral functions to a much higher precision by deriving a modified Chebyshev series expansion that allows to reduce the expansion order by a factor $\sim\frac{1}{6}$. We show that in a certain limit the Chebyshev technique becomes equivalent to computing spectral functions via time evolution and subsequent Fourier transform. This introduces a novel recursive time evolution algorithm that instead of the group operator $e^{-iHt}$ only involves the action of the generator $H$. For quantum impurity problems, we introduce an adapted discretization scheme for the bath spectral function. We discuss the relevance of these results for matrix product state (MPS) based DMRG-type algorithms, and their use within dynamical mean-field theory (DMFT). We present strong evidence that the Chebyshev recursion extracts less spectral information from $H$ than time evolution algorithms when fixing a given amount of created entanglement. △ Less

Submitted 27 April, 2015; v1 submitted 28 January, 2015; originally announced January 2015.

Comments: 12 pages + 6 pages appendix, 11 figures

Journal ref: Phys. Rev. B 91, 115144 (2015)

A Strictly Single-Site DMRG Algorithm with Subspace Expansion

Authors: Claudius Hubig, Ian P. McCulloch, Ulrich Schollwöck, F. Alexander Wolf

Abstract: We introduce a strictly single-site DMRG algorithm based on the subspace expansion of the Alternating Minimal Energy (AMEn) method. The proposed new MPS basis enrichment method is sufficient to avoid local minima during the optimisation, similarly to the density matrix perturbation method, but computationally cheaper. Each application of $\hat H$ to $|Ψ\rangle$ in the central eigensolver is reduce… ▽ More We introduce a strictly single-site DMRG algorithm based on the subspace expansion of the Alternating Minimal Energy (AMEn) method. The proposed new MPS basis enrichment method is sufficient to avoid local minima during the optimisation, similarly to the density matrix perturbation method, but computationally cheaper. Each application of $\hat H$ to $|Ψ\rangle$ in the central eigensolver is reduced in cost for a speed-up of $\approx (d + 1)/2$, with $d$ the physical site dimension. Further speed-ups result from cheaper auxiliary calculations and an often greatly improved convergence behaviour. Runtime to convergence improves by up to a factor of 2.5 on the Fermi-Hubbard model compared to the previous single-site method and by up to a factor of 3.9 compared to two-site DMRG. The method is compatible with real-space parallelisation and non-abelian symmetries. △ Less

Submitted 12 April, 2015; v1 submitted 22 January, 2015; originally announced January 2015.

Comments: 9 pages, 6 figures; added comparison with two-site DMRG

Journal ref: Phys. Rev. B 91, 155115 (2015)

Solving nonequilibrium dynamical mean-field theory using matrix product states

Authors: F. Alexander Wolf, Ian P. McCulloch, Ulrich Schollwöck

Abstract: We solve the nonequilibrium dynamical mean-field theory (DMFT) using matrix product states (MPS). This allows us to treat much larger bath sizes and by that reach substantially longer times (factor $\sim$ 2 -- 3) than with exact diagonalization. We show that the star geometry of the underlying impurity problem can have substantially better entanglement properties than the previously favoured chain… ▽ More We solve the nonequilibrium dynamical mean-field theory (DMFT) using matrix product states (MPS). This allows us to treat much larger bath sizes and by that reach substantially longer times (factor $\sim$ 2 -- 3) than with exact diagonalization. We show that the star geometry of the underlying impurity problem can have substantially better entanglement properties than the previously favoured chain geometry. This has immense consequences for the efficiency of an MPS-based description of general impurity problems: in the case of equilibrium DMFT, it leads to an orders-of-magnitude speedup. We introduce an approximation for the two-time hybridization function that uses time-translational invariance, which can be observed after a certain relaxation time after a quench to a time-independent Hamiltonian. △ Less

Submitted 19 December, 2014; v1 submitted 13 October, 2014; originally announced October 2014.

Comments: 11 pages + 3 pages appendix, 14 figures

Journal ref: Phys. Rev. B 90, 235131 (2014)

Chebyshev Matrix Product State Impurity Solver for the Dynamical Mean-Field Theory

Authors: F. Alexander Wolf, Ian P. McCulloch, Olivier Parcollet, Ulrich Schollwöck

Abstract: We compute the spectral functions for the two-site dynamical cluster theory and for the two-orbital dynamical mean-field theory in the density-matrix renormalization group (DMRG) framework using Chebyshev expansions represented with matrix product states (MPS). We obtain quantitatively precise results at modest computational effort through technical improvements regarding the truncation scheme and… ▽ More We compute the spectral functions for the two-site dynamical cluster theory and for the two-orbital dynamical mean-field theory in the density-matrix renormalization group (DMRG) framework using Chebyshev expansions represented with matrix product states (MPS). We obtain quantitatively precise results at modest computational effort through technical improvements regarding the truncation scheme and the Chebyshev rescaling procedure. We furthermore establish the relation of the Chebyshev iteration to real-time evolution, and discuss technical aspects as computation time and implementation in detail. △ Less

Submitted 7 July, 2014; originally announced July 2014.

Comments: 20 pages, 12 figures

Journal ref: Phys. Rev. B 90, 115124 (2014)

Dynamical correlation functions and the quantum Rabi model

Authors: F. Alexander Wolf, Fabio Vallone, Guillermo Romero, Marcus Kollar, Enrique Solano, Daniel Braak

Abstract: We study the quantum Rabi model within the framework of the analytical solution developed in Phys. Rev. Lett. 107,100401 (2011). In particular, through time-dependent correlation functions, we give a quantitative criterion for classifying two regions of the quantum Rabi model, involving the Jaynes-Cummings, the ultrastrong, and deep strong coupling regimes. In addition, we find a stationary qubit-… ▽ More We study the quantum Rabi model within the framework of the analytical solution developed in Phys. Rev. Lett. 107,100401 (2011). In particular, through time-dependent correlation functions, we give a quantitative criterion for classifying two regions of the quantum Rabi model, involving the Jaynes-Cummings, the ultrastrong, and deep strong coupling regimes. In addition, we find a stationary qubit-field entangled basis that governs the whole dynamics as the coupling strength overcomes the mode frequency. △ Less

Submitted 8 February, 2013; v1 submitted 27 November, 2012; originally announced November 2012.

Comments: 8 pages, 8 figures. Revised version, accepted for publication in Physical Review A

Journal ref: Phys. Rev. A 87, 023835 (2013)

Exact real-time dynamics of the quantum Rabi model

Authors: F. Alexander Wolf, Marcus Kollar, Daniel Braak

Abstract: We use the analytical solution of the quantum Rabi model to obtain absolutely convergent series expressions of the exact eigenstates and their scalar products with Fock states. This enables us to calculate the numerically exact time evolution of <σ_x(t)> and <σ_z(t)> for all regimes of the coupling strength, without truncation of the Hilbert space. We find a qualitatively different behavior of bot… ▽ More We use the analytical solution of the quantum Rabi model to obtain absolutely convergent series expressions of the exact eigenstates and their scalar products with Fock states. This enables us to calculate the numerically exact time evolution of <σ_x(t)> and <σ_z(t)> for all regimes of the coupling strength, without truncation of the Hilbert space. We find a qualitatively different behavior of both observables which can be related to their representations in the invariant parity subspaces. △ Less

Submitted 22 May, 2012; v1 submitted 27 March, 2012; originally announced March 2012.

Comments: 8 pages, 7 figures, published version

Journal ref: Phys. Rev. A 85, 053817 (2012)

Expansion of Bose-Hubbard Mott insulators in optical lattices

Authors: Mark Jreissaty, Juan Carrasquilla, F. Alexander Wolf, Marcos Rigol

Abstract: We study the expansion of bosonic Mott insulators in the presence of an optical lattice after switching off a confining potential. We use the Gutzwiller mean-field approximation and consider two different setups. In the first one, the expansion is restricted to one direction. We show that this leads to the emergence of two condensates with well defined momenta, and argue that such a construct can… ▽ More We study the expansion of bosonic Mott insulators in the presence of an optical lattice after switching off a confining potential. We use the Gutzwiller mean-field approximation and consider two different setups. In the first one, the expansion is restricted to one direction. We show that this leads to the emergence of two condensates with well defined momenta, and argue that such a construct can be used to create atom lasers in optical lattices. In the second setup, we study Mott insulators that are allowed to expand in all directions in the lattice. In this case, a simple condensate is seen to develop within the mean-field approximation. However, its constituent bosons are found to populate many nonzero momentum modes. An analytic understanding of both phenomena in terms of the exact dispersion relation in the hard-core limit is presented. △ Less

Submitted 9 July, 2012; v1 submitted 4 August, 2011; originally announced August 2011.

Comments: 11 pages, 9 figures. Figures 2,3,4 corrected

Journal ref: Phys. Rev. A 84, 043610 (2011)

Supercurrent through grain boundaries in the presence of strong correlations

Authors: F. A. Wolf, S. Graser, F. Loder, T. Kopp

Abstract: Strong correlations are known to severely reduce the mobility of charge carriers near half-filling and thus have an important influence on the current carrying properties of grain boundaries in the high-$T_c$ cuprates. In this work we present an extension of the Gutzwiller projection approach to treat electronic correlations below as well as above half-filling consistently. We apply this method to… ▽ More Strong correlations are known to severely reduce the mobility of charge carriers near half-filling and thus have an important influence on the current carrying properties of grain boundaries in the high-$T_c$ cuprates. In this work we present an extension of the Gutzwiller projection approach to treat electronic correlations below as well as above half-filling consistently. We apply this method to investigate the critical current through grain boundaries with a wide range of misalignment angles for electron- and hole-doped systems. For the latter excellent agreement with experimental data is found. We further provide a detailed comparison to an analogous weak-coupling evaluation. △ Less

Submitted 14 April, 2012; v1 submitted 28 June, 2011; originally announced June 2011.

Comments: 4 pages, 3 figures

Journal ref: Phys. Rev. Lett. 108, 117002 (2012)

Generalized Gibbs ensemble prediction of prethermalization plateaus and their relation to nonthermal steady states in integrable systems

Authors: Marcus Kollar, F. Alexander Wolf, Martin Eckstein

Abstract: A quantum many-body system which is prepared in the ground state of an integrable Hamiltonian does not directly thermalize after a sudden small parameter quench away from integrability. Rather, it will be trapped in a prethermalized state and can thermalize only at a later stage. We discuss several examples for which this prethermalized state shares some properties with the nonthermal steady state… ▽ More A quantum many-body system which is prepared in the ground state of an integrable Hamiltonian does not directly thermalize after a sudden small parameter quench away from integrability. Rather, it will be trapped in a prethermalized state and can thermalize only at a later stage. We discuss several examples for which this prethermalized state shares some properties with the nonthermal steady state that emerges in the corresponding integrable system. These examples support the notion that nonthermal steady states in integrable systems may be viewed as prethermalized states that never decay further. Furthermore we show that prethermalization plateaus are under certain conditions correctly predicted by generalized Gibbs ensembles, which are the appropriate extension of standard statistical mechanics in the presence of many constants of motion. This establishes that the relaxation behaviors of integrable and nearly integrable systems are continuously connected and described by the same statistical theory. △ Less

Submitted 10 February, 2011; originally announced February 2011.

Comments: 11 pages, 2 figures

Journal ref: Phys. Rev. B 84, 054304 (2011)

Collapse and revival oscillations as a probe for the tunneling amplitude in an ultra-cold Bose gas

Authors: F. Alexander Wolf, Itay Hen, Marcos Rigol

Abstract: We present a theoretical study of the quantum corrections to the revival time due to finite tunneling in the collapse and revival of matter wave interference after a quantum quench. We study hard-core bosons in a superlattice potential and the Bose-Hubbard model by means of exact numerical approaches and mean-field theory. We consider systems without and with a trap** potential present. We show… ▽ More We present a theoretical study of the quantum corrections to the revival time due to finite tunneling in the collapse and revival of matter wave interference after a quantum quench. We study hard-core bosons in a superlattice potential and the Bose-Hubbard model by means of exact numerical approaches and mean-field theory. We consider systems without and with a trap** potential present. We show that the quantum corrections to the revival time can be used to accurately determine the value of the hop** parameter in experiments with ultracold bosons in optical lattices. △ Less

Submitted 7 February, 2011; v1 submitted 8 October, 2010; originally announced October 2010.

Comments: 10 pages, 12 figures, typos in section 3A corrected

Journal ref: Phys. Rev. A 82, 043601 (2010)

New theoretical approaches for correlated systems in nonequilibrium

Authors: M. Eckstein, A. Hackl, S. Kehrein, M. Kollar, M. Moeckel, P. Werner, F. A. Wolf

Abstract: We review recent developments in the theory of interacting quantum many-particle systems that are not in equilibrium. We focus mainly on the nonequilibrium generalizations of the flow equation approach and of dynamical mean-field theory (DMFT). In the nonequilibrium flow equation approach one first diagonalizes the Hamiltonian iteratively, performs the time evolution in this diagonal basis, and th… ▽ More We review recent developments in the theory of interacting quantum many-particle systems that are not in equilibrium. We focus mainly on the nonequilibrium generalizations of the flow equation approach and of dynamical mean-field theory (DMFT). In the nonequilibrium flow equation approach one first diagonalizes the Hamiltonian iteratively, performs the time evolution in this diagonal basis, and then transforms back to the original basis, thereby avoiding a direct perturbation expansion with errors that grow linearly in time. In nonequilibrium DMFT, on the other hand, the Hubbard model can be mapped onto a time-dependent self-consistent single-site problem. We discuss results from the flow equation approach for nonlinear transport in the Kondo model, and further applications of this method to the relaxation behavior in the ferromagnetic Kondo model and the Hubbard model after an interaction quench. For the interaction quench in the Hubbard model, we have also obtained numerical DMFT results using quantum Monte Carlo simulations. In agreement with the flow equation approach they show that for weak coupling the system relaxes to a "prethermalized" intermediate state instead of rapid thermalization. We discuss the description of nonthermal steady states with generalized Gibbs ensembles. △ Less

Submitted 27 May, 2010; originally announced May 2010.

Comments: 19 pages, 6 figures, submitted to Eur. Phys. J. for publication in the Special Topics volume "Cooperative Phenomena in Solids: Metal-Insulator Transitions and Ordering of Microscopic Degrees of Freedom"

Journal ref: Eur. Phys. J. Special Topics 180, 217 (2010)