Nishant Totla

EECS Homepage


I'm a third 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. In particular, I'd like to apply techniques from these areas to new and interesting problems in other systems areas. Click here to read more about current and previous work.


I'm looking for internships for summer 2015. Feel free to contact me if you have an interesting opportunity!

I'm working on programming models for secure hardware.

Contact Information

545L Cory Hall
Berkeley, CA - 94720

Back to Top

Research Experience


Research Projects

Programming Model for Secure Hardware (September '14 - present)

Advisor: Sanjit Seshia


Graduate Student Researcher, UC Berkeley

For people running sensitive applications on remote infrastructure, the trusted computing base includes the hardware, privileged software (such as the OS) and even the people with physical access to the data. Intel SGX will change that by providing security features (memory protection, attestation etc.) to the programmer. I'm exploring programming models to help programmers write applications that can efficiently use these security features. In particular, I'm focusing on program partitioning using annotations.

Massive Parallelization for SAT Solvers (June '13 - May '14)

Advisor: Sanjit Seshia


Graduate Student Researcher, UC Berkeley

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

[Paper] [Poster]

Synthesis-based Compiler for GreenArrays (November '12 - September '14)

Advisor: Rastislav Bodík


Graduate Student Researcher, UC Berkeley

Developed 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 was funded by the Qualcomm Innovation Fellowship.

[Paper] (PLDI '14)

Comparing Expressive Power of Temporal Logics (August '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.


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

Exploring Research Literature using Visualization (September '14 - present)

Guide: Maneesh Agrawala

Exploring research literature in a new area can be a difficult task, with a large set of decentralized conferences and journals present in every field. I'm building a tool that uses smart visualization techniques to assist paper search, allowing the user to quickly find the most relevant set of papers to read.

Survey: Automatic Generation of Program Invariants (August '12 - December '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.


Crowd-sourcing for Software Debugging and Verification (August '12 - April '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.


Extracting Variant Data from Templatized Web Pages (January '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.


Modeling the Selective Repeat Protocol in EventB (January '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.



Poster Presentations

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

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




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

Qualcomm Innovation Fellowship Finals, Santa Clara, CA, USA


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

Berkeley Chaperone Project Retreat, Santa Cruz, CA, USA



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.


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

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.


Back to Top



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


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


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



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.



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.



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


Download PDF
Back to Top


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.


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.


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.


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.


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.


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.


I love spending a peaceful afternoon or late night reading a book. I have no particular preferences, have mostly 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