 Our research in software development spans all aspects of making developers more productive and software more trustworthy. It includes programming-language design, compilers, specification and verification, development environments and tools, runtime environments, formal models of systems, performance monitoring and optimization, and quality improvement. |
- T2 termination proverAutomatic program verification tool for proving termination and other liveness properties
- Code DiggerCode Digger is a Microsoft® Visual Studio® 2012 extension that analyzes possible execution paths through your .NET code. The result is a table where each row shows a unique behavior of your code. The table helps you understand the behavior of the code, and it may also uncover hidden bugs.
- Automated Problem Generation for EducationIntelligent Tutoring Systems (ITS) can significantly enhance the educational experience, both in the classroom and online. A key aspect of ITS is the ability to automatically generate problems of a certain difficulty level and that exercise use of certain concepts. This can help avoid copyright or plagiarism issues and help generate personalized workflows. This project develops technologies for problem generation in various subject domains including math, logic, and even language learning.
- PerfOratorProgramming models such as HIVE and DryadLINQ provide programmers with simple declarative abstractions for writing data intensive computations that can run on a large cluster of machines. However, this level of abstraction comes at a cost – the inability to understand, predict and debug performance. This project aims at building performance models for predicting the performance of the query while identifying bottleneck resources and computations.
Loris D'Antoni and Margus Veanes, Equivalence of Extended Symbolic Finite Transducers, in 25th International Conference on Computer Aided Verification (CAV'13), Springer, July 2013
Arun Chaganty, Akash Lal, Aditya V. Nori, and Sriram K. Rajamani, Combining Relational Learning with SMT Solvers using CEGAR, in Computer Aided Verification (CAV), Lecture Notes in Computer Science, July 2013
Manuel Fahndrich and Francesco Logozzo, Proceedings of the 20th Static Analysis Symposium, Springer Verlag, June 2013
Rahul Sharma, Saurabh Gupta, Bharath Hariharan, Alex Aiken, and Aditya V. Nori, Verification as Learning Geometric Concepts, in Static Analysis Symposium (SAS), Springer Verlag, June 2013
Sam Blackshear and Shuvendu Lahiri, Almost-Correct Specifications: A Modular Semantic Framework for Assigning Confidence to Warnings, in Programming Language Design and Implementation (PLDI'13), ACM, June 2013
