
Abets
Demonstrator
vrain
Demonstrator
vrainABETS is an assertion-based dynamic parser that automatically computes abstract views of Maude executions. ABETS is built on top of a versatile program fragmenter and employs run-time assertion checking to improve dynamic analysis. ABETS can be used to improve error diagnosis in models (programs) written in Maude by automatically simplifying the size and complexity of the analyzed programs and their traces. The main strengths of the tool are: (i) automatic detection of erroneous program behavior with respect to a set of assertions, (ii) automatic inference of accurate fragmentation criteria for the detected errors, and (iii) automatic generation of simplified counterexamples.
See in the summary section
Program verification, safety analysis, provable security. Protocol crypto-analysis. Automated analysis, modeling, verification, synthesis, learning, debugging and optimization of complex systems and models