Projects
Established:
Angelic verification (AV) brings the benefits of static assertion checking to production software without inundating users with false alarms and not burdening them with upfront modeling. In other words, the goal of AV is to democratize static assertion checking for…
Established:
Seabed is a project to provide analytics over encrypted Big Data. The challenge is to develop fast yet secure cryptographic techniques that support a suite of applications such as Business Intelligence tools and large-scale Machine Learning frameworks. Towards this, we…
Established:
Corral is a whole-program analysis tool for Boogie programs. Corral uses goal-directed symbolic search techniques to find assertion violations. It leverages the powerful theorem prover Z3. It is available open source on GitHub. Corral, by default, does a bounded search up to a recursion depth…