Anish Tondwalkar

Photo of Anish Tondwalkar

I am a PhD Student in Computer Science in the Jacobs School of Engineering at UC San Diego. My advisor is Ranjit Jhala. Previously, I graduated with an M.S. in Computer Science from UVa, where I worked with Wes Weimer.

You can reach me at


I’m interested in the organization of information, the processing of information, and the organization of processing of information—both by the universe in general and humans in particular. In practice this means:

Current Projects:


Finding Bugs in Liquid Haskell

UVa+UCSD Computer Science

Dependent types provide strong guarantees but can be hard to program, admitting mistakes in the implementation as well as the specification. We present algorithms for resolving verification failures by both finding bugs in implementations and also completing annotations in the Liquid Haskell refinement type framework. We present a fault localization algorithm for finding likely bug locations when verification failure stems from a bug in the implementation. We use the type checker as an oracle to search for a set of minimal unsatisfiable type constraints that map to possible bug locations. Conversely, we present an algorithm based on Craig interpolation to discover predicates that allow the type checker to verify programs that would otherwise be deemed unsafe due to inadequate type annotations. We evaluate our algorithms on an indicative benchmark of Haskell programs with Liquid Haskell type annotations. Our fault localization algorithm localizes more bugs than the vanilla Liquid Haskell type checker while still returning a small number of false positives. Our predicate discovery algorithm infers refinements types for large classes of benchmark programs, including all those that admit bounded constraint unrolling. In addition, the design of our algorithms allows them to be effectively extended to other typing systems. [PDF]

Quasinormal Mode Frequencies of AdS-Ressiner-Nördstrom Black Holes

UVa Physics

We investigate quasinormal mode frequencies ωn of the Dirac equation in a Reissner-Nördstrom-AdSD background in space-time dimension D > 3, in the black brane (large black hole) limit. By asymptotic, we mean large overtone number n with everything else held fixed.


Naval Research Lab

The Naval Research Laboratory is conducting an interdisciplinary physics-based Space Weather model development and validation program called the Integrated Sun-Earth System for the Operational Environment (ISES-OE).

In contrast to other geospace integration efforts, a key aspect of ISES is determining the extent to which current models capture the climate of the ionosphere and thermosphere. Until now, complementary long-term simulations using physics-based ionosphere models have not been performed. As part of this program, numerous runs of the physics-based SAMI3 model have been made and compared to global measurements of electron density. The data sets includes Ionosonde NmF2 and hmF2 measurements, GPS Total Electron Content (TEC) measurements and others.

Several modifications to SAMI3 were incorporated including updates to the Solar EUV fluxes, the NRL MSIS neutral atmospheric model parameterization at Solar Minimum and compensating for variations in the Sun-to-Earth distance. Data and model comparisons during times of higher solar activity will be presented with an emphasis on understanding the effects of coupling of the neutral atmosphere, neutral winds and driving electric fields on our ability to model the measured global electron density data. We examine responses to solar EUV radiation and geomagnetic activity, and semiannual and annual oscillations that all induce geospace variability.


Naval Research Lab

Plasma lines excited by a powerful, high-frequency (HF) radio wave are studied using data obtained with an ultrahigh frequency (UHF) radar at HAARP (High Frequency Active Auroral Research Program). Of particular interest is persistent enhancement of the radar backscatter power during HF on at several HF frequencies.

The persistent enhancement is induced with the HF frequency slightly lower than foF2 by a few hundred kHz; by contrast the persistent enhancement does not appear when the HF frequency is equal to and higher than foF2 or lower than foF2 by more than 500 kHz. When persistent enhancements of the radar backscatter power appear, two case studies show that the local plasma frequency at the reflection height of the O-mode polarization wave is close to the second or third electron gyroharmonic frequencies, but one case study shows that the local plasma frequency at the reflection height is significantly different from the third electron gyroharmonic frequency.


Naval Research Lab

A microwave driven resonator is as an electron/ion cloud generator for illumination and plasma source applications. A sustained porous cavity resonator (PCR) glow discharge is externally excited using a resonant frequency electromagnetic (EM) wave that excites large internal electric fields. The resonator amplifies the incident electric field by factors of about 100 causing a breakdown of the neutral gas inside the sphere. A glowing plasma ball is sustained around the point where the maximum electric fields exceed the plasma-discharge threshold for the low-pressure gas inside the resonator. After the EM pump field is removed, the plasma light source is rapidly quenched. The externally driven spherical PCR was fabricated from a theoretical design of the PCR for a laboratory demonstration of the plasma ball generation system. Using both theory and experiment, basic research has been applied to understand:

  1. the EMs of resonator excitation and amplification
  2. the generation of light by glow radio frequency discharge
  3. the effect of background neutral density of the size and intensity of the glowing plasma clouds.

For this study, plasma resonators were constructed for the spherical TM101 and TE101 modes and a TE011 circular-cylindrical cavity. All PCR structures provide the ability to confine a plasma into a desired spatial shape without magnetic fields.