VSL Publications

Automated Verification of Chapel Programs Using Model Checking and Symbolic Execution

Cite
Timothy K. Zirkel and Stephen F. Siegel and Timothy McClory, Automated Verification of Chapel Programs Using Model Checking and Symbolic Execution. 5th NASA Formal Methods Symposium, NFM2013, Moffett Field CA, USA, May 14–16, 2013, Proceedings. Lecture Notes in Computer Science 7871, Springer Berlin Heidelberg (2013), pages 198–212.
Abstract
Chapel is a new programming language targeting high performance computing. Chapel makes it easier to write parallel code, but is still subject to concurrency problems such as deadlocks, race conditions, and nondeterministic results. In theory, model checking and symbolic execution tools can help with these problems, but certain Chapel primitives are difficult to represent in the models used by existing tools. For example, some primitives dynamically create arbitrarily nested scopes with threads executing within those scopes. We present (1) a new formal model that naturally represents these dynamic concepts and (2) a new prototype model checking/symbolic execution tool for Chapel programs that uses this model as its intermediate representation. We describe how the tool translates Chapel into this IR and the results of applying the tool to several synthetic Chapel programs.
Downloads
  1. Paper on publisher's web site
  2. loops_vmcai_2012.pdf (preprint)
BibTeX 
@incollection{
  year={2013},
  isbn={978-3-642-38087-7},
  booktitle={NASA Formal Methods},
  volume={7871},
  series={Lecture Notes in Computer Science},
  editor={Brat, Guillaume and Rungta, Neha and Venet, Arnaud},
  doi={10.1007/978-3-642-38088-4_14},
  title={Automated Verification of Chapel Programs Using Model Checking and Symbolic Execution},
  url={http://dx.doi.org/10.1007/978-3-642-38088-4_14},
  publisher={Springer Berlin Heidelberg},
  author={Zirkel, TimothyK. and Siegel, StephenF. and McClory, Timothy},
  pages={198-212}
}
VSL | Publications