Nishant Totla

EECS Homepage

Hello!

I'm a second year graduate student pursuing a PhD in the Dept. of Electrical Engineering and Computer Sciences at the University of California, Berkeley. My advisor is Prof. Sanjit Seshia.

I graduated from the Indian Institute of Technology Bombay in 2012, majoring in Computer Science and with a Minor degree in Mathematics.

Research Interests

I'm broadly interested in programming languages, synthesis, and formal methods. I'm also interested in designing collaborative constraint solving and proofs, particularly for program verification. Click here to read more about current and previous work.

News

I will be interning with the User Growth team at Twitter HQ, San Francisco this summer.

Chlorophyll: Synthesis-Aided Compiler for Low-Power Spatial Architectures accepted at PLDI 2014!

Contact Information

545L Cory Hall
Berkeley, CA - 94720



Back to Top

Research Experience


  

Research Projects


Massive Parallelization for SAT Solvers (June '13 - present)

Advisor: Sanjit Seshia

     

Graduate Student Researcher, UC Berkeley

Currently working on designing a hybrid parallelized SAT Solver based on a combination of the portfolio and divide-and-conquer approaches. The key goal is for the solver to efficiently scale to a large number (few hundred to thousand) of cores. We are using benchmarks from model checking and verification to tune and optimize the solver.

[Paper] [Poster]


Synthesis-based Compiler for GreenArrays (Nov '12 - present)

Advisor: Rastislav Bodík

     

Graduate Student Researcher, UC Berkeley

Developing a synthesis-based compiler toolchain that allows a programmer to write high-level C-style programs for spatial low-power architectures. These architectures are hard to program because of various issues, but a synthesis-based compiler helps the programmer, and can be designed and optimized faster than a traditional compiler. It is also retargetable (can be optimized for a different hardware). This work is funded by the Qualcomm Innovation Fellowship.

[Paper] (PLDI '14)


Comparing Expressive Power of Temporal Logics (Aug '11 - May '12)

Advisors: S Krishna, Paritosh Pandya

     

Bachelors' Thesis, IIT Bombay

We extended Ehrenfeucht-Fraissé (EF) to pointwise and continuous interpretations of Metric Temporal Logic (MTL), proving the corresponding EF Theorem. The theorem also holds in the presence of additional syntactic restrictions on modal operators or interval constraints, or both. This simplified proofs for many known expressibility results, and allowed us to discover some previously unknown results as well.

[Paper]


Synthesis from Incompatible Specifications (May '11 - July '11)

Advisors: Pavol Černý, Thomas Henzinger

     

Summer Internship, IST Austria

For a quantitative view of the relationship between specification and implementation, quantitative simulation distances were defined for automata, using 2-player mean payoff games. We first extended the definition to symmetric bisimulation, creating a metric space on automata, further extending it to work with continuous alphabet. We then used this framework to design an algorithm that finds an implementation given multiple mutually incompatible specifications. The implementation minimizes the maximum distance from each specification. We also showed that this problem is in NEXPTIME.

[Paper] (EMSOFT '12) [Report]


Complete Instantiation-based Interpolation (May '10 - July '10)

Advisors: Thomas Wies, Thomas Henzinger

     

Summer Internship, IST Austria

Finding inductive invariants for loops is one of the core tasks in formal program verification and reasoning about properties of programs. We considered the problem of automatically finding non-trivial inductive invariants for programs that manipulate list-like linked data structures. We developed a new approach for this problem using hierarchic reasoning over Local Theory Extensions, to generate Craig Interpolants.

[Paper] (POPL '13) [Report]


  

Class Projects


Survey: Automatic Generation of Program Invariants (Aug '12 - Dec '12)

Guide: George Necula

Extensively surveyed major theoretical and heuristic techniques for automatically generating program loop invariants. Techniques specifically focused on integer programs, and completeness of invariant generation.

[Paper]


Crowd-sourcing for Software Debugging and Verification (Aug '12 - Apr '13)

Guide: Sanjit Seshia

Program verification is a computationally hard task. While humans are better with creative tasks such as suggesting invariants, it is easier to automate checking correctness of these invariants. We designed a framework for human-aided program verification, where human input can be combined with automated techniques to prove properties of complex programs.

[Paper]


Extracting Variant Data from Templatized Web Pages (Jan '11 - May '11)

Guide: Sudarshan S

We developed a tool which learns the website template using a small number of representative pages generated from that template. We then used the deduced template to extract variant data (supposed to be the actual content on the site, and not structural information or ads) from the remaining pages. The search index built from data extracted by this tool was demonstrated (on a few selected websites) to give more relevant search results compared to flat indexing.

[Paper]


Modeling the Selective Repeat Protocol in EventB (Jan '11 - May '11)

Guide: Om Damani

Formally specified correctness and efficiency properties, and designed a model for the selective repeat sliding window packet transfer protocol through a series of refinements in the EventB language. Proved correctness of the model using RODIN tool and thus obtained provable bounds on the window size.

[Paper]


  

Poster Presentations


Programming Model for Spatial Low-power Architectures (September '13)

Qualcomm Innovation Fellowship Winners' Day, San Diego, CA, USA

[PPTX]


  

Talks


Programming Model and Synthesis for Low-power Spatial Architectures (March '13)

Qualcomm Innovation Fellowship Finals, Santa Clara, CA, USA

[PDF] [PPTX]


Large-scale Hybrid Parallel SAT Solving (May '14)

Berkeley Chaperone Project Retreat, Santa Cruz, CA, USA

[PPTX]


  

Side Projects


Research.js: Sharing your Research on the Web

Most research tools are publicly available but rarely used or tried out due to the difficulty of building them, which hinders the sharing of ideas. We used emscripten, an LLVM to JavaScript compiler to convert some SAT and SMT solvers to JavaScript, hoping to generalize the idea to all tools that can be compiled to LLVM bitcode.

[Paper]


proveIt: Crowd-sourced Program Verification

This was implemented to follow up on my class project. We designed a web app that allows users to register and submit invariants for programs. Inputs from multiple users are combined together to generate correctness proofs for the full program. This effort is far from complete, but you can check it out on http://crowdprover.herokuapp.com/.

Properties of ω-automata using Simulation Distances

During my internship at IST Austria, we proved several interesting topological properties on the metric space of finite automata, with the metric defined by simulation distances. We also considered the question of obtaining midpoints in this space.

[Paper]


Back to Top

Publications

2014

Phitchaya Mangpo Phothilimthana, Tikhon Jelvis, Rohin Shah, Nishant Totla, Sarah Chasins, Rastislav Bodík, "Chlorophyll: Synthesis-Aided Compiler for Low-Power Spatial Architectures", Proceedings of the 35th Annual Conference on Programming Language Design and Implementation (PLDI), ACM Press, 2014

2013

Nishant Totla, Thomas Wies, "Complete Instantiation-based Interpolation", Proceedings of the 40th Annual Symposium on Principles of Programming Languages (POPL), ACM Press, 2013

2012

Pavol Černý, Sivakanth Gopi, Thomas A. Henzinger, Arjun Radhakrishna, Nishant Totla, "Synthesis from Incompatible Specifications", Proceedings of the 12th Annual Conference on Embedded Software (EMSOFT), ACM Press, 2012 Back to Top

Distinctions


  

Scholarships and Fellowships


Won the Qualcomm Innovation Fellowship for the year 2013-14.

Won the Aditya Birla Group Scholarship for 2008-12, awarded to only 10 undergraduates from India each year, based on academic and extra-curricular excellence, and leadership qualities. This funded my undergraduate education.

Awarded the CBSE Merit Scholarship for 2008-12, for the top 300 students in AIEEE 2008.

Received the Infosys Foundation Cash Award for winning a Gold Medal at the International Physics Olympiad, 2008.

  

Olympiads


Won a Gold Medal at the 39th International Physics Olympiad 2008, held in Hanoi, Vietnam.

Selected among the top 25 students from India in the Indian National Mathematics Olympiad 2007.

Awarded National Gold Medal in the Indian National Physics Olympiad 2008, for finishing among the top 35 students all over the country, out of around 36,000 candidates.

Awarded National Gold Medal in the Indian National Chemistry Olympiad 2008, for finishing among the top 42 students all over the country, out of around 28,000 candidates.

Among the top 36 students from India in the Indian National Astronomy Olympiad in 2007 and 2008.

  

Academic


All India Rank 2 in the IIT Joint Entrance Examination 2008, out of more than 375,000 students.

All India Rank 43 in AIEEE 2008, out of more than 800,000 students.

Awarded the IIT Bombay Institute Award from Academic Excellence for the year 2008-09.

Back to Top

Resumé



Download PDF
Back to Top

Personal


Apart from research, I'm interested in a variety of other things. I try to do as much as I can, but 24 hours per day are too few, and some things take up more time than others. You can also visit my personal homepage to know more about me.

Running

I've been serious about long-distance running since I started in early 2013. For me, it is a lifelong pursuit of perfection. Additionally, it motivates me to stay fit and make healthy choices, while making many other athletic activities accessible.

Football

I've been watching football and supporting Arsenal Football Club since 2003. I played a lot too back in school, but have cut down since I started running. I still follow games every week though.

Music

I learned to play the keyboard and guitar in school, and have been playing since. I've also performed in events and competitions. I don't get enough time to practice now, but would love to start again, just looking for a reason.

Blogging

I have a blog where I write about a lot of my thoughts and ideas, and also events that ought to be remembered. I usually write in bursts. I also maintain a separate research blog.

Food and Cooking

Being vegetarian means I need to be much more mindful of what I eat. I have recently started to enjoy cooking. I spend a great deal of time trying to learn more about the sources and processes behind the foods I eat.

Adventure Sports

I'm a total sucker for anything that can provide an adrenaline rush. The top two sports on my list right now are skydiving and skiing, both of which I'm keen to pursue up to at least semi-professional level.

Biking

I like taking my bike on long rides, especially with lots of hills. A lot of my biking is also done as cross-training for running, or while healing from running injuries.

Reading

I love spending a peaceful afternoon or late night reading a book. I have no particular preferences, have most read (and enjoyed) fantasy, humor and non-fiction.

Movies and TV Shows

I try to watch good movies and TV shows in whatever free time I can manage. While I have no favourite movies, the X-Files is my all-time favourite TV show.

Back to Top