Anish Tondwalkar [cv]

Photo of Anish Tondwalkar

Department Of Computer Science
University of Virgina
Office: Rice 434-8
Email: lastname@virginia.edu

I am a com­bined BS/MS Stu­dent of Com­put­er Sci­ence in the School of En­gi­neer­ing at the Uni­ver­si­ty of Vir­ginia. My ad­vi­sor is Wes Weimer. I also work with Ran­jit Jha­la at UCSD and Pe­ter Arnold at UVa.

Research

I’m in­ter­est­ed in the or­ga­ni­za­tion of in­for­ma­tion, the pro­cess­ing of in­for­ma­tion, and the or­ga­ni­za­tion of pro­cess­ing of in­for­ma­tion—both by the uni­verse in gen­er­al and hu­mans in par­tic­u­lar. In prac­tice this means:

Cur­rent Projects:

Projects

Find­ing Bugs in Liq­uid Haskell

UVa+UCSD Com­put­er Sci­ence

De­pen­dent types pro­vide strong guar­an­tees but can be hard to pro­gram, ad­mit­ting mis­takes in the im­ple­men­ta­tion as well as the spec­i­fi­ca­tion. We present al­go­rithms for re­solv­ing ver­i­fi­ca­tion fail­ures by both find­ing bugs in im­ple­men­ta­tions and also com­plet­ing an­no­ta­tions in the Liq­uid Haskell re­fine­ment type frame­work. We present a fault lo­cal­iza­tion al­go­rithm for find­ing like­ly bug lo­ca­tions when ver­i­fi­ca­tion fail­ure stems from a bug in the im­ple­men­ta­tion. We use the type check­er as an or­a­cle to search for a set of min­i­mal un­sat­is­fi­able type con­straints that map to pos­si­ble bug lo­ca­tions. Con­verse­ly, we present an al­go­rithm based on Craig in­ter­po­la­tion to dis­cov­er pred­i­cates that al­low the type check­er to ver­i­fy pro­grams that would oth­er­wise be deemed un­safe due to in­ad­e­quate type an­no­ta­tions. We eval­u­ate our al­go­rithms on an in­dica­tive bench­mark of Haskell pro­grams with Liq­uid Haskell type an­no­ta­tions. Our fault lo­cal­iza­tion al­go­rithm lo­cal­izes more bugs than the vanil­la Liq­uid Haskell type check­er while still re­turn­ing a small num­ber of false pos­i­tives. Our pred­i­cate dis­cov­ery al­go­rithm in­fers re­fine­ments types for large class­es of bench­mark pro­grams, in­clud­ing all those that ad­mit bound­ed con­straint un­rolling. In ad­di­tion, the de­sign of our al­go­rithms al­lows them to be ef­fec­tive­ly ex­tend­ed to oth­er typ­ing sys­tems. [PDF]

Qua­si­nor­mal Mode Fre­quen­cies of AdS-Ressin­er-Nörd­strom Black Holes

UVa Physics

We in­ves­ti­gate qua­si­nor­mal mode fre­quen­cies ωn of the Dirac equa­tion in a Reiss­ner-Nörd­strom-AdSD back­ground in space-time di­men­sion D > 3, in the black brane (large black hole) lim­it. By as­ymp­tot­ic, we mean large over­tone num­ber n with every­thing else held fixed. [write­up in progress]

SAMI

Naval Re­search Lab

The Naval Re­search Lab­o­ra­to­ry is con­duct­ing an in­ter­dis­ci­pli­nary physics-based Space Weath­er mod­el de­vel­op­ment and val­i­da­tion pro­gram called the In­te­grat­ed Sun-Earth Sys­tem for the Op­er­a­tional En­vi­ron­ment (ISES-OE).

In con­trast to oth­er geo­space in­te­gra­tion ef­forts, a key as­pect of ISES is de­ter­min­ing the ex­tent to which cur­rent mod­els cap­ture the cli­mate of the ionos­phere and ther­mos­phere. Un­til now, com­ple­men­tary long-term sim­u­la­tions us­ing physics-based ionos­phere mod­els have not been per­formed. As part of this pro­gram, nu­mer­ous runs of the physics-based SAMI3 mod­el have been made and com­pared to glob­al mea­sure­ments of elec­tron den­si­ty. The data sets in­cludes Ionosonde NmF2 and hmF2 mea­sure­ments, GPS To­tal Elec­tron Con­tent (TEC) mea­sure­ments and oth­ers.

Sev­er­al mod­i­fi­ca­tions to SAMI3 were in­cor­po­rat­ed in­clud­ing up­dates to the So­lar EUV flux­es, the NRL MSIS neu­tral at­mos­pher­ic mod­el pa­ra­me­ter­i­za­tion at So­lar Min­i­mum and com­pen­sat­ing for vari­a­tions in the Sun-to-Earth dis­tance. Data and mod­el com­par­isons dur­ing times of high­er so­lar ac­tiv­i­ty will be pre­sent­ed with an em­pha­sis on un­der­stand­ing the ef­fects of cou­pling of the neu­tral at­mos­phere, neu­tral winds and dri­ving elec­tric fields on our abil­i­ty to mod­el the mea­sured glob­al elec­tron den­si­ty data. We ex­am­ine re­spons­es to so­lar EUV ra­di­a­tion and ge­o­mag­net­ic ac­tiv­i­ty, and semi­an­nu­al and an­nu­al os­cil­la­tions that all in­duce geo­space vari­abil­i­ty.

HAARP

Naval Re­search Lab

Plas­ma lines ex­cit­ed by a pow­er­ful, high-fre­quen­cy (HF) ra­dio wave are stud­ied us­ing data ob­tained with an ul­tra­high fre­quen­cy (UHF) radar at HAARP (High Fre­quen­cy Ac­tive Au­ro­ral Re­search Pro­gram). Of par­tic­u­lar in­ter­est is per­sis­tent en­hance­ment of the radar backscat­ter pow­er dur­ing HF on at sev­er­al HF fre­quen­cies.

The per­sis­tent en­hance­ment is in­duced with the HF fre­quen­cy slight­ly low­er than foF2 by a few hun­dred kHz; by con­trast the per­sis­tent en­hance­ment does not ap­pear when the HF fre­quen­cy is equal to and high­er than foF2 or low­er than foF2 by more than 500 kHz. When per­sis­tent en­hance­ments of the radar backscat­ter pow­er ap­pear, two case stud­ies show that the lo­cal plas­ma fre­quen­cy at the re­flec­tion height of the O-mode po­lar­iza­tion wave is close to the sec­ond or third elec­tron gy­ro­har­mon­ic fre­quen­cies, but one case study shows that the lo­cal plas­ma fre­quen­cy at the re­flec­tion height is sig­nif­i­cant­ly dif­fer­ent from the third elec­tron gy­ro­har­mon­ic fre­quen­cy.

SPCR

Naval Re­search Lab

A mi­crowave dri­ven res­onator is as an elec­tron/ion cloud gen­er­a­tor for il­lu­mi­na­tion and plas­ma source ap­pli­ca­tions. A sus­tained porous cav­i­ty res­onator (PCR) glow dis­charge is ex­ter­nal­ly ex­cit­ed us­ing a res­o­nant fre­quen­cy elec­tro­mag­net­ic (EM) wave that ex­cites large in­ter­nal elec­tric fields. The res­onator am­pli­fies the in­ci­dent elec­tric field by fac­tors of about 100 caus­ing a break­down of the neu­tral gas in­side the sphere. A glow­ing plas­ma ball is sus­tained around the point where the max­i­mum elec­tric fields ex­ceed the plas­ma-dis­charge thresh­old for the low-pres­sure gas in­side the res­onator. Af­ter the EM pump field is re­moved, the plas­ma light source is rapid­ly quenched. The ex­ter­nal­ly dri­ven spher­i­cal PCR was fab­ri­cat­ed from a the­o­ret­i­cal de­sign of the PCR for a lab­o­ra­to­ry demon­stra­tion of the plas­ma ball gen­er­a­tion sys­tem. Us­ing both the­o­ry and ex­per­i­ment, ba­sic re­search has been ap­plied to un­der­stand:

  1. the EMs of res­onator ex­ci­ta­tion and am­pli­fi­ca­tion
  2. the gen­er­a­tion of light by glow ra­dio fre­quen­cy dis­charge
  3. the ef­fect of back­ground neu­tral den­si­ty of the size and in­ten­si­ty of the glow­ing plas­ma clouds.

For this study, plas­ma res­onators were con­struct­ed for the spher­i­cal TM101 and TE101 modes and a TE011 cir­cu­lar-cylin­dri­cal cav­i­ty. All PCR struc­tures pro­vide the abil­i­ty to con­fine a plas­ma into a de­sired spa­tial shape with­out mag­net­ic fields.

Bibliography