The focus of Formal Methods and Verification Group is to develop formal techniques and tools for automatic verification and analysis of systems. The research activities of the group are supported in parts by US National Science Foundation grants IIS 225823, CCF 1555780, CCF 1116836, CCF 1143734 and CCF 0702758.
Members
Faculty: Samik Basu
Students
Current
- Erik Rauer (PhD)
- Yanhui Zhu (PhD, co-advosor, Pavan Aduri)
- Liwen Wang (MS)
- Karthik Hanumanthaiah (MS)
- Nagasharan Sathish (MS)
Alums
- Xiaoyun Fu (PhD, co-advisor: Pavan Aduri)
- Madhavan Rajagopal Padmanabhan (MS/PhD, co-advisor: Pavan Aduri): Amazon
- Zachary Oster (PhD): Associate Professor, University of Wisconsin, Whitewater
- Michelle Ruse (PhD): Professor, Des Moines Area Community College
- Tanmoy Sarkar (PhD): Microsoft
- Ganesh Ram Santhanam (PhD, co-advisor: Vasant Honavar)
- Jyotishman Pathak (PhD, co-advisor: Vasant Honavar): Professor and Division Chief of Health Informatics, Weill Cornell Medical College
- Sayaan Mitra (PhD, co-advisor: Ratnesh Kumar): Adobe
- Natalia Stakhanova (PhD): Assistant Professor, University of New Brunswick
- Sanchayani Pal (MS, co-Advisor: Myra Cohen)
- Rishabh Bhatt (MS, co-advisor: Pavan Aduri)
- Michael Dixon (MS)
- Bailey Righi (MS)
- Preeti Bhardwaj (MS): IBM
- Raj Gourav Kumar (MS)
- Sriram Balasubramanian (MS): Care.com
- Naresh Somisetty (MS): Microsoft
- Shiva Nalla (MS): Capital One
- Sai-Sravanthi Nudurupati (MS)
- Maheedhar Gunasekharan (MS): Randstad
- Priyanka Thyagarajan (MS): Amazon
- Swapnanjan Chatterjee (MS): PwC
- Sneha Bankar (MS): YP
- Paul Jennings (MS): MoSys
- Yuly Suvorov (MS): Google
- Curt Keller (MS): Continental Data Graphics
- Carl Chapman (BS Software Engineering)
- Katarina Mitchell (BS Computer Engineering): Uncorked Studio
Projects
† undergraduate student
‡ graduate student
Information Propagation Problems (Controlling or maximizing diffusion) .
Project Collaborators: Yanhui Zhu, Preeti Bhardwaj‡, Raj Gaurav Kumar‡, Madhavan Rajagopal Padmanabhan‡, Xiaoyun Fu‡, Rishabh Bhatt‡, Pavan Aduri.
Reasoning with Qualitative Preference . Many applications call for techniques for representing and reasoning about qualitative preferences over a set of alternatives. The objective is to investigate different types of qualitative preference languages in terms of their expressive power and develop efficient techniques to reason using qualitative prefereces.
Project Collaborators: Erik Rauer‡, Liwen Wang‡, Morgan Prieskorn†, Carl Chapman†, Katarina Mitchell†, Zachary Oster‡, Jia Tao, Ganesh Ram Santhanam, Robyn Lutz and Vasant Honavar.
Preference based Requirements Analysis in Software Engineering . Typically, alternative designs, technical and managerial choices in the domain of Software Engineering are analyzed on the basis of quantitative preferences and trade-offs. However, in many scenarios it is difficult to obtain (directly from users) and/or compute automatically preferences in quantitative terms. The objective is to develop an alternative approach purely based on qualitative preferences and realize application specific preference reasoning algorithms.
Project Collaborators: Zachary Oster‡ and Ganesh Ram Santhanam.
Verification of Asynchronous Systems. A crucial problem in dependability of concurrent and distributed software systems is the coordination of different components that form the whole system. In order to complete a task, components of a software system have to coordinate their executions by interacting with each other. Message-based communication is an increasingly common interaction mechanism used in concurrent and distributed systems where components interact with each other by sending and receiving messages. The goal of this project is to develop novel techniques for specification, analysis, and verification of message-based interactions.
Project Collaborators: Tevfik Bultan (UCSB), Oscar Ibarra (UCSB) and Meriem Ouderni (UMA).
Testing Database Applications. Database applications are built using two different programming language constructs; one that controls the behavior of the application, also referred to as the host language, and the other that allows the application to access/retrieve information from the backend database, also referred to as the query language. The interplay between these two languages make testing of database applications a challenging process. The objective of this project is to develop a testing framework that can automatically generate high-quality test cases for database applications.
Project Collaborators: Tanmoy Sarkar‡ and Johnny Wong.
Model Checking Parameterized Systems . Parameterized System describes an infinite family of (finite-state) systems, where each instance of the family is identified by the valuation of the parameter. Verification of parameterized system is undecidable in general. The challenge is to develop sound verification techniques for parameterized systems such that the techniques are independent of communication topology of the components of the system.
Project Collaborators: Hridesh Rajan, Youssef Hanna‡ and David Samuelson†.
Probabilistic Model Checking .
Project Collaborators: Paul Jennings‡ and Arka P. Ghosh (Statistics, ISU)
Vulnerability Analysis of Web Applications. Web applications that accept user input are vulnerable to class of attacks known as injection attacks, among which include SQL Injection and Cross-Site Scripting Attacks. These injection attacks occur when a user input containing malicious values is passed from the browser to the server application, possibly onto the database or onto other data store. The objective is to develop techniques based on model checking, program analysis and testing to identify possible scripting attacks in Web applications.
Project Collaborators: Michelle Ruse‡.
Web Service Composition. One of the main challenges for developing composite services is that the user needs to have the knowledge of existing component services and manually compose them in a fashion that results in the desired composition. Furthermore, the user is responsible for understanding and using service specification languages like OWL-S and WSDL. This restricts the number of users who can develop and deploy new services and also makes the process of service composition (even by knowledgeable users) tedious and error-prone. This project aims at developing a methodology that not only enhances the current state-of-art techniques for Web service composition but also enables end-users to develop, realize and execute composite services with little or no knowledge of the specifics of service composition.
Project Collaborators: Zachary Oster‡, Ganesh Ram Santhanam, Jyotishman Pathak‡, Dinanath Nadkarni‡, Hongyu Sun‡, Robyn Lutz and Vasant Honavar