The Effect of Concurrent Programming Idioms on Verification - A Position Paper

David Harel, Guy Katz, Assaf Marron, Gera Weiss

2015

Abstract

In recent years formal verification techniques have become an important part of the development cycle of concurrent software. In order to tackle the state explosion problem and verify larger systems, a great deal of work has been put into improving the scalability of verification tools. In this work, we seek to draw attention to an alternative/complementary approach to improving scalability, which sometimes receives less notice: the effect the concurrent programming model itself has on one’s ability to verify programs encoded within it. Recent work suggests that a suitable choice of model, tailored to the problem at hand, may render the produced software more amenable to verification techniques. We recapitulate some recent and new results demonstrating this effect in programming models for discrete, synchronous reactive systems, and outline some directions for future work. We hope that the paper will trigger additional research on this important topic.

Paper Citation

in Harvard Style

Harel D., Katz G., Marron A. and Weiss G. (2015). The Effect of Concurrent Programming Idioms on Verification - A Position Paper . In Proceedings of the 3rd International Conference on Model-Driven Engineering and Software Development - Volume 1: MODELSWARD, ISBN 978-989-758-083-3, pages 363-369. DOI: 10.5220/0005324203630369

in Bibtex Style

@conference{modelsward15,
author={David Harel and Guy Katz and Assaf Marron and Gera Weiss},
title={The Effect of Concurrent Programming Idioms on Verification - A Position Paper},
booktitle={Proceedings of the 3rd International Conference on Model-Driven Engineering and Software Development - Volume 1: MODELSWARD,},
year={2015},
pages={363-369},
publisher={SciTePress},
organization={INSTICC},
doi={10.5220/0005324203630369},
isbn={978-989-758-083-3},
}

in EndNote Style

TY - CONF
JO - Proceedings of the 3rd International Conference on Model-Driven Engineering and Software Development - Volume 1: MODELSWARD,
TI - The Effect of Concurrent Programming Idioms on Verification - A Position Paper
SN - 978-989-758-083-3
AU - Harel D.
AU - Katz G.
AU - Marron A.
AU - Weiss G.
PY - 2015
SP - 363
EP - 369
DO - 10.5220/0005324203630369