dat logo




A Framework for Deadlock Detection in ABS
by Elena Giachino, Cosimo Laneve, Michael Lienhardt. December 2014
COMMENT: This is the reference paper of DF4ABS.

Deadlock analysis of unbounded process networks
by Elena Giachino, Naoki Kobayashi, Cosimo Laneve. March 2014
COMMENT: This is the reference paper about the theory behind the DF4ABS/FixPoint 2.0 algorithm.

Deadlock detection in linear recursive programs
by Elena Giachino, Cosimo Laneve. July 2013
COMMENT: This is the reference paper about the theory behind DF4ABS/model-check.

DeadLock Analysis of Concurrent Objects -- Theory and Practice
by Elena Giachino, Carlo A. Grazia, Cosimo Laneve, Michael Lienhardt, Peter Y.W. Wong. Proc. 10th Conference of integrated Formal Methods (iFM 2013). LNCS 7940, 2013.
COMMENT: This paper describes in some detail the DF4ABS inference system and fixpoint module.

ABS: A Core Language for Abstract Behavioral Specification
by Einar Broch Johnsen, Reiner Hahnle, Jan Scha╠łfer, Rudolf Schlatte, and Martin Steffen, Proc. 9th Intl. Symp. on Formal Methods for Components and Objects (FMCO 2010). LNCS 6957, 2010.
COMMENT: This is the reference paper about the syntax and semantics of core ABS

The ABS Language Specification
by the HATS Project, September 2012.
COMMENT: This is the current language specification of ABS


HATS Abstract Behavioral Specification: The Architectural View
by Reiner Hahnle, Michiel Helvensteijn, Einar Broch Johnsen, Michael Lienhardt, Davide Sangiorgi, Ina Schaefer, and Peter Y. H. Wong, Proc. 10th Intl. Symposium on Formal Methods for Components and Objects (FMCO 2011). LNCS 7542, 2011.
COMMENT: The architecture of the ABS Tool Suite is described in this paper.