Smartphone and web programming

Smartphones and web browsers are now the preferred application development platforms. Applications designed for them share many features that are not common in traditional desktop or server software and are therefore in need of tools specifically designed for them. For instance, smartphone and web applications are event-driven, selectively privileged, multi-user and integrated with online/cloud services. We work on language design and program analysis for improving programmability, concurrency, security and performance of these applications and the foundational components such as protocols, browsers and server/OS modules that support them.

Concurrency analysis of event-driven (or asynchronous) programs

  1. Ivan Gavran, Filip Niksic, Aditya Kanade, Rupak Majumdar, Viktor Vafeiadis. Rely/guarantee reasoning for asynchronous programs. 26th International Conference on Concurrency Theory (CONCUR), 2015.
  2. Pallavi Maiya, Aditya Kanade, Rupak Majumdar. Race detection for Android applications (DroidRacer). 35th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2014.

Correctness and compatibility of communication protocols

  1. Jay Thakkar, Aditya Kanade. Non-deterministic transducer models of retransmission protocols over noisy channels. Information Processing Letters (IPL), Volume 115, 2015.
  2. Jay Thakkar, Aditya Kanade, Rajeev Alur. Transducer-based algorithmic verification of retransmission protocols over noisy channels. 2013 IFIP Joint Conference on Formal Techniques for Distributed Systems (33rd FORTE/15th FMOODS)2013.
  3. Jay Thakkar, Aditya Kanade. Transducer models of sliding window ARQ protocols for noisy channels (Poster). IBM Collaborative Academia Exchange (I-CARE), 2012. First runner-up award.
  4. Pranavadatta Devaki, Aditya Kanade. Static analysis for checking data format compatibility of programs. 32nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), 2012.

Intelligent programming support

Over the past few years, programming has become a central activity not only in the industry but also in education (including K-12 education) and increasingly in the lives of end-users (e.g. in automation of simple recurrent tasks). At the same time, the areas of program analysis, machine learning and interactive computing technologies have made tremendous progress. Our objective is to develop novel techniques, building upon this progress and contributing to it, for improving productivity of developers in real-life software development, and for assisting students, educators and end-users with regards to programming.

Automated software engineering

  1. Mohammed Afraz, Diptikalyan Saha, Aditya Kanade. P3: Partitioned path profiling. 10th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE), 2015.
  2. Anirudh Santhiar, Omesh Pandita, Aditya Kanade. Mining unit tests for discovery and migration of math APIs (MathFinder). ACM Transactions on Software Engineering and Methodology (TOSEM), 2014.
  3. Shalini Kaleeswaran, Varun Tulsian, Aditya Kanade, Alessandro Orso. MintHint: Automated synthesis of repair hints (MintHint). 36th IEEE and ACM SIGSOFT International Conference on Software Engineering (ICSE), 2014. (Teaser video on youtube)
  4. Varun Tulsian, Aditya Kanade, Rahul Kumar, Akash Lal, Aditya Nori. MUX: Algorithm selection for software model checkers. 11th IEEE TCSE and ACM SIGSOFT Working Conference on Mining Software Repositories (MSR), 2014.
  5. Anirudh Santhiar, Omesh Pandita, Aditya Kanade. Discovering math APIs by mining unit tests (MathFinder). 16th EATCS International Conference on Fundamental Approaches to Software Engineering (FASE), 2013.
  6. Aditya Kanade, Rajeev Alur, Sriram Rajamani, G. Ramalingam. Representation dependence testing using program inversion. 18th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE), 2010.


Formal analysis of embedded control software

Embedded control software comprises discrete logic to monitor and control continuous dynamics of a system (e.g. a vehicle or an aeroplane). We have worked on formal semantics and analysis of designs of embedded control software, in particular, those expressed in the industry-leading Simulink/Stateflow environment from MathWorks.

Relevant publications

  1. Aditya Kanade, Rajeev Alur, Franjo Ivančić, S. Ramesh, Sriram Sankaranarayanan, K.C. Shashidhar. Generating and analyzing symbolic traces of Simulink/Stateflow models (Prototype tool). 21st International Conference on Computer Aided Verification (CAV), 2009.
  2. Rajeev Alur, Aditya Kanade, S. Ramesh, K.C. Shashidhar. Symbolic analysis for improving simulation coverage of Simulink/Stateflow models. 8th ACM and IEEE International Conference on Embedded Software (EMSOFT), 2008. ACM SIGBED EMSOFT best paper award
  3. Rajeev Alur, Aditya Kanade, Gera Weiss. Ranking automata and games for prioritized requirements. 20th International Conference on Computer Aided Verification (CAV), 2008

Compiler verification

Compilers constitute critical software infrastructure responsible for correct execution of source code. Modern compilers perform many advanced optimizations to make program execution more efficient. The high complexity of such optimizations demands verification techniques. We have worked on translation validation and theorem-prover based verification of compiler optimizations, using temporal logic based modeling of correctness requirements and precise definitions of optimizing transformations.

Verification and translation validation of compiler optimizations
  1. Aditya Kanade, Amitabha Sanyal, Uday P. Khedker. A logic for correlating temporal properties across program transformations. CoRR/ArXiv Technical Report, 2012.
  2. Aditya Kanade, Amitabha Sanyal, Uday P. Khedker. Validation of GCC optimizers through trace generation (SPOTS). Software Practice and Experience (SPE), Volume 39, Number 6, 2009.
  3. Aditya Kanade. SPOTS: A system for proving optimizing transformations sound. PhD thesis, IIT Bombay, 2007.
  4. Aditya Kanade, Amitabha Sanyal, Uday P. Khedker. Structuring optimizing transformations and proving them sound(SPOTS). Electronic Notes in Theoretical Computer Science (ENTCS), Volume 176, Number 3, 2007.
  5. Aditya Kanade, Amitabha Sanyal, Uday P. Khedker. A PVS based framework for validating compiler optimizations  (SPOTS). 4th IEEE International Conference on Software Engineering and Formal Methods (SEFM), 2006.
  6. Aditya Kanade, Uday P. Khedker, Amitabha Sanyal. Heterogeneous fixed points with application to points-to analysis. 3rd AAFS Asian Symposium on Programming Languages and Systems (APLAS), 2005.