Project: Implementation and Evaluation of Verification Algorithms for Boolean While Programs
Teamprojekt im Wintersemester 2018/19
News
- October 8
- The date of the kickoff meeting has been fixed: Oct 24 at 10 o'clock.
Organisation
During the winter term 2018/19, the Institute of Theoretical Computer Science offers a project on the Verification of Boolean Programs, headed by Prof. Dr. Roland Meyer. If you are interested in participating, please send a mail to Sebastian Wolff. (Currently, there are five registered participants; the project will take place.)
Topic
The goal of the project is to implement and evaluate various techniques for verifying boolean while programs. More precisely, the tasks involve:
- Implement a front-end, that is, a parser for a human-readable programming/domain-specific language.
- Implement various verification back-ends, for example, IC3/PDR, model checking based on BDDs, language-based verification, bounded model checking (BMC), verification conditions, interpolation.
- Implement backtracking to extract counter examples from incorrect programs that exemplify the incorrectness.
- Continuously improve the implementations to improve the runtime, creating an array of more and more elaborate implementations of a single technique.
- Create a comprehensive test suite.
- Evaluate your implementations on the test suite.
The main question that drives the project is how does the performance of certain verification algorithms depend on elaborate implementations?
If you have questions, please contact Sebastian Wolff.