Showing 1–31 of 31 results for author: Summers, A

Catalysis in Extreme Field Environments: The Case of Strongly Ionized $SiO_{2}$ Nanoparticle Surfaces

Authors: Thomas M. Linker, Ritika Dagar, Alexandra Feinberg, Samuel Sahel-Schackis, Ken-ichi Nomura, Aiichiro Nakano, Fuyuki Shimojo, Priya Vashishta, Uwe Bergmann, Matthias F. Kling, Adam M. Summers

Abstract: High electric fields can significantly alter catalytic environments and the resultant chemical processes. Such fields arise naturally in biological systems but can also be artificially induced through localized excitations at nanoscale. Recently, strong field excitation of dielectric nanoparticles has emerged as an avenue for studying catalysis in highly ionized environments producing extreme elec… ▽ More High electric fields can significantly alter catalytic environments and the resultant chemical processes. Such fields arise naturally in biological systems but can also be artificially induced through localized excitations at nanoscale. Recently, strong field excitation of dielectric nanoparticles has emerged as an avenue for studying catalysis in highly ionized environments producing extreme electric fields. While the dynamics of surface ion emission driven by ultrafast laser ionization has been heavily explored, understanding the molecular dynamics leading to fragmentation has remained elusive. To address this, we employed a multiscale approach utilizing non-adiabatic quantum molecular dynamics (NAQMD) simulations on hydrogenated silica surfaces in both bare and wetted environments under field conditions mimicking those of an ionized nanoparticle. Our findings indicate that hole localization drives fragmentation dynamics, leading to surface silanol dissociation within 50 fs and charge transfer-induced water splitting in wetted environments within 150 fs. Further insight into such ultrafast mechanisms is critical for advancement of catalysis on the surface of charged nanosystems. △ Less

Submitted 24 June, 2024; v1 submitted 21 June, 2024; originally announced June 2024.

Design and Performance of a Magnetic Bottle Electron Spectrometer for High-Energy Photoelectron Spectroscopy

Authors: Kurtis Borne, Jordan T ONeal, Jun Wang, Erk Isele, Razib Obaid, Nora Berrah, Xinxin Cheng, Philip H Bucksbaum, Justin James, Andri Kamalov, Kirk A Larsen, Xiang Li, Ming-Fu Lin, Yusong Liu, Agostino Marinelli, Adam Summers, Emily Thierstein, Thomas Wolf, Daniel Rolles, Peter Walter, James P Cryan, Taran Driver

Abstract: We describe the design and performance of a magnetic bottle electron spectrometer~(MBES) for high-energy electron spectroscopy. Our design features a ${\sim2}$~m long electron drift tube and electrostatic retardation lens, achieving sub-electronvolt (eV) electron kinetic energy resolution for high energy (several hundred eV) electrons with close to 4$π$ collection efficiency. A segmented anode… ▽ More We describe the design and performance of a magnetic bottle electron spectrometer~(MBES) for high-energy electron spectroscopy. Our design features a ${\sim2}$~m long electron drift tube and electrostatic retardation lens, achieving sub-electronvolt (eV) electron kinetic energy resolution for high energy (several hundred eV) electrons with close to 4$π$ collection efficiency. A segmented anode electron detector enables the simultaneous collection of photoelectron spectra in high resolution and high collection efficiency modes. This versatile instrument is installed at the TMO endstation at the LCLS x-ray free-electron laser (XFEL). In this paper, we demonstrate its high resolution, collection efficiency and spatial selectivity in measurements where it is coupled to an XFEL source. These combined characteristics are designed to enable high-resolution time-resolved measurements using x-ray photoelectron, absorption, and Auger-Meitner spectroscopy. We also describe the pervasive artifact in MBES time-of-flight spectra that arises from a periodic modulation in electron detection efficiency, and present a robust analysis procedure for its removal. △ Less

Submitted 18 June, 2024; originally announced June 2024.

Reasoning about Interior Mutability in Rust using Library-Defined Capabilities

Authors: Federico Poli, Xavier Denis, Peter Müller, Alexander J. Summers

Abstract: Existing automated verification techniques for safe Rust code rely on the strong type-system properties to reason about programs, especially to deduce which memory locations do not change (i.e., are framed) across function calls. However, these type guarantees do not hold in the presence of interior mutability (e.g., when interacting with any concurrent data structure). As a consequence, existing… ▽ More Existing automated verification techniques for safe Rust code rely on the strong type-system properties to reason about programs, especially to deduce which memory locations do not change (i.e., are framed) across function calls. However, these type guarantees do not hold in the presence of interior mutability (e.g., when interacting with any concurrent data structure). As a consequence, existing verification techniques for safe code such as Prusti and Creusot are either unsound or fundamentally incomplete if applied to this setting. In this work, we present the first technique capable of automatically verifying safe clients of existing interiorly mutable types. At the core of our approach, we identify a novel notion of implicit capabilities: library-defined properties that cannot be expressed using Rust's types. We propose new annotations to specify these capabilities and a first-order logic encoding suitable for program verification. We have implemented our technique in a verifier called Mendel and used it to prove absence of panics in Rust programs that make use of popular standard-library types with interior mutability, including Rc, Arc, Cell, RefCell, AtomicI32, Mutex and RwLock. Our evaluation shows that these library annotations are useful for verifying usages of real-world libraries, and powerful enough to require zero client-side annotations in many of the verified programs. △ Less

Submitted 14 May, 2024; originally announced May 2024.

A Formal Model to Prove Instantiation Termination for E-matching-Based Axiomatisations (Extended Version)

Authors: Rui Ge, Ronald Garcia, Alexander J. Summers

Abstract: SMT-based program analysis and verification often involve reasoning about program features that have been specified using quantifiers; incorporating quantifiers into SMT-based reasoning is, however, known to be challenging. If quantifier instantiation is not carefully controlled, then runtime and outcomes can be brittle and hard to predict. In particular, uncontrolled quantifier instantiation can… ▽ More SMT-based program analysis and verification often involve reasoning about program features that have been specified using quantifiers; incorporating quantifiers into SMT-based reasoning is, however, known to be challenging. If quantifier instantiation is not carefully controlled, then runtime and outcomes can be brittle and hard to predict. In particular, uncontrolled quantifier instantiation can lead to unexpected incompleteness and even non-termination. E-matching is the most widely-used approach for controlling quantifier instantiation, but when axiomatisations are complex, even experts cannot tell if their use of E-matching guarantees completeness or termination. This paper presents a new formal model that facilitates the proof, once and for all, that giving a complex E-matching-based axiomatisation to an SMT solver, such as Z3 or cvc5, will not cause non-termination. Key to our technique is an operational semantics for solver behaviour that models how the E-matching rules common to most solvers are used to determine when quantifier instantiations are enabled, but abstracts over irrelevant details of individual solvers. We demonstrate the effectiveness of our technique by presenting a termination proof for a set theory axiomatisation adapted from those used in the Dafny and Viper verifiers. △ Less

Submitted 27 April, 2024; originally announced April 2024.

Comments: extended version of IJCAR 2024 publication

Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language (extended version)

Authors: Gaurav Parthasarathy, Thibault Dardinier, Benjamin Bonneau, Peter Müller, Alexander J. Summers

Abstract: Automated program verifiers are typically implemented using an intermediate verification language (IVL), such as Boogie or Why3. A verifier front-end translates the input program and specification into an IVL program, while the back-end generates proof obligations for the IVL program and employs an SMT solver to discharge them. Soundness of such verifiers therefore requires that the front-end tran… ▽ More Automated program verifiers are typically implemented using an intermediate verification language (IVL), such as Boogie or Why3. A verifier front-end translates the input program and specification into an IVL program, while the back-end generates proof obligations for the IVL program and employs an SMT solver to discharge them. Soundness of such verifiers therefore requires that the front-end translation faithfully captures the semantics of the input program and specification in the IVL program, and that the back-end reports success only if the IVL program is actually correct. For a verification tool to be trustworthy, these soundness conditions must be satisfied by its actual implementation, not just the program logic it uses. In this paper, we present a novel validation methodology that, given a formal semantics for the input language and IVL, provides formal soundness guarantees for front-end implementations. For each run of the verifier, we automatically generate a proof in Isabelle showing that the correctness of the produced IVL program implies the correctness of the input program. This proof can be checked independently from the verifier, in Isabelle, and can be combined with existing work on validating back-ends to obtain an end-to-end soundness result. Our methodology based on forward simulation employs several modularisation strategies to handle the large semantic gap between the input language and the IVL, as well as the intricacies of practical, optimised translations. We present our methodology for the widely-used Viper and Boogie languages. Our evaluation shows that it is effective in validating the translations performed by the existing Viper implementation. △ Less

Submitted 9 May, 2024; v1 submitted 4 April, 2024; originally announced April 2024.

Comments: Extended version of PLDI 2024 publication

Tracking Surface Charge Dynamics on Single Nanoparticles

Authors: Ritika Dagar, Wenbin Zhang, Philipp Rosenberger, Thomas M. Linker, Ana Sousa-Castillo, Marcel Neuhaus, Sambit Mitra, Shubhadeep Biswas, Alexandra Feinberg, Adam M. Summers, Aiichiro Nakano, Priya Vashishta, Fuyuki Shimojo, Jian Wu, Cesar Costa Vera, Stefan A. Maier, Emiliano Cortés, Boris Bergues, Matthias F. Kling

Abstract: Surface charges play a fundamental role in physics and chemistry, particularly in sha** the catalytic properties of nanomaterials. Tracking nanoscale surface charge dynamics remains challenging due to the involved length and time scales. Here, we demonstrate real-time access to the nanoscale charge dynamics on dielectric nanoparticles employing reaction nanoscopy. We present a four-dimensional v… ▽ More Surface charges play a fundamental role in physics and chemistry, particularly in sha** the catalytic properties of nanomaterials. Tracking nanoscale surface charge dynamics remains challenging due to the involved length and time scales. Here, we demonstrate real-time access to the nanoscale charge dynamics on dielectric nanoparticles employing reaction nanoscopy. We present a four-dimensional visualization of the non-linear charge dynamics on strong-field irradiated single SiO$_2$ nanoparticles with femtosecond-nanometer resolution and reveal how surface charges affect surface molecular bonding with quantum dynamical simulations. We performed semi-classical simulations to uncover the roles of diffusion and charge loss in the surface charge redistribution process. Understanding nanoscale surface charge dynamics and its influence on chemical bonding on a single nanoparticle level unlocks an increased ability to address global needs in renewable energy and advanced healthcare. △ Less

Submitted 4 January, 2024; originally announced January 2024.

Comments: 26 pages with (4+6(SI)) figures

Enhanced optical conductivity and many-body effects in strongly-driven photo-excited semi-metallic graphite

Authors: T. P. H. Sidiropoulos, N. Di Palo, D. E. Rivas, A. Summers, S. Severino, M. Reduzzi, J. Biegert

Abstract: The excitation of quasi-particles near the extrema of the electronic band structure is a gateway to electronic phase transitions in condensed matter. In a many-body system, quasi-particle dynamics are strongly influenced by the electronic single-particle structure and have been extensively studied in the weak optical excitation regime. Yet, under strong optical excitation, where light fields coher… ▽ More The excitation of quasi-particles near the extrema of the electronic band structure is a gateway to electronic phase transitions in condensed matter. In a many-body system, quasi-particle dynamics are strongly influenced by the electronic single-particle structure and have been extensively studied in the weak optical excitation regime. Yet, under strong optical excitation, where light fields coherently drive carriers, the dynamics of many-body interactions that can lead to new quantum phases remain largely unresolved. Here, we induce such a highly non-equilibrium many-body state through strong optical excitation of charge carriers near the van Hove singularity in graphite. We investigate the system's evolution into a strongly-driven photo-excited state with attosecond soft X-ray core-level spectroscopy. Surprisingly, we find an enhancement of the optical conductivity of nearly ten times the quantum conductivity and pinpoint it to carrier excitations in flat bands. This interaction regime is robust against carrier-carrier interaction with coherent optical phonons acting as an attractive force reminiscent of superconductivity. The strongly-driven non-equilibrium state is markedly different from the single-particle structure and macroscopic conductivity and is a consequence of the non-adiabatic many-body state. △ Less

Submitted 11 August, 2023; originally announced August 2023.

Resource Specifications for Resource-Manipulating Programs

Authors: Zachary Grannan, Alexander J. Summers

Abstract: Specifications for modular program verifiers are expressed as constraints on program states (e.g. preconditions) and relations on program states (e.g. postconditions). For programs whose domain is managing resources of any kind (e.g. cryptocurrencies), such state-based specifications must make explicit properties that a human would implicitly understand for free. For example, it's clear that depos… ▽ More Specifications for modular program verifiers are expressed as constraints on program states (e.g. preconditions) and relations on program states (e.g. postconditions). For programs whose domain is managing resources of any kind (e.g. cryptocurrencies), such state-based specifications must make explicit properties that a human would implicitly understand for free. For example, it's clear that depositing into your bank account will not change other balances, but classically this must be stated as a frame condition. As a result, classical specifications for resource-manipulating programs quickly become verbose and difficult to interpret, write and debug. In this paper, we present a novel methodology that extends a modular program verifier to support user-defined first-class resources, allowing resource-related operations and properties to be expressed directly and eliminating the need to reify implicit knowledge in the specifications. We implement our methodology as an extension of the program verifier Prusti, and use it to verify real-world smart contracts and a key part of a blockchain application. Our evaluation demonstrates that specifications written with our methodology are more concise and substantially simpler than specifications written purely in terms of program states. △ Less

Submitted 18 April, 2024; v1 submitted 24 April, 2023; originally announced April 2023.

Compositional Reasoning for Side-effectful Iterators and Iterator Adapters

Authors: Aurel Bílý, Jonas Hansen, Peter Müller, Alexander J. Summers

Abstract: Iteration is a programming operation that traditionally refers to visiting the elements of a data structure in sequence. However, modern programming systems such as Rust, Java, and C# generalise iteration far beyond the traditional use case. They allow iterators to be parameterised with (potentially side-effectful) closures and support the composition of iterators to form iterator chains, where ea… ▽ More Iteration is a programming operation that traditionally refers to visiting the elements of a data structure in sequence. However, modern programming systems such as Rust, Java, and C# generalise iteration far beyond the traditional use case. They allow iterators to be parameterised with (potentially side-effectful) closures and support the composition of iterators to form iterator chains, where each iterator in the chain consumes values from its predecessor and produces values for its successor. Such generalisations pose three major challenges for modular specification and verification of iterators and the client code using them: (1) How can parameterised iterators be specified modularly and their (accumulated) side effects reasoned about? (2) How can the behaviour of an iterator chain be derived from the specifications of its component iterators? (3) How can proofs about such iterators be automated? We present the first methodology for the modular specification and verification of advanced iteration idioms with side-effectful computations. It addresses the three challenges above using a combination of inductive two-state invariants, higher-order closure contracts, and separation logic-like ownership. We implement and our methodology in a state-of-the-art SMT-based Rust verifier. Our evaluation shows that our methodology is sufficiently expressive to handle advanced and idiomatic iteration idioms and requires modest annotation overhead. △ Less

Submitted 18 October, 2022; originally announced October 2022.

MSC Class: 68Q60 ACM Class: F.3.1

Non-Adiabatic Electronic and Vibrational Ring-Opening Dynamics resolved with Attosecond Core-Level Spectroscopy

Authors: S. Severino, K. M. Ziems, M. Reduzzi, A. Summers, H. -W. Sun, Y. -H. Chien, S. Gräfe, J. Biegert

Abstract: Non-adiabatic dynamics and conical intersections play a central role in the chemistry of most polyatomic molecules, ranging from isomerization to heterocyclic ring opening and avoided photo-damage of DNA. Studying the underpinning correlated dynamics of electronic and nuclear wave packets is a major challenge in real-time and, many times involves optically dark transient states. We show that attos… ▽ More Non-adiabatic dynamics and conical intersections play a central role in the chemistry of most polyatomic molecules, ranging from isomerization to heterocyclic ring opening and avoided photo-damage of DNA. Studying the underpinning correlated dynamics of electronic and nuclear wave packets is a major challenge in real-time and, many times involves optically dark transient states. We show that attosecond core-level spectroscopy reveals the pathway dynamics of neutral furan across its conical intersections and dark states. Our method measures electronic-nuclear correlations to detect the dephasing of electronic coherence due to nuclear motion and identifies the ring-opened isomer as the dominant product. These results demonstrate the efficacy of attosecond core level spectroscopy as a potent method to investigate the real-time dynamics of photochemical reaction pathways in complex molecular systems. △ Less

Submitted 7 October, 2022; v1 submitted 9 September, 2022; originally announced September 2022.

Establishing the Capabilities of the Murchison Widefield Array as a Passive Radar for the Surveillance of Space

Authors: Brendan Hennessy, Robert Young, Steven Tingay, Ashley Summers, Daniel Gustainis, Brian Crosse, Marcin Sokolowski

Abstract: This paper describes the use of the Murchison Widefield Array, a low-frequency radio telescope at a radio-quiet Western Australian site, as a radar receiver forming part of a continent-spanning multistatic radar network for the surveillance of space. This paper details the system geometry employed, the orbit-specific radar signal processing, and the orbit determination algorithms necessary to ensu… ▽ More This paper describes the use of the Murchison Widefield Array, a low-frequency radio telescope at a radio-quiet Western Australian site, as a radar receiver forming part of a continent-spanning multistatic radar network for the surveillance of space. This paper details the system geometry employed, the orbit-specific radar signal processing, and the orbit determination algorithms necessary to ensure resident space objects are detected, tracked, and propagated. Finally, the paper includes the results processed after a short collection campaign utilising several FM radio transmitters across the country, up to a maximum baseline distance of over 2500 km. The results demonstrate the Murchison Widefield Array is able to provide widefield and persistent coverage of objects in low Earth orbit. △ Less

Submitted 6 June, 2022; originally announced June 2022.

Journal ref: Remote Sensing, 2022, 14(11), 2571

Sound Automation of Magic Wands (extended version)

Authors: Thibault Dardinier, Gaurav Parthasarathy, Noé Weeks, Alexanders J. Summers, Peter Müller

Abstract: The magic wand $\mathbin{-\!\!*}$ (also called separating implication) is a separation logic connective commonly used to specify properties of partial data structures, for instance during iterative traversals. A footprint of a magic wand formula $A \mathbin{-\!\!*} B$ is a state that, combined with any state in which $A$ holds, yields a state in which $B$ holds. The key challenge of proving a magi… ▽ More The magic wand $\mathbin{-\!\!*}$ (also called separating implication) is a separation logic connective commonly used to specify properties of partial data structures, for instance during iterative traversals. A footprint of a magic wand formula $A \mathbin{-\!\!*} B$ is a state that, combined with any state in which $A$ holds, yields a state in which $B$ holds. The key challenge of proving a magic wand (also called packaging a wand) is to find such a footprint. Existing package algorithms either have a high annotation overhead or, as we show in this paper, are unsound. We present a formal framework that precisely characterises a wide design space of possible package algorithms applicable to a large class of separation logics. We prove in Isabelle/HOL that our formal framework is sound and complete, and use it to develop a novel package algorithm that offers competitive automation and is sound. Moreover, we present a novel, restricted definition of wands and prove in Isabelle/HOL that it is possible to soundly combine fractions of such wands, which is not the case for arbitrary wands. We have implemented our techniques for the Viper language, and demonstrate that they are effective in practice. △ Less

Submitted 2 August, 2022; v1 submitted 23 May, 2022; originally announced May 2022.

Comments: Extended version of CAV 2022 publication

REST: Integrating Term Rewriting with Program Verification (Extended Version)

Authors: Zachary Grannan, Niki Vazou, Eva Darulova, Alexander J. Summers

Abstract: We introduce REST, a novel term rewriting technique for theorem proving that uses online termination checking and can be integrated with existing program verifiers. REST enables flexible but terminating term rewriting for theorem proving by: (1) exploiting newly-introduced term orderings that are more permissive than standard rewrite simplification orderings; (2) dynamically and iteratively select… ▽ More We introduce REST, a novel term rewriting technique for theorem proving that uses online termination checking and can be integrated with existing program verifiers. REST enables flexible but terminating term rewriting for theorem proving by: (1) exploiting newly-introduced term orderings that are more permissive than standard rewrite simplification orderings; (2) dynamically and iteratively selecting orderings based on the path of rewrites taken so far; and (3) integrating external oracles that allow steps that cannot be justified with rewrite rules. Our REST approach is designed around an easily implementable core algorithm, parameterizable by choices of term orderings and their implementations; in this way our approach can be easily integrated into existing tools. We implemented REST as a Haskell library and incorporated it into Liquid Haskell's evaluation strategy, extending Liquid Haskell with rewriting rules. We evaluated our REST implementation by comparing it against both existing rewriting techniques and E-matching and by showing that it can be used to supplant manual lemma application in many existing Liquid Haskell proofs. △ Less

Submitted 16 February, 2022; v1 submitted 11 February, 2022; originally announced February 2022.

Few-femtosecond resolved imaging of laser-driven nanoplasma expansion

Authors: C. Peltz, J. A. Powell, P. Rupp, A Summers, T. Gorkhover, M. Gallei, I. Halfpap, E. Antonsson, B. Langer, C. Trallero-Herrero, C. Graf, D. Ray, Q. Liu, T. Osipov, M. Bucher, K. Ferguson, S. Möller, S. Zherebtsov, D. Rolles, E. Rühl, G. Coslovich, R. N. Coffee, C. Bostedt, A. Rudenko, M. F. Kling , et al. (1 additional authors not shown)

Abstract: The free expansion of a planar plasma surface is a fundamental non-equilibrium process relevant for various fields but as-yet experimentally still difficult to capture. The significance of the associated spatiotemporal plasma motion ranges from astrophysics and controlled fusion to laser machining, surface high-harmonic generation, plasma mirrors, and laser-particle acceleration. Here, we show tha… ▽ More The free expansion of a planar plasma surface is a fundamental non-equilibrium process relevant for various fields but as-yet experimentally still difficult to capture. The significance of the associated spatiotemporal plasma motion ranges from astrophysics and controlled fusion to laser machining, surface high-harmonic generation, plasma mirrors, and laser-particle acceleration. Here, we show that x-ray coherent diffractive imaging can surpass existing approaches and enables the quantitative real-time analysis of the sudden free expansion of nanoplasmas. For laser-ionized SiO$_2$ nanospheres, we resolve the formation of the emerging nearly self-similar plasma profile evolution and expose the so far inaccessible shell-wise expansion dynamics including the associated startup delay and rarefaction front velocity. Our results establish time-resolved diffractive imaging as an accurate quantitative diagnostic platform for tracing and characterizing plasma expansion and indicate the possibility to resolve various laser-driven processes including shock formation and wave-breaking phenomena with unprecedented resolution. △ Less

Submitted 15 March, 2022; v1 submitted 20 September, 2021; originally announced September 2021.

Strong-field control of plasmonic properties in core-shell nanoparticles

Authors: Jeffrey Powell, Jianxiong Li, Adam Summers, Seyyed Javad Robatjazi, Michael Davino, Philipp Rupp, Erfan Saydanzad, Christopher M. Sorensen, Daniel Rolles, Matthias F. Kling, Carlos Trallero-Herrero, Uwe Thumm, Artem Rudenko

Abstract: The strong-field control of plasmonic nanosystems opens up new perspectives for nonlinear plasmonic spectroscopy and petahertz electronics. Questions, however, remain regarding the nature of nonlinear light-matter interactions at sub-wavelength spatial and ultrafast temporal scales. Addressing this challenge, we investigated the strong-field control of the plasmonic response of Au nanoshells with… ▽ More The strong-field control of plasmonic nanosystems opens up new perspectives for nonlinear plasmonic spectroscopy and petahertz electronics. Questions, however, remain regarding the nature of nonlinear light-matter interactions at sub-wavelength spatial and ultrafast temporal scales. Addressing this challenge, we investigated the strong-field control of the plasmonic response of Au nanoshells with a SiO$_2$ core to an intense laser pulse. We show that the photoelectron energy spectrum from these core-shell nanoparticles displays a striking transition between the weak and strong-field regime. This observed transition agrees with the prediction of our modified Mie-theory simulation that incorporates the nonlinear dielectric nanoshell response. The demonstrated intensity-dependent optical control of the plasmonic response in prototypical core-shell nanoparticles paves the way towards ultrafast switching and opto-electronic signal modulation with more complex nanostructures. △ Less

Submitted 15 August, 2021; originally announced August 2021.

Formally Validating a Practical Verification Condition Generator (extended version)

Authors: Gaurav Parthasarathy, Peter Müller, Alexander J. Summers

Abstract: A program verifier produces reliable results only if both the logic used to justify the program's correctness is sound, and the implementation of the program verifier is itself correct. Whereas it is common to formally prove soundness of the logic, the implementation of a verifier typically remains unverified. Bugs in verifier implementations may compromise the trustworthiness of successful verifi… ▽ More A program verifier produces reliable results only if both the logic used to justify the program's correctness is sound, and the implementation of the program verifier is itself correct. Whereas it is common to formally prove soundness of the logic, the implementation of a verifier typically remains unverified. Bugs in verifier implementations may compromise the trustworthiness of successful verification results. Since program verifiers used in practice are complex, evolving software systems, it is generally not feasible to formally verify their implementation. In this paper, we present an alternative approach: we validate successful runs of the widely-used Boogie verifier by producing a certificate which proves correctness of the obtained verification result. Boogie performs a complex series of program translations before ultimately generating a verification condition whose validity should imply the correctness of the input program. We show how to certify three of Boogie's core transformation phases: the elimination of cyclic control flow paths, the (SSA-like) replacement of assignments by assumptions using fresh variables (passification), and the final generation of verification conditions. Similar translations are employed by other verifiers. Our implementation produces certificates in Isabelle, based on a novel formalisation of the Boogie language. △ Less

Submitted 29 May, 2021; originally announced May 2021.

Comments: Extended version of CAV 2021 publication

Rich Specifications for Ethereum Smart Contract Verification

Authors: Christian Bräm, Marco Eilers, Peter Müller, Robin Sierra, Alexander J. Summers

Abstract: Smart contracts are programs that execute inside blockchains such as Ethereum to manipulate digital assets. Since bugs in smart contracts may lead to substantial financial losses, there is considerable interest in formally proving their correctness. However, the specification and verification of smart contracts faces challenges that do not arise in other application domains. Smart contracts freque… ▽ More Smart contracts are programs that execute inside blockchains such as Ethereum to manipulate digital assets. Since bugs in smart contracts may lead to substantial financial losses, there is considerable interest in formally proving their correctness. However, the specification and verification of smart contracts faces challenges that do not arise in other application domains. Smart contracts frequently interact with unverified, potentially adversarial outside code, which substantially weakens the assumptions that formal analyses can (soundly) make. Moreover, the core functionality of smart contracts is to manipulate and transfer resources; describing this functionality concisely requires dedicated specification support. Current reasoning techniques do not fully address these challenges, being restricted in their scope or expressiveness (in particular, in the presence of re-entrant calls), and offering limited means of expressing the resource transfers a contract performs. In this paper, we present a novel specification methodology tailored to the domain of smart contracts. Our specification constructs and associated reasoning technique are the first to enable: (1) sound and precise reasoning in the presence of unverified code and arbitrary re-entrancy, (2) modular reasoning about collaborating smart contracts, and (3) domain-specific specifications based on resources and resource transfers, which allow expressing a contract's behavior in intuitive and concise ways and exclude typical errors by default. We have implemented our approach in 2vyper, an SMT-based automated verification tool for Ethereum smart contracts written in the Vyper language, and demonstrated its effectiveness in succinctly capturing and verifying strong correctness guarantees for real-world contracts. △ Less

Submitted 9 September, 2021; v1 submitted 20 April, 2021; originally announced April 2021.

Higher order harmonic generation and strong field ionization with Bessel-Gauss beams in a thin jet geometry

Authors: Michael Davino, Adam Summers, Tobias Saule, Jan Tross, Edward McManus, Brandin Davis, Carlos A. Trallero-Herrero

Abstract: A promising alternative to Gaussian beams for use in strong field science is Bessel-Gauss (BG or Bessel-like) laser beams as they are easily produced with readily available optics and provide more flexibility of the spot size and working distances. Here we use BG beams produced with a lens-axicon optical system for higher order harmonic generation (HHG) in a thin gas jet. The finite size of the in… ▽ More A promising alternative to Gaussian beams for use in strong field science is Bessel-Gauss (BG or Bessel-like) laser beams as they are easily produced with readily available optics and provide more flexibility of the spot size and working distances. Here we use BG beams produced with a lens-axicon optical system for higher order harmonic generation (HHG) in a thin gas jet. The finite size of the interaction region allows for scans of the HHG yield along the propagation axis. Further, by measuring the ionization yield in unison with the extreme ultraviolet (XUV) we are able to distinguish regions of maximum ionization from regions of optimum XUV generation. This distinction is of great importance for BG fields as the generation of BG beams with axicons often leads to oscillations of the on-axis intensity, which can be exploited for extended phase matching conditions. We observed such oscillations in the ionization and XUV flux along the propagation axis for the first time. As it is the case for Gaussian modes, the harmonic yield is not maximum at the point of highest ionization. Finally, despite Bessel beams having a hole in the center in the far field, the XUV beam is well collimated making BG modes a great alternative when spatial filtering of the fundamental is desired. △ Less

Submitted 10 February, 2021; originally announced February 2021.

Comments: Submitted to JOSA B, 8 pages, 4 figures

Unraveling Ultrafast Photoionization in Hexagonal Boron Nitride

Authors: Lianjie Xue, Song Liu, Yang Hang, Adam M. Summers, Derrek J. Wilson, Xinya Wang, **** Chen, Thomas G. Folland, Jordan A. Hachtel, Hongyu Shi, Sajed Hosseini-Zavareh, Suprem R. Das, Shuting Lei, Zhuhua Zhang, Christopher M. Sorensen, Wanlin Guo, Joshua D. Caldwell, James H. Edgar, Cosmin I. Blaga, Carlos A. Trallero-Herrero

Abstract: The non-linear response of dielectrics to intense, ultrashort electric fields has been a sustained topic of interest for decades with one of its most important applications being femtosecond laser micro/nano-machining. More recently, renewed interests in strong field physics of solids were raised with the advent of mid-infrared femtosecond laser pulses, such as high-order harmonic generation, opti… ▽ More The non-linear response of dielectrics to intense, ultrashort electric fields has been a sustained topic of interest for decades with one of its most important applications being femtosecond laser micro/nano-machining. More recently, renewed interests in strong field physics of solids were raised with the advent of mid-infrared femtosecond laser pulses, such as high-order harmonic generation, optical-field-induced currents, etc. All these processes are underpinned by photoionization (PI), namely the electron transfer from the valence to the conduction bands, on a time scale too short for phononic motion to be of relevance. Here, in hexagonal boron nitride, we reveal that the bandgap can be finely manipulated by femtosecond laser pulses as a function of field polarization direction with respect to the lattice, in addition to the field's intensity. It is the modification of bandgap that enables the ultrafast PI processes to take place in dielectrics. We further demonstrate the validity of the Keldysh theory in describing PI in dielectrics in the few TW/cm2 regime. △ Less

Submitted 26 January, 2021; v1 submitted 25 January, 2021; originally announced January 2021.

Comments: 13 pages, 4 figures

Machine Learning and Meta-Analysis Approach to Identify Patient Comorbidities and Symptoms that Increased Risk of Mortality in COVID-19

Authors: Sakifa Aktar, Ashis Talukder, Md. Martuza Ahamad, A. H. M. Kamal, Jahidur Rahman Khan, Md. Protikuzzaman, Nasif Hossain, Julian M. W. Quinn, Mathew A. Summers, Teng Liaw, Valsamma Eapen, Mohammad Ali Moni

Abstract: Background: Providing appropriate care for people suffering from COVID-19, the disease caused by the pandemic SARS-CoV-2 virus is a significant global challenge. Many individuals who become infected have pre-existing conditions that may interact with COVID-19 to increase symptom severity and mortality risk. COVID-19 patient comorbidities are likely to be informative about individual risk of severe… ▽ More Background: Providing appropriate care for people suffering from COVID-19, the disease caused by the pandemic SARS-CoV-2 virus is a significant global challenge. Many individuals who become infected have pre-existing conditions that may interact with COVID-19 to increase symptom severity and mortality risk. COVID-19 patient comorbidities are likely to be informative about individual risk of severe illness and mortality. Accurately determining how comorbidities are associated with severe symptoms and mortality would thus greatly assist in COVID-19 care planning and provision. Methods: To assess the interaction of patient comorbidities with COVID-19 severity and mortality we performed a meta-analysis of the published global literature, and machine learning predictive analysis using an aggregated COVID-19 global dataset. Results: Our meta-analysis identified chronic obstructive pulmonary disease (COPD), cerebrovascular disease (CEVD), cardiovascular disease (CVD), type 2 diabetes, malignancy, and hypertension as most significantly associated with COVID-19 severity in the current published literature. Machine learning classification using novel aggregated cohort data similarly found COPD, CVD, CKD, type 2 diabetes, malignancy and hypertension, as well as asthma, as the most significant features for classifying those deceased versus those who survived COVID-19. While age and gender were the most significant predictor of mortality, in terms of symptom-comorbidity combinations, it was observed that Pneumonia-Hypertension, Pneumonia-Diabetes and Acute Respiratory Distress Syndrome (ARDS)-Hypertension showed the most significant effects on COVID-19 mortality. Conclusions: These results highlight patient cohorts most at risk of COVID-19 related severe morbidity and mortality which have implications for prioritization of hospital resources. △ Less

Submitted 21 August, 2020; originally announced August 2020.

Report number: 2008.12683

Journal ref: Diagnostics 2021

Local Reasoning for Global Graph Properties

Authors: Siddharth Krishna, Alexander J. Summers, Thomas Wies

Abstract: Separation logics are widely used for verifying programs that manipulate complex heap-based data structures. These logics build on so-called separation algebras, which allow expressing properties of heap regions such that modifications to a region do not invalidate properties stated about the remainder of the heap. This concept is key to enabling modular reasoning and also extends to concurrency.… ▽ More Separation logics are widely used for verifying programs that manipulate complex heap-based data structures. These logics build on so-called separation algebras, which allow expressing properties of heap regions such that modifications to a region do not invalidate properties stated about the remainder of the heap. This concept is key to enabling modular reasoning and also extends to concurrency. While heaps are naturally related to mathematical graphs, many ubiquitous graph properties are non-local in character, such as reachability between nodes, path lengths, acyclicity and other structural invariants, as well as data invariants which combine with these notions. Reasoning modularly about such graph properties remains notoriously difficult, since a local modification can have side-effects on a global property that cannot be easily confined to a small region. In this paper, we address the question: What separation algebra can be used to avoid proof arguments reverting back to tedious global reasoning in such cases? To this end, we consider a general class of global graph properties expressed as fixpoints of algebraic equations over graphs. We present mathematical foundations for reasoning about this class of properties, imposing minimal requirements on the underlying theory that allow us to define a suitable separation algebra. Building on this theory we develop a general proof technique for modular reasoning about global graph properties over program heaps, in a way which can be integrated with existing separation logics. To demonstrate our approach, we present local proofs for two challenging examples: a priority inheritance protocol and the non-blocking concurrent Harris list. △ Less

Submitted 19 November, 2019; originally announced November 2019.

Modular Verification of Heap Reachability Properties in Separation Logic

Authors: Arshavir Ter-Gabrielyan, Alexander J. Summers, Peter Müller

Abstract: The correctness of many algorithms and data structures depends on reachability properties, that is, on the existence of chains of references between objects in the heap. Reasoning about reachability is difficult for two main reasons. First, any heap modification may affect an unbounded number of reference chains, which complicates modular verification, in particular, framing. Second, general graph… ▽ More The correctness of many algorithms and data structures depends on reachability properties, that is, on the existence of chains of references between objects in the heap. Reasoning about reachability is difficult for two main reasons. First, any heap modification may affect an unbounded number of reference chains, which complicates modular verification, in particular, framing. Second, general graph reachability is not supported by SMT solvers, which impedes automatic verification. In this paper, we present a modular specification and verification technique for reachability properties in separation logic. For each method, we specify reachability only locally within the fragment of the heap on which the method operates. A novel form of reachability framing for relatively convex subheaps allows one to extend reachability properties from the heap fragment of a callee to the larger fragment of its caller, enabling precise procedure-modular reasoning. Our technique supports practically important heap structures, namely acyclic graphs with a bounded outdegree as well as (potentially cyclic) graphs with at most one path (modulo cycles) between each pair of nodes. The integration into separation logic allows us to reason about reachability and other properties in a uniform way, to verify concurrent programs, and to automate our technique via existing separation logic verifiers. We demonstrate that our verification technique is amenable to SMT-based verification by encoding a number of benchmark examples into the Viper verification infrastructure. △ Less

Submitted 15 August, 2019; originally announced August 2019.

Comments: OOPSLA-2019

Interplay of pulse duration, peak intensity, and particle size in laser-driven electron emission from silica nanospheres

Authors: Jeffrey A. Powell, Adam M. Summers, Qingcao Liu, Seyyed Javad Robatjazi, Philipp Rupp, Johannes Stierle, Carlos A. Trallero-herrero, Matthias F. Kling, Artem Rudenko

Abstract: We present the results of a systematic study of photoelectron emission from gasphase dielectric nanoparticles (SiO2) irradiated by intense 25 fs, 780 nm linearly polarized laser pulses as a function of particle size (20 nm to 750 nm in diameter) and laser intensity. We also introduce an experimental technique to reduce the effects of focal volume averaging. The highest photoelectron energies show… ▽ More We present the results of a systematic study of photoelectron emission from gasphase dielectric nanoparticles (SiO2) irradiated by intense 25 fs, 780 nm linearly polarized laser pulses as a function of particle size (20 nm to 750 nm in diameter) and laser intensity. We also introduce an experimental technique to reduce the effects of focal volume averaging. The highest photoelectron energies show a strong size dependence, increasing by a factor of six over the range of particles sizes studied at a fixed intensity. For smaller particle sizes (up to 200 nm), our findings agree well with earlier results obtained with few-cycle, ~4 fs pulses. For large nanoparticles, which exhibit stronger near-field localization due to field-propagation effects, we observe the emission of much more energetic electrons, reaching energies up to ~200 times the ponderomotive energy. This strong deviation in maximum photoelectron energy is attributed to the increase in ionization and charge interaction for many-cycle pulses at similar intensities. △ Less

Submitted 22 July, 2019; originally announced July 2019.

Comments: 14 pages, 5 figures

Unwind: Interactive Fish Straightening

Authors: Francis Williams, Alexander Bock, Harish Doraiswamy, Cassandra Donatelli, Kayla Hall, Adam Summers, Daniele Panozzo, Cláudio T. Silva

Abstract: The ScanAllFish project is a large-scale effort to scan all the world's 33,100 known species of fishes. It has already generated thousands of volumetric CT scans of fish species which are available on open access platforms such as the Open Science Framework. To achieve a scanning rate required for a project of this magnitude, many specimens are grouped together into a single tube and scanned all a… ▽ More The ScanAllFish project is a large-scale effort to scan all the world's 33,100 known species of fishes. It has already generated thousands of volumetric CT scans of fish species which are available on open access platforms such as the Open Science Framework. To achieve a scanning rate required for a project of this magnitude, many specimens are grouped together into a single tube and scanned all at once. The resulting data contain many fish which are often bent and twisted to fit into the scanner. Our system, Unwind, is a novel interactive visualization and processing tool which extracts, unbends, and untwists volumetric images of fish with minimal user interaction. Our approach enables scientists to interactively unwarp these volumes to remove the undesired torque and bending using a piecewise-linear skeleton extracted by averaging isosurfaces of a harmonic function connecting the head and tail of each fish. The result is a volumetric dataset of a individual, straight fish in a canonical pose defined by the marine biologist expert user. We have developed Unwind in collaboration with a team of marine biologists: Our system has been deployed in their labs, and is presently being used for dataset construction, biomechanical analysis, and the generation of figures for scientific publication. △ Less

Submitted 5 February, 2020; v1 submitted 9 April, 2019; originally announced April 2019.

Formalizing Atom-ty** and the Dissemination of Force Fields with Foyer

Authors: Christoph Klein, Andrew Z. Summers, Matthew W. Thompson, Justin Gilmer, Clare McCabe, Peter T. Cummings, Janos Sallai, Christopher R. Iacovella

Abstract: A key component to enhancing reproducibility in the molecular simulation community is reducing ambiguity in the parameterization of molecular models. Ambiguity in molecular models often stems from the dissemination of molecular force fields in a format that is not directly usable or is ambiguously documented via a non-machine readable mechanism. Specifically, the lack of a general tool for perform… ▽ More A key component to enhancing reproducibility in the molecular simulation community is reducing ambiguity in the parameterization of molecular models. Ambiguity in molecular models often stems from the dissemination of molecular force fields in a format that is not directly usable or is ambiguously documented via a non-machine readable mechanism. Specifically, the lack of a general tool for performing automated atom-ty** under the rules of a particular force field facilitates errors in model parameterization that may go unnoticed if other researchers are unable reproduce this process. Here, we present Foyer, a Python tool that enables users to define force field atom-ty** rules in a format that is both machine- and human-readable thus eliminating ambiguity in atom-ty** and additionally providing a framework for force field dissemination. Foyer defines force fields in an XML format, where SMARTS strings are used to define the chemical context of a particular atom type. Herein we describe the underlying methodology of the Foyer package, highlighting its advantages over typical atom-ty** approaches and demonstrate is application in several use-cases. △ Less

Submitted 7 December, 2018; originally announced December 2018.

Comments: 39 Page, 4 Figures, 8 Listings

Permission Inference for Array Programs

Authors: Jérôme Dohrau, Alexander J. Summers, Caterina Urban, Severin Münger, Peter Müller

Abstract: Information about the memory locations accessed by a program is, for instance, required for program parallelisation and program verification. Existing inference techniques for this information provide only partial solutions for the important class of array-manipulating programs. In this paper, we present a static analysis that infers the memory footprint of an array program in terms of permission… ▽ More Information about the memory locations accessed by a program is, for instance, required for program parallelisation and program verification. Existing inference techniques for this information provide only partial solutions for the important class of array-manipulating programs. In this paper, we present a static analysis that infers the memory footprint of an array program in terms of permission pre- and postconditions as used, for example, in separation logic. This formulation allows our analysis to handle concurrent programs and produces specifications that can be used by verification tools. Our analysis expresses the permissions required by a loop via maximum expressions over the individual loop iterations. These maximum expressions are then solved by a novel maximum elimination algorithm, in the spirit of quantifier elimination. Our approach is sound and is implemented; an evaluation on existing benchmarks for memory safety of array programs demonstrates accurate results, even for programs with complex access patterns and nested loops. △ Less

Submitted 11 April, 2018; originally announced April 2018.

Automating Deductive Verification for Weak-Memory Programs

Authors: Alexander J. Summers, Peter Müller

Abstract: Writing correct programs for weak memory models such as the C11 memory model is challenging because of the weak consistency guarantees these models provide. The first program logics for the verification of such programs have recently been proposed, but their usage has been limited thus far to manual proofs. Automating proofs in these logics via first-order solvers is non-trivial, due to reasoning… ▽ More Writing correct programs for weak memory models such as the C11 memory model is challenging because of the weak consistency guarantees these models provide. The first program logics for the verification of such programs have recently been proposed, but their usage has been limited thus far to manual proofs. Automating proofs in these logics via first-order solvers is non-trivial, due to reasoning features such as higher-order assertions, modalities and rich permission resources. In this paper, we provide the first implementation of a weak memory program logic using existing deductive verification tools. We tackle three recent program logics: Relaxed Separation Logic and two forms of Fenced Separation Logic, and show how these can be encoded using the Viper verification infrastructure. In doing so, we illustrate several novel encoding techniques which could be employed for other logics. Our work is implemented, and has been evaluated on examples from existing papers as well as the Facebook open-source Folly library. △ Less

Submitted 19 February, 2018; v1 submitted 18 March, 2017; originally announced March 2017.

Comments: Extended version of TACAS 2018 publication

MSC Class: 68N30 ACM Class: D.2.4; F.3.1

Automatic Verification of Iterated Separating Conjunctions using Symbolic Execution

Authors: Peter Müller, Malte Schwerhoff, Alexander J. Summers

Abstract: In permission logics such as separation logic, the iterated separating conjunction is a quantifier denoting access permission to an unbounded set of heap locations. In contrast to recursive predicates, iterated separating conjunctions do not prescribe a structure on the locations they range over, and so do not restrict how to traverse and modify these locations. This flexibility is important for t… ▽ More In permission logics such as separation logic, the iterated separating conjunction is a quantifier denoting access permission to an unbounded set of heap locations. In contrast to recursive predicates, iterated separating conjunctions do not prescribe a structure on the locations they range over, and so do not restrict how to traverse and modify these locations. This flexibility is important for the verification of random-access data structures such as arrays and data structures that can be traversed in multiple ways such as graphs. Despite its usefulness, no automatic program verifier natively supports iterated separating conjunctions; they are especially difficult to incorporate into symbolic execution engines, the prevalent technique for building verifiers for these logics. In this paper, we present the first symbolic execution technique to support general iterated separating conjunctions. We propose a novel representation of symbolic heaps and flexible support for logical specifications that quantify over heap locations. Our technique exhibits predictable and fast performance despite employing quantifiers at the SMT level, by carefully controlling quantifier instantiations. It is compatible with other features of permission logics such as fractional permissions, recursive predicates, and abstraction functions. Our technique is implemented as an extension of the Viper verification infrastructure. △ Less

Submitted 6 May, 2016; v1 submitted 2 March, 2016; originally announced March 2016.

ACM Class: F.3.1

Optical damage threshold of Au nanowires in strong femtosecond laser fields

Authors: A. M. Summers, A. S. Ramm, Govind Paneru, M. F. Kling, B. N. Flanders, C. A. Trallero-Herrero

Abstract: Ultrashort, intense light pulses permit the study of nanomaterials in the optical non-linear regime, potentially leading to optoelectronics that operate in the petahertz domain. These non-linear regimes are often present just below the damage threshold thus requiring the careful tuning of laser parameters to avoid the melting and disintegration of the materials. Detailed studies of the damage thre… ▽ More Ultrashort, intense light pulses permit the study of nanomaterials in the optical non-linear regime, potentially leading to optoelectronics that operate in the petahertz domain. These non-linear regimes are often present just below the damage threshold thus requiring the careful tuning of laser parameters to avoid the melting and disintegration of the materials. Detailed studies of the damage threshold of nanoscale materials are therefore needed. We present results on the damage threshold of Au nanowires when illuminated by intense femtosecond pulses. These nanowires were synthesized with the directed electrochemical nanowire assembly (DENA) process in two configurations: (1) free-standing Au nanowires on W electrodes and (2) Au nanowires attached to fused silica slides. In both cases the wires have a single-crystalline structure. For laser pulses with durations of 108 fs and 32 fs at 790 nm at a repetition rate of 2 kHz, we find that the free-standing nanowires melt at intensities close to 3 TW/cm$^2$ and 7.5 TW/cm$^2$, respectively. The Au nanowires attached to silica slides melt at slightly higher intensities, just above 10 TW/cm$^2$ for 32 fs pulses. Our results can be explained with an electron-phonon interaction model that describes the absorbed laser energy and subsequent heat conduction across the wire. △ Less

Submitted 13 December, 2013; v1 submitted 11 December, 2013; originally announced December 2013.

Comments: 12 pages 6 figures, Submitted to Optics Express

The Relationship Between Separation Logic and Implicit Dynamic Frames

Authors: Matthew J. Parkinson, Alexander J. Summers

Abstract: Separation logic is a concise method for specifying programs that manipulate dynamically allocated storage. Partially inspired by separation logic, Implicit Dynamic Frames has recently been proposed, aiming at first-order tool support. In this paper, we precisely connect the semantics of these two logics. We define a logic whose syntax subsumes both that of a standard separation logic, and that o… ▽ More Separation logic is a concise method for specifying programs that manipulate dynamically allocated storage. Partially inspired by separation logic, Implicit Dynamic Frames has recently been proposed, aiming at first-order tool support. In this paper, we precisely connect the semantics of these two logics. We define a logic whose syntax subsumes both that of a standard separation logic, and that of implicit dynamic frames as sub-syntaxes. We define a total heap semantics for our logic, and, for the separation logic subsyntax, prove it equivalent the standard partial heaps model. In order to define a semantics which works uniformly for both subsyntaxes, we define the novel concept of a minimal state extension, which provides a different (but equivalent) definition of the semantics of separation logic implication and magic wand connectives, while also giving a suitable semantics for these connectives in implicit dynamic frames. We show that our resulting semantics agrees with the existing definition of weakest pre-condition semantics for the implicit dynamic frames fragment. Finally, we show that we can encode the separation logic fragment of our logic into the implicit dynamic frames fragment, preserving semantics. For the connectives typically supported by tools, this shows that separation logic can be faithfully encoded in a first-order automatic verification tool (Chalice). △ Less

Submitted 29 July, 2012; v1 submitted 30 March, 2012; originally announced March 2012.

ACM Class: F.3.1

Journal ref: Logical Methods in Computer Science, Volume 8, Issue 3 (July 31, 2012) lmcs:802

The Suzaku View of the Disk-Jet Connection in the Low Excitation Radio Galaxy NGC 6251

Authors: D. A. Evans, A. C. Summers, M. J. Hardcastle, R. P. Kraft, P. Gandhi, J. H. Croston, J. C. Lee

Abstract: We present results from an 87-ks Suzaku observation of the canonical low-excitation radio galaxy (LERG) NGC 6251. We have previously suggested that LERGs violate conventional AGN unification schemes: they may lack an obscuring torus and are likely to accrete in a radiatively inefficient manner, with almost all of the energy released by the accretion process being channeled into powerful jets. We m… ▽ More We present results from an 87-ks Suzaku observation of the canonical low-excitation radio galaxy (LERG) NGC 6251. We have previously suggested that LERGs violate conventional AGN unification schemes: they may lack an obscuring torus and are likely to accrete in a radiatively inefficient manner, with almost all of the energy released by the accretion process being channeled into powerful jets. We model the 0.5-20 keV Suzaku spectrum with a single power law of photon index $Γ=1.82^{+0.04}_{-0.05}$, together with two collisionally ionized plasma models whose parameters are consistent with the known galaxy- and group-scale thermal emission. Our observations confirm that there are no signatures of obscured, accretion-related X-ray emission in NGC 6251, and we show that the luminosity of any such component must be substantially sub-Eddington in nature. △ Less

Submitted 29 September, 2011; originally announced September 2011.

Comments: 5 pages, 3 figures, 2 tables. Accepted for publication in ApJ Letters