×

zbMATH — the first resource for mathematics

Parametric and sliced causality. (English) Zbl 1135.68468
Damm, Werner (ed.) et al., Computer aided verification. 19th international conference, CAV 2007, Berlin, Germany, July 3–7, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-73367-6/pbk). Lecture Notes in Computer Science 4590, 240-253 (2007).
Summary: Happen-before causal partial orders have been widely used in concurrent program verification and testing. This paper presents a parametric approach to happen-before causal partial orders. Existing variants of happen-before relations can be obtained as instances of the parametric framework. A novel causal partial order, called sliced causality, is then defined also as an instance of the parametric framework, which loosens the obvious but strict happen-before relation by considering static and dynamic dependence information about the program. Sliced causality has been implemented in a runtime predictive analysis tool for Java, named jPredictor, and the evaluation results show that sliced causality can significantly improve the capability of concurrent verification and testing.
For the entire collection see [Zbl 1119.68005].

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Software:
jPredictor
PDF BibTeX XML Cite
Full Text: DOI