Abstract
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.
Cite
CITATION STYLE
Din, C. C., Bubel, R., & Hähnle, R. (2015). KeY-ABS: A deductive verification tool for the concurrent modelling language ABS. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9195, pp. 517–526). Springer Verlag. https://doi.org/10.1007/978-3-319-21401-6_35
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
