Lightning

The Lightning Tool is a language workbench distributed as an Eclipse plugin. It can be used to: – Create modelling languages from scratch, following an agile design process – Provide intuitive domain specific visualisations to existing models – Seamlessly execute language specifications for both verification and validation purposes – Specifying analysable and efficiently computable model…

Forge

Forge is a program analysis framework that allows a procedure in a conventional object oriented language to be automatically checked against a rich interface specification. The framework uses a bounded verification technique, in which all executions of a procedure are examined up to a user-provided bound on the heap and number of loop unrollings. If…