CS615 Projects: Autumn 2017

Project Policy

Students are required to do their project work in groups of size 2; in exceptional circumstances, groups of size 3 may be allowed.
Each student group is required to do the following as part of their project:

Choose an abstract domain from the following list.
1. Intervals of rational numbers with a congruence relation (rational congruence domain)
2. Predicate abstraction with a given set of predicates
3. Access location based heap abstraction
Please feel free to discuss with the instructor for details of these domains.
Implement the abstract domain APIs in CAnalyzer for your chosen domain
Choose a code fragment (ideally approx 50 lines of uncommented C/C++/Java code) from an open source software, and verify at least one interesting property of the chosen code fragment using CAnalyzer working with your abstract domain implementation.

Each project will be evaluated separately based on a project report to be submitted prior to end-semester exams, and a live demonstration of the project.

The project necessarily involves implementing your chosen abstract domain in CAnalyzer. For this, you will need to familiarize yourself with the documentation and README files available here. The site is password protected. Please check moodle for login credentials.

The project evaluation schedule is as given below. During each of these evaluations, students must meet the instructor/TA and explain their project, and also give a demonstration of the project, if asked for.

Deliverables Date Where

Code and properties to be analyzed; abstract domain to be used; plan of implementation in CAnalyzer; a brief report Oct 27 Moodle

Final report; demonstration of working of abstract domain in CAnalyzer, using CAnalyzer with your domain to demonstrate property verification Nov 24 CFDVS Lab

Deliverables	Date	Where
Code and properties to be analyzed; abstract domain to be used; plan of implementation in CAnalyzer; a brief report	Oct 27	Moodle
Final report; demonstration of working of abstract domain in CAnalyzer, using CAnalyzer with your domain to demonstrate property verification	Nov 24	CFDVS Lab