Formal analysis in the Cloud

מערכת מבוססת ענן לאימות פורמלי

תיאור הפרויקט:

Formal verification systems allow rigorous mathematical analysis of software and hardware systems to prove their correctness or identify bugs that are hard to detect using traditional testing. Verification methods are inherently computationally expensive, and the focus of this project will be to develop and test a solution that allows to run the analysis on the cloud, activating parallel computations and analysis tasks, and enable the user to interact with the system effectively using a local machine

תכולת הפרויקט:

Developing and testing a prototype cloud based formal verification framework

דרישות:

Good programming skills, interest to learn about formal verification methods, taking course 83691 Formal Verification and Synthesis in parallel to project

מקורות:

Temporal Verification of Reactive Systems. Z. Manna and A. Pnueli. Springer. Model Checking. E.M. Clarke, O. Grumberg and D. Peled. MIT Pres