|
|
|
| SyncGen | syncgen | Automatic synchronization code generation |
| SpEx | spex | Specification Extensions for Bogor |
| Spec Patterns | patterns | Property specification for finite-state verification. |
| SpAda | spada | SpAda is an Eclipse plug-in for developing applications in SPARK -- a subset of Ada for high assurance applications developed by Praxis High Integrity Systems. SpAda provides integrated support for the Praxis SPARK Examiner -- a static checking tool that enforces very coding rules and information flow requirements. SpAda is integrated with AdaCore's GNATBench Eclipse plug-in for Ada.
Future versions of SpAda will provide advanced analysis capabilities to aid developers in constructing information flow specifications based on SPARK's "derives" annotations.
Our ultimate vision involves extending SpAda so that it becomes an integrated development environment that specifically targets development of information assurance applications in SPARK.
|
| Software Model Checking | smc | Software Model Checking course |
|
Search for projects in all categories
Enter * to return all
To search for projects, please enter the criteria in the text box and press "Search" to get the results
