×

KeY-ABS

swMATH ID: 39518
Software Authors: Din, Crystal Chang; Bubel, Richard; Hähnle, Reiner
Description: Key-ABS: a deductive verification tool for the concurrent modelling language ABS. We present KeY-ABS, a tool for deductive verification of concurrent and distributed programs written in ABS. KeY-ABS allows to verify data dependent and history-based functional properties of ABS models. In this paper we give a glimpse of system workflow, tool architecture, and the usage of KeY-ABS. In addition, we briefly present the syntax, semantics and calculus of KeY-ABS Dynamic Logic (ABSDL). The system is available for download.
Homepage: https://abs-models.org/tutorial_pdfs/KeY-ABS.pdf
Related Software: ABS; OptiMathSAT; vZ; SACO; SYMBA; Algorithm 864; z3; CPLEX
Referenced in: 3 Publications

Referencing Publications by Year