\begin{thebibliography}{100}

\bibitem{ACSL:Reference}
{ACSL}: {ANSI}/{ISO} {C} {S}pecification {L}anguage.
\newblock \url{http://frama-c.com/acsl.html}.
\newblock Accessed Sep.\ 6, 2019.

\bibitem{ada2012}
{A}da {R}eference {M}anual 2012.
\newblock \url{http://docs.adacore.com/live/wave/arm12/html/arm12/arm12.html}.
\newblock Accessed Sep.\ 6, 2019.

\bibitem{spark}
{SPARK} 2014 {R}eference {M}anual.
\newblock \url{http://docs.adacore.com/spark2014- docs/html/lrm/}.
\newblock Accessed Sep.\ 6, 2019.

\bibitem{amani:2017:complex}
S.~Amani, J.~Andronick, M.~Bortin, C.~Lewis, C.~Rizkallah, and J.~Tuong.
\newblock {COMPLEX}: {A} {V}erification {F}ramework for {C}oncurrent
  {I}mperative {P}rograms.
\newblock In {\em Proceedings of the 6th ACM SIGPLAN Conference on Certified
  Programs and Proofs}, CPP 2017, pages 138--150, New York, NY, USA, 2017. ACM.
\newblock \url{http://doi.acm.org/10.1145/3018610.3018627}.

\bibitem{araujo:2011:enabling}
W.~Araujo, L.~C. Briand, and Y.~Labiche.
\newblock {E}nabling the {R}untime {A}ssertion {C}hecking of {C}oncurrent
  {C}ontracts for the {J}ava {M}odeling {L}anguage.
\newblock In {\em Proceedings of the 33rd International Conference on Software
  Engineering}, ICSE '11, pages 786--795, New York, NY, USA, 2011. ACM.
\newblock \url{http://doi.acm.org/10.1145/1985793.1985903}.

\bibitem{armstrong:2013:programming}
J.~Armstrong.
\newblock {\em {P}rogramming {E}rlang: {S}oftware for a {C}oncurrent {W}orld}.
\newblock Pragmatic Bookshelf, 2013.

\bibitem{Ashcroft:1975:PAP:1739967.1740302}
E.~A. Ashcroft.
\newblock Proving assertions about parallel programs.
\newblock {\em J. Comput. Syst. Sci.}, 10(1):110--135, Feb. 1975.

\bibitem{ball:2010:towards}
T.~Ball, B.~Hackett, S.~Lahiri, S.~Qadeer, and J.~Vanegue.
\newblock {T}owards {S}calable {M}odular {C}hecking of {U}ser-{D}efined
  {P}roperties.
\newblock In {\em Verified Software: Theories, Tools and Experiments (VSTTE
  2010)}. Springer Verlag, August 2010.
\newblock
  \url{https://www.microsoft.com/en-us/research/publication/towards-scalable-modular-checking-of-user-defined-properties-2/}.

\bibitem{Barnes:2012:SPA}
J.~Barnes.
\newblock {\em {S}park: {T}he {P}roven {A}pproach to {H}igh {I}ntegrity
  {S}oftware}.
\newblock Altran Praxis, http://www.altran.co.uk, UK, 2012.
\newblock \url{http://www.altran.co.uk, UK}.

\bibitem{barnett:2006:boogie}
M.~Barnett, B.-Y.~E. Chang, R.~DeLine, B.~Jacobs, and K.~R.~M. Leino.
\newblock {B}oogie: {A} {M}odular {R}eusable {V}erifier for {O}bject-{O}riented
  {P}rograms.
\newblock In F.~S. de~Boer, M.~M. Bonsangue, S.~Graf, and W.-P. de~Roever,
  editors, {\em Formal Methods for Components and Objects}, pages 364--387,
  Berlin, Heidelberg, 2006. Springer Berlin Heidelberg.
\newblock \url{https://doi.org/10.1007/11804192_17}.

\bibitem{barnett:2005:specsharp}
M.~Barnett, K.~R.~M. Leino, and W.~Schulte.
\newblock The {S}pec{\#} {P}rogramming {S}ystem: {A}n {O}verview.
\newblock In G.~Barthe, L.~Burdy, M.~Huisman, J.-L. Lanet, and T.~Muntean,
  editors, {\em Construction and Analysis of Safe, Secure, and Interoperable
  Smart Devices}, pages 49--69, Berlin, Heidelberg, 2005. Springer Berlin
  Heidelberg.
\newblock \url{https://doi.org/10.1007/978-3-540-30569-9\_3}.

\bibitem{barrett-etal:2011:cvc4}
C.~Barrett, C.~L. Conway, M.~Deters, L.~Hadarean, D.~Jovanovi\'{c}, T.~King,
  A.~Reynolds, and C.~Tinelli.
\newblock {CVC4}.
\newblock In {\em International Conference on Computer Aided Verification},
  pages 171--177, 2011.

\bibitem{beckert:2007:KeY}
B.~Beckert, R.~H\"{a}hnle, and P.~H. Schmitt.
\newblock {\em Verification of Object-oriented Software: The KeY Approach}.
\newblock Springer-Verlag, Berlin, Heidelberg, 2007.
\newblock \url{http://doi.org/10.1007/978-3-540-69061-0}.

\bibitem{bergstra2001handbook}
J.~A. Bergstra, A.~Ponse, and S.~A. Smolka.
\newblock {\em Handbook of process algebra}.
\newblock Elsevier, 2001.

\bibitem{Bernaschi:2002:EIR:1895489.1895529}
M.~Bernaschi, G.~Iannello, and M.~Lauria.
\newblock {E}fficient {I}mplementation of {R}educe-scatter in {MPI}.
\newblock In {\em Proceedings of the 10th Euromicro Conference on Parallel,
  Distributed and Network-based Processing}, EUROMICRO-PDP'02, pages 301--308,
  Washington, DC, USA, 2002. IEEE Computer Society.

\bibitem{bernholdt-etal:2018:mpi_exascale}
D.~E. Bernholdt, S.~Boehm, G.~Bosilca, M.~Gorentla~Venkata, R.~E. Grant, T.~J.
  Naughton, III, H.~P. Pritchard, M.~Schulz, and G.~R. Vallee.
\newblock {A} {S}urvey of {MPI} {U}sage in the {U.S.}\ {E}xascale {C}omputing
  {P}roject.
\newblock Technical Report 790, Oak Ridge National Lab., June 2018.
\newblock \url{https://doi.org/10.2172/1462877}.

\bibitem{biere:2003:bounded}
A.~Biere, A.~Cimatti, E.~M. Clarke, O.~Strichman, Y.~Zhu, et~al.
\newblock {B}ounded {M}odel {C}hecking.
\newblock {\em Advances in computers}, 58(11):117--148, 2003.

\bibitem{blom:2017:vercors}
S.~Blom, S.~Darabi, M.~Huisman, and W.~Oortwijn.
\newblock The vercors tool set: Verification of parallel and concurrent
  software.
\newblock In N.~Polikarpova and S.~Schneider, editors, {\em Integrated Formal
  Methods}, pages 102--110, Cham, 2017. Springer International Publishing.
\newblock \url{https://doi.org/10.1007/978-3-319-66845-1_7}.

\bibitem{board:1993:ieee}
I.~Board.
\newblock {I}eee {S}tandard {C}lassification for {S}oftware {A}nomalies.
\newblock {\em IEEE Std}, 1044, 1993.

\bibitem{Bronevetsky:2009:CSD:1545006.1545049}
G.~Bronevetsky.
\newblock Communication-sensitive static dataflow for parallel message passing
  applications.
\newblock In {\em Proceedings of the 7th Annual IEEE/ACM International
  Symposium on Code Generation and Optimization}, CGO '09, pages 1--12,
  Washington, DC, USA, 2009. IEEE Computer Society.
\newblock \url{http://dx.doi.org/10.1109/CGO.2009.32}.

\bibitem{christakis:2011:detection}
M.~Christakis and K.~Sagonas.
\newblock Detection of asynchronous message passing errors using static
  analysis.
\newblock In R.~Rocha and J.~Launchbury, editors, {\em Practical Aspects of
  Declarative Languages}, pages 5--18, Berlin, Heidelberg, 2011. Springer
  Berlin Heidelberg.

\bibitem{clangstaticanalyzer}
Clang static analyzer.
\newblock \url{http://clang-analyzer.llvm.org}.
\newblock Accessed Sep.\ 6, 2019.

\bibitem{clarke:2000:modelchecking}
E.~M. Clarke, Jr., O.~Grumberg, and D.~A. Peled.
\newblock {\em {M}odel {C}hecking}.
\newblock MIT Press, Cambridge, MA, USA, 1999.

\bibitem{clarke:1976:symbolically}
L.~A. {Clarke}.
\newblock {A} {S}ystem to {G}enerate {T}est {D}ata and {S}ymbolically {E}xecute
  {P}rograms.
\newblock {\em IEEE Transactions on Software Engineering}, SE-2(3):215--222,
  Sep. 1976.
\newblock \url{http://doi.org/10.1109/TSE.1976.233817}.

\bibitem{cohen-etal:2009:vcc}
E.~Cohen, M.~Dahlweid, M.~Hillebrand, D.~Leinenbach, M.~Moskal, T.~Santen,
  W.~Schulte, and S.~Tobies.
\newblock {VCC}: {A} {P}ractical {S}ystem for {V}erifying {C}oncurrent {C}.
\newblock In S.~Berghofer, T.~Nipkow, C.~Urban, and M.~Wenzel, editors, {\em
  Theorem Proving in Higher Order Logics}, volume 5674 of {\em Lecture Notes in
  Computer Science}, pages 23--42. Springer Berlin / Heidelberg, 2009.
\newblock \url{http://dx.doi.org/10.1007/978-3-642-03359-9_2}.

\bibitem{alt-ergo}
S.~{Conchon}, M.~{Iguernelala}, and A.~{Mebsout}.
\newblock {A} {C}ollaborative {F}ramework for {N}on-{L}inear {I}nteger
  {A}rithmetic {R}easoning in {A}lt-{E}rgo.
\newblock In {\em 2013 15th International Symposium on Symbolic and Numeric
  Algorithms for Scientific Computing}, pages 161--168, Sep. 2013.
\newblock \url{http://doi.org/10.1109/SYNASC.2013.29}.

\bibitem{correctness:2017:proceedings}
{\em {C}orrectness'17: Proceedings of the First International Workshop on
  Software Correctness for HPC Applications}, New York, NY, USA, 2017. ACM.
\newblock \url{https://correctness-workshop.github.io/2017/}.

\bibitem{correctness:2018:proceedings}
{\em {C}orrectness'18: Proceedings of the Second International Workshop on
  Software Correctness for HPC Applications}, Los Alamitos, CA, USA, nov 2018.
  IEEE Computer Society.
\newblock
  \url{https://doi.ieeecomputersociety.org/10.1109/Correctness.2018.00004}.

\bibitem{Cranen:2013:OMT:2450387.2450410}
S.~Cranen, J.~F. Groote, J.~J.~A. Keiren, F.~P.~M. Stappers, E.~P. de~Vink,
  W.~Wesselink, and T.~A.~C. Willemse.
\newblock An overview of the mcrl2 toolset and its recent advances.
\newblock In {\em Proceedings of the 19th International Conference on Tools and
  Algorithms for the Construction and Analysis of Systems}, TACAS'13, pages
  199--213, Berlin, Heidelberg, 2013. Springer-Verlag.

\bibitem{cuoq2012framac}
P.~Cuoq, F.~Kirchner, N.~Kosmatov, V.~Prevosto, J.~Signoles, and B.~Yakobowski.
\newblock {F}rama-{C}.
\newblock In G.~Eleftherakis, M.~Hinchey, and M.~Holcombe, editors, {\em
  Software Engineering and Formal Methods}, pages 233--247, Berlin, Heidelberg,
  2012. Springer Berlin Heidelberg.
\newblock \url{https://doi.org/10.1007/978-3-642-33826-7_16}.

\bibitem{cuoq:2011:wp}
P.~Cuoq, B.~Monate, A.~Pacalet, and V.~Prevosto.
\newblock Functional dependencies of c functions via weakest pre-conditions.
\newblock {\em International Journal on Software Tools for Technology
  Transfer}, 13(5):405--417, Oct 2011.
\newblock \url{"https://doi.org/10.1007/s10009-011-0192-z"}.

\bibitem{dannenberg:1982:formal}
R.~B. {Dannenberg} and G.~W. {Ernst}.
\newblock {F}ormal {P}rogram {V}erification {U}sing {S}ymbolic {E}xecution.
\newblock {\em IEEE Transactions on Software Engineering}, SE-8(1):43--52, Jan
  1982.
\newblock \url{10.1109/TSE.1982.234773}.

\bibitem{Z3Prover}
L.~de~Moura and N.~Bj{\o}rner.
\newblock Z3: An {E}fficient {SMT} {S}olver.
\newblock In C.~R. Ramakrishnan and J.~Rehof, editors, {\em Tools and
  Algorithms for the Construction and Analysis of Systems}, pages 337--340,
  Berlin, Heidelberg, 2008. Springer Berlin Heidelberg.

\bibitem{drake:2005:overview}
J.~B. Drake, P.~W. Jones, and G.~R. Carr.
\newblock {O}verview of the {S}oftware {D}esign of the {C}ommunity {C}limate
  {S}ystem {M}odel.
\newblock {\em IJHPCA}, 19:177--186, 2005.
\newblock \url{https://journals.sagepub.com/doi/pdf/10.1177/1094342005056094}.

\bibitem{Droste:2015:MSA:2833157.2833159}
A.~Droste, M.~Kuhn, and T.~Ludwig.
\newblock {MPI}-{C}hecker: {S}tatic {A}nalysis for {MPI}.
\newblock In {\em Proceedings of the Second Workshop on the LLVM Compiler
  Infrastructure in HPC}, LLVM '15, pages 3:1--3:10, New York, NY, USA, 2015.
  ACM.
\newblock \url{http://doi.acm.org/10.1145/2833157.2833159}.

\bibitem{dwyer:1999:patterns}
M.~B. {Dwyer}, G.~S. {Avrunin}, and J.~C. {Corbett}.
\newblock {P}atterns in property specifications for finite-state verification.
\newblock In {\em Proceedings of the 1999 International Conference on Software
  Engineering (IEEE Cat. No.99CB37002)}, pages 411--420, May 1999.
\newblock \url{http://doi.org/10.1145/302405.302672}.

\bibitem{falgout:2002:hypre}
R.~D. Falgout and U.~M. Yang.
\newblock \emph{hypre}: {A} {L}ibrary of {H}igh {P}erformance
  {P}reconditioners.
\newblock In P.~M.~A. Sloot, A.~G. Hoekstra, C.~J.~K. Tan, and J.~J. Dongarra,
  editors, {\em Computational Science --- ICCS 2002}, pages 632--641, Berlin,
  Heidelberg, 2002. Springer Berlin Heidelberg.
\newblock \url{https://doi.org/10.1007/3-540-47789-6\_66}.

\bibitem{filliatre:2013:why3}
J.-C. Filli{\^a}tre and A.~Paskevich.
\newblock {W}hy3 --- {W}here {P}rograms {M}eet {P}rovers.
\newblock In M.~Felleisen and P.~Gardner, editors, {\em Programming Languages
  and Systems}, pages 125--128, Berlin, Heidelberg, 2013. Springer Berlin
  Heidelberg.
\newblock \url{https://doi.org/10.1007/978-3-642-37036-6_8}.

\bibitem{Floyd1993}
R.~W. Floyd.
\newblock {\em {A}ssigning {M}eanings to {P}rograms}, pages 65--81.
\newblock Springer Netherlands, Dordrecht, 1993.
\newblock \url{https://doi.org/10.1007/978-94-011-1793-7\_4}.

\bibitem{Forejt:2017:PPA:3133234.3095075}
V.~Forejt, S.~Joshi, D.~Kroening, G.~Narayanaswamy, and S.~Sharma.
\newblock Precise predictive analysis for discovering communication deadlocks
  in mpi programs.
\newblock {\em ACM Trans. Program. Lang. Syst.}, 39(4):15:1--15:27, Aug. 2017.

\bibitem{godefroid:1993:refining}
P.~Godefroid and D.~Pirottin.
\newblock Refining dependencies improves partial-order verification methods
  (extended abstract).
\newblock In C.~Courcoubetis, editor, {\em Computer Aided Verification}, pages
  438--449, Berlin, Heidelberg, 1993. Springer Berlin Heidelberg.

\bibitem{gopalakrishnan-etal:2017:correctness}
G.~Gopalakrishnan, P.~D. Hovland, C.~Iancu, S.~Krishnamoorthy, I.~Laguna, R.~A.
  Lethin, K.~Sen, S.~F. Siegel, and A.~Solar-Lezama.
\newblock {R}eport of the {HPC} {C}orrectness {S}ummit.
\newblock Technical report, USDOE Office of Science (SC), 2017.
\newblock \url{https://arxiv.org/abs/1705.07478}.

\bibitem{gordon:1989:mechanizing}
M.~J.~C. Gordon.
\newblock {\em Mechanizing Programming Logics in Higher Order Logic}, pages
  387--439.
\newblock Springer New York, New York, NY, 1989.
\newblock \url{https://doi.org/10.1007/978-1-4612-3658-0_10}.

\bibitem{Gosling:2014:JLS:2636997}
J.~Gosling, B.~Joy, G.~L. Steele, G.~Bracha, and A.~Buckley.
\newblock {\em {T}he {J}ava {L}anguage {S}pecification, {J}ava {SE} 8
  {E}dition}.
\newblock Addison-Wesley Professional, 1st edition, 2014.

\bibitem{hatton:1997:T_Experiments}
L.~Hatton.
\newblock The {T} experiments: Errors in scientific software.
\newblock {\em IEEE Computational Science \& Engineering}, 4(2):27--38, Apr.
  1997.

\bibitem{hatton:2012:defects}
L.~Hatton.
\newblock Defects, scientific computation and the scientific method.
\newblock In A.~M. Dienstfrey and R.~F. Boisvert, editors, {\em Uncertainty
  Quantification in Scientific Computing}, volume 377 of {\em IFIP Advances in
  Information and Communication Technology}, pages 123--138. Springer Berlin
  Heidelberg, 2012.

\bibitem{hatton-roberts:1994:accurate}
L.~Hatton and A.~Roberts.
\newblock How accurate is scientific software?
\newblock {\em {IEEE} {T}ransactions on {S}oftware {E}ngineering},
  20(10):785--797, Oct. 1994.

\bibitem{Hentschel2018}
M.~Hentschel, R.~Bubel, and R.~H\"{a}hnle.
\newblock {T}he {S}ymbolic {E}xecution {D}ebugger ({SED}): a platform for
  interactive symbolic execution, debugging, verification and more.
\newblock {\em International Journal on Software Tools for Technology
  Transfer}, 2018.

\bibitem{Hilbrich:2012:MRE:2388996.2389037}
T.~Hilbrich, J.~Protze, M.~Schulz, B.~R. de~Supinski, and M.~S. M\"{u}ller.
\newblock Mpi runtime error detection with must: Advances in deadlock
  detection.
\newblock In {\em Proceedings of the International Conference on High
  Performance Computing, Networking, Storage and Analysis}, SC '12, pages
  30:1--30:11, Los Alamitos, CA, USA, 2012. IEEE Computer Society Press.
\newblock \url{http://dl.acm.org/citation.cfm?id=2388996.2389037}.

\bibitem{hoare:1969:axiomatic}
C.~A.~R. Hoare.
\newblock {A}n axiomatic basis for computer programming.
\newblock {\em Communications of the {ACM}}, 12(10):576--580, 1969.

\bibitem{Hoare:1985:CSP:3921}
C.~A.~R. Hoare.
\newblock {\em Communicating Sequential Processes}.
\newblock Prentice-Hall, Inc., Upper Saddle River, NJ, USA, 1985.

\bibitem{holzmann1997spin}
G.~J. {Holzmann}.
\newblock The model checker spin.
\newblock {\em IEEE Transactions on Software Engineering}, 23(5):279--295, May
  1997.

\bibitem{huchant2019multivalued}
P.~Huchant, E.~Saillard, D.~Barthou, and P.~Carribault.
\newblock Multi-valued expression analysis for collective checking.
\newblock In R.~Yahyapour, editor, {\em Euro-Par 2019: Parallel Processing},
  pages 29--43, Cham, 2019. Springer International Publishing.
\newblock \url{https://doi.org/10.1007/978-3-030-29400-7_3}.

\bibitem{iso:2011:c11}
{International Organization for Standardization} and {International
  Electrotechnical Commission}.
\newblock {ISO/IEC 989:2011 N1570: Programming Languages -- C}.
\newblock \url{http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1570.pdf}, Apr.
  2011.

\bibitem{Jackson:2006:SAL}
D.~Jackson.
\newblock {\em Software Abstractions: Logic, Language, and Analysis}.
\newblock The MIT Press, 2006.

\bibitem{Jacobs:2010:QTV:1947873.1947902}
B.~Jacobs, J.~Smans, and F.~Piessens.
\newblock A quick tour of the verifast program verifier.
\newblock In {\em Proceedings of the 8th Asian Conference on Programming
  Languages and Systems}, APLAS'10, pages 304--311, Berlin, Heidelberg, 2010.
  Springer-Verlag.
\newblock \url{http://dl.acm.org/citation.cfm?id=1947873.1947902}.

\bibitem{java8}
{J}ava {SE} 8.
\newblock
  \url{https://www.oracle.com/technetwork/java/javase/overview/java8-2100321.html}.
\newblock Accessed Sep.\ 6, 2019.

\bibitem{johansen:2017:earthquake}
H.~{Johansen}, A.~{Rodgers}, N.~A. {Petersson}, D.~{McCallen}, B.~{Sjogreen},
  and M.~{Miah}.
\newblock {T}oward {E}xascale {E}arthquake {G}round {M}otion {S}imulations for
  {N}ear-{F}ault {E}ngineering {A}nalysis.
\newblock {\em Computing in Science Engineering}, 19(5):27--37, 2017.
\newblock \url{http://doi.org/10.1109/MCSE.2017.3421558}.

\bibitem{KANG2019220}
Q.~Kang, J.~L. Träff, R.~Al-Bahrani, A.~Agrawal, A.~Choudhary, and W.~keng
  Liao.
\newblock Scalable algorithms for mpi intergroup allgather and allgatherv.
\newblock {\em Parallel Computing}, 85:220 -- 230, 2019.

\bibitem{10.1007/BFb0013032}
S.~Katz and D.~Peled.
\newblock {A}n efficient verification method for parallel and distributed
  programs.
\newblock In J.~W. de~Bakker, W.~P. de~Roever, and G.~Rozenberg, editors, {\em
  Linear Time, Branching Time and Partial Order in Logics and Models for
  Concurrency}, pages 489--507, Berlin, Heidelberg, 1989. Springer Berlin
  Heidelberg.
\newblock \url{https://doi.org/10.1007/BFb0013032}.

\bibitem{Kauer:2010:MII:1860141.1860452}
S.~Kauer and J.~F.~H. Winkler.
\newblock {M}echanical {I}nference of {I}nvariants for {FOR}-loops.
\newblock {\em J. Symb. Comput.}, 45(11):1101--1113, Nov. 2010.

\bibitem{khanna2018dynamic}
D.~Khanna, S.~Sharma, C.~Rodr{\'i}guez, and R.~Purandare.
\newblock Dynamic {S}ymbolic {V}erification of {MPI} {P}rograms.
\newblock In K.~Havelund, J.~Peleska, B.~Roscoe, and E.~de~Vink, editors, {\em
  Formal Methods}, pages 466--484, Cham, 2018. Springer International
  Publishing.
\newblock \url{https://doi.org/10.1007/978-3-319-95582-7\_28}.

\bibitem{king:1976:symbolic}
J.~C. King.
\newblock {S}ymbolic execution and program testing.
\newblock {\em Communications of the ACM}, 19(7):385--394, 1976.
\newblock \url{https://doi.org/10.1145/360248.360252}.

\bibitem{Kleymann:1999:HLA:2769784.2769811}
T.~Kleymann.
\newblock {H}oare {L}ogic and {A}uxiliary {V}ariables.
\newblock {\em Form. Asp. Comput.}, 11(5):541--566, Dec. 1999.

\bibitem{kovacs:2013:firstorder}
L.~Kov\'{a}cs and A.~Voronkov.
\newblock {F}irst-{O}rder {T}heorem {P}roving and {V}ampire.
\newblock In {\em Proceedings of the 25th International Conference on Computer
  Aided Verification - Volume 8044}, CAV 2013, pages 1--35, New York, NY, USA,
  2013. Springer-Verlag New York, Inc.
\newblock \url{http://dx.doi.org/10.1007/978-3-642-39799-8_1}.

\bibitem{krammer2004marmot}
B.~Krammer, K.~Bidmon, M.~S. M{\"u}ller, and M.~M. Resch.
\newblock Marmot: An mpi analysis and checking tool.
\newblock In {\em Advances in Parallel Computing}, volume~13, pages 493--500.
  Elsevier, 2004.
\newblock \url{https://doi.org/10.1016/S0927-5452(04)80063-7}.

\bibitem{krenn:2009:test}
W.~Krenn and B.~K. Aichernig.
\newblock {T}est {C}ase {G}eneration by {C}ontract {M}utation in {S}pec{\#}.
\newblock {\em Electronic Notes in Theoretical Computer Science}, 253(2):71 --
  86, 2009.
\newblock
  \url{http://www.sciencedirect.com/science/article/pii/S157106610900406X}.

\bibitem{kroening:2014:cbmc}
D.~Kroening and M.~Tautschnig.
\newblock Cbmc -- c bounded model checker.
\newblock In E.~{\'A}brah{\'a}m and K.~Havelund, editors, {\em Tools and
  Algorithms for the Construction and Analysis of Systems}, pages 389--391,
  Berlin, Heidelberg, 2014. Springer Berlin Heidelberg.

\bibitem{lahiri2012security}
S.~Lahiri.
\newblock {S}ecurity audit using extended static checking: Is it cost-effective
  yet?
\newblock Technical Report MSR-TR-2012-103, microsoft, October 2012.
\newblock
  \url{https://www.microsoft.com/en-us/research/publication/security-audit-using-extended-static-checking-is-it-cost-effective-yet/}.

\bibitem{lamport:1980:hoare}
L.~Lamport.
\newblock {T}he `{H}oare logic' of concurrent programs.
\newblock {\em Acta Informatica}, 14(1):21--37, Jun 1980.
\newblock \url{https://doi.org/10.1007/BF00289062}.

\bibitem{leavens:1999:jml}
G.~T. Leavens, A.~L. Baker, and C.~Ruby.
\newblock {\em {JML}: {A} {N}otation for {D}etailed {D}esign}, pages 175--188.
\newblock Springer US, Boston, MA, 1999.
\newblock \url{https://doi.org/10.1007/978-1-4615-5229-1_12}.

\bibitem{leino:2010:dafny}
K.~R.~M. Leino.
\newblock {D}afny: {A}n {A}utomatic {P}rogram {V}erifier for {F}unctional
  {C}orrectness.
\newblock In E.~M. Clarke and A.~Voronkov, editors, {\em Logic for Programming,
  Artificial Intelligence, and Reasoning}, pages 348--370, Berlin, Heidelberg,
  2010. Springer Berlin Heidelberg.
\newblock \url{https://doi.org/10.1007/978-3-642-17511-4_20}.

\bibitem{leino:2009:verification}
K.~R.~M. Leino, P.~M{\"u}ller, and J.~Smans.
\newblock {\em {V}erification of {C}oncurrent {P}rograms with {C}halice}, pages
  195--222.
\newblock Springer Berlin Heidelberg, Berlin, Heidelberg, 2009.
\newblock \url{https://doi.org/10.1007/978-3-642-03829-7_7}.

\bibitem{leino:1999:checkingjava}
K.~R.~M. Leino, J.~B. Saxe, and R.~Stata.
\newblock Checking java programs via guarded commands.
\newblock In {\em Proceedings of the Workshop on Object-Oriented Technology},
  pages 110--111, London, UK, UK, 1999. Springer-Verlag.
\newblock \url{http://dl.acm.org/citation.cfm?id=646779.704969}.

\bibitem{lipton:reduction}
R.~J. Lipton.
\newblock {R}eduction: {A} {M}ethod of {P}roving {P}roperties of {P}arallel
  {P}rograms.
\newblock {\em Commun. ACM}, 18(12):717--721, Dec. 1975.

\bibitem{Lopez:2015:PVM:2814270.2814302}
H.~A. L\'{o}pez, E.~R.~B. Marques, F.~Martins, N.~Ng, C.~Santos, V.~T.
  Vasconcelos, and N.~Yoshida.
\newblock Protocol-based {V}erification of {M}essage-passing {P}arallel
  {P}rograms.
\newblock In {\em Proceedings of the 2015 ACM SIGPLAN International Conference
  on Object-Oriented Programming, Systems, Languages, and Applications}, OOPSLA
  2015, pages 280--298, New York, NY, USA, 2015. ACM.
\newblock \url{http://doi.acm.org/10.1145/2814270.2814302}.

\bibitem{10.1007/978-3-030-03421-4_12}
Z.~Luo and S.~F. Siegel.
\newblock {S}ymbolic {E}xecution and {D}eductive {V}erification {A}pproaches to
  {V}erify{T}his 2017 {C}hallenges.
\newblock In T.~Margaria and B.~Steffen, editors, {\em Leveraging Applications
  of Formal Methods, Verification and Validation. Verification}, pages
  160--178, Cham, 2018. Springer International Publishing.

\bibitem{luo2018towards}
Z.~{Luo} and S.~F. {Siegel}.
\newblock Towards deductive verification of message-passing parallel programs.
\newblock In {\em 2018 IEEE/ACM 2nd International Workshop on Software
  Correctness for HPC Applications (Correctness)}, pages 59--68, Nov 2018.
\newblock \url{https://doi.org/10.1109/Correctness.2018.00012}.

\bibitem{Luo:2017:VMP:3127024.3127032}
Z.~Luo, M.~Zheng, and S.~F. Siegel.
\newblock Verification of mpi programs using civl.
\newblock In {\em Proceedings of the 24th European MPI Users' Group Meeting},
  EuroMPI '17, pages 6:1--6:11, New York, NY, USA, 2017. ACM.
\newblock \url{http://doi.acm.org/10.1145/3127024.3127032}.

\bibitem{Manna:1984:APP:2731.2734}
Z.~Manna and A.~Pnueli.
\newblock {A}dequate {P}roof {P}rinciples for {I}nvariance and {L}iveness
  {P}roperties of {C}oncurrent {P}rograms.
\newblock {\em Sci. Comput. Program.}, 4(3):257--289, Dec. 1984.

\bibitem{mathuriya:2017:embracingquantum}
A.~Mathuriya, Y.~Luo, R.~C. Clay, III, A.~Benali, L.~Shulenburger, and J.~Kim.
\newblock {E}mbracing a {N}ew {E}ra of {H}ighly {E}fficient and {P}roductive
  {Q}uantum {M}onte {C}arlo {S}imulations.
\newblock In {\em Proceedings of the International Conference for High
  Performance Computing, Networking, Storage and Analysis}, SC '17, pages
  38:1--38:12, New York, NY, USA, 2017. ACM.
\newblock \url{http://doi.acm.org/10.1145/3126908.3126952}.

\bibitem{mcmillan:1993:symbolic}
K.~L. McMillan.
\newblock {\em {S}ymbolic {M}odel {C}hecking}, pages 25--60.
\newblock Springer US, Boston, MA, 1993.
\newblock \url{https://doi.org/10.1007/978-1-4615-3190-6_3}.

\bibitem{McMillan:2010:LAP:2144310.2144323}
K.~L. McMillan.
\newblock {L}azy {A}nnotation for {P}rogram {T}esting and {V}erification.
\newblock In {\em Proceedings of the 22Nd International Conference on Computer
  Aided Verification}, CAV'10, pages 104--118, Berlin, Heidelberg, 2010.
  Springer-Verlag.

\bibitem{merali:2010:error}
Z.~Merali.
\newblock {E}rror: why scientific programming does not compute.
\newblock {\em Nature}, 467(7317):775--777, 2010.

\bibitem{mpi-forum:2015:mpi31}
{Message Passing Interface Forum}.
\newblock {MPI}: A {M}essage-{P}assing {I}nterface standard, version 3.1.
\newblock \url{https://www.mpi-forum.org/docs/mpi-3.1/mpi31-report.pdf}, June
  2015.

\bibitem{Meyer:1988:eiffel}
B.~Meyer.
\newblock Eiffel: A language and environment for software engineering.
\newblock {\em J. Syst. Softw.}, 8(3):199--246, June 1988.

\bibitem{Meyer:1992:ADC}
B.~Meyer.
\newblock Applying "{D}esign by {C}ontract".
\newblock {\em Computer}, 25(10):40--51, Oct. 1992.

\bibitem{Newton1975}
G.~Newton.
\newblock {P}roving {P}roperties of {I}nteracting {P}rocesses.
\newblock {\em Acta Informatica}, 4(2):117--126, Jun 1975.

\bibitem{oortwijn2016future}
W.~Oortwijn, S.~Blom, and M.~Huisman.
\newblock Future-based {S}tatic {A}nalysis of {M}essage {P}assing {P}rograms.
\newblock In D.~Orchard and N.~Yoshida, editors, {\em Proceedings PLACES 2016},
  pages 65--72, 4 2016.
\newblock \url{https://doi.org/10.4204/EPTCS.211.7}.

\bibitem{Owicki1976}
S.~Owicki and D.~Gries.
\newblock {A}n {A}xiomatic {P}roof {T}echnique for {P}arallel {P}rograms
  {I}$^*$.
\newblock {\em Acta Informatica}, 6(4):319--340, Dec 1976.

\bibitem{Owicki:1982:PLP:357172.357178}
S.~Owicki and L.~Lamport.
\newblock {P}roving {L}iveness {P}roperties of {C}oncurrent {P}rograms.
\newblock {\em ACM Trans. Program. Lang. Syst.}, 4(3):455--495, July 1982.

\bibitem{Palmer:2007:SDD:1273647.1273657}
R.~Palmer, G.~Gopalakrishnan, and R.~M. Kirby.
\newblock {S}emantics {D}riven {D}ynamic {P}artial-order {R}eduction of
  {MPI}-based {P}arallel {P}rograms.
\newblock In {\em Proceedings of the 2007 ACM Workshop on Parallel and
  Distributed Systems: Testing and Debugging}, PADTAD '07, pages 43--53, New
  York, NY, USA, 2007. ACM.
\newblock \url{http://doi.acm.org/10.1145/1273647.1273657}.

\bibitem{rebelo:2014:aspectjml}
H.~Reb\^{e}lo, G.~T. Leavens, M.~Bagherzadeh, H.~Rajan, R.~Lima, D.~M.
  Zimmerman, M.~Corn{\'e}lio, and T.~Th\"{u}m.
\newblock {A}spect{JML}: {M}odular {S}pecification and {R}untime {C}hecking for
  {C}rosscutting {C}ontracts.
\newblock In {\em Proceedings of the 13th International Conference on
  Modularity}, MODULARITY '14, pages 157--168, New York, NY, USA, 2014. ACM.
\newblock \url{http://doi.acm.org/10.1145/2577080.2577084}.

\bibitem{reynolds2002separation}
J.~C. {R}eynolds.
\newblock {S}eparation {L}ogic: a {L}ogic for {S}hared {M}utable {D}ata
  {S}tructures.
\newblock In {\em Proceedings 17th Annual IEEE Symposium on Logic in Computer
  Science}, pages 55--74, July 2002.
\newblock \url{http://doi.org/10.1109/LICS.2002.1029817}.

\bibitem{romano-etal:2015:openmc}
P.~K. Romano, N.~E. Horelik, B.~R. Herman, A.~G. Nelson, B.~Forget, and
  K.~Smith.
\newblock {O}pen{MC}: {A} state-of-the-art {M}onte {C}arlo code for research
  and development.
\newblock {\em Annals of Nuclear Energy}, 82:90 -- 97, 2015.
\newblock
  \url{http://www.sciencedirect.com/science/article/pii/S030645491400379X}.

\bibitem{Ruefenacht:2017:GRD:3163938.3164013}
M.~Ruefenacht, M.~Bull, and S.~Booth.
\newblock {G}eneralisation of {R}ecursive {D}oubling for {A}llreduce.
\newblock {\em Parallel Comput.}, 69(C):24--44, Nov. 2017.

\bibitem{Sankaranarayanan04non-linearloop}
S.~Sankaranarayanan, H.~B. Sipma, and Z.~Manna.
\newblock {N}on-linear {L}oop {I}nvariant {G}eneration using {G}r\"{o}bner
  {B}ases, 2004.

\bibitem{10.1007/978-3-540-30579-8_27}
S.~F. Siegel.
\newblock Efficient verification of halting properties for mpi programs with
  wildcard receives.
\newblock In R.~Cousot, editor, {\em Verification, Model Checking, and Abstract
  Interpretation}, pages 413--429, Berlin, Heidelberg, 2005. Springer Berlin
  Heidelberg.
\newblock \url{https://doi.org/10.1007/978-3-540-30579-8_27}.

\bibitem{siegel2007verifying}
S.~F. Siegel.
\newblock Verifying parallel programs with mpi-spin.
\newblock In F.~Cappello, T.~Herault, and J.~Dongarra, editors, {\em Recent
  Advances in Parallel Virtual Machine and Message Passing Interface}, pages
  13--14, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg.

\bibitem{Siegel:2005:MWM:1065944.1065957}
S.~F. Siegel and G.~S. Avrunin.
\newblock Modeling wildcard-free mpi programs for verification.
\newblock In {\em Proceedings of the Tenth ACM SIGPLAN Symposium on Principles
  and Practice of Parallel Programming}, PPoPP '05, pages 95--106, New York,
  NY, USA, 2005. ACM.
\newblock \url{http://doi.acm.org/10.1145/1065944.1065957}.

\bibitem{siegel-etal:2015:civl_sc}
S.~F. Siegel, M.~Zheng, Z.~Luo, T.~K. Zirkel, A.~V. Marianiello, J.~G.
  Edenhofner, M.~B. Dwyer, and M.~S. Rogers.
\newblock {CIVL}: The {C}oncurrency {I}ntermediate {V}erification {L}anguage.
\newblock In {\em Proceedings of the International Conference for High
  Performance Computing, Networking, Storage and Analysis}, SC '15, pages
  61:1--61:12, New York, 2015. ACM.
\newblock \url{http://doi.acm.org/10.1145/2807591.2807635}.

\bibitem{siegel2011tass}
S.~F. Siegel and T.~K. Zirkel.
\newblock {TASS}: The {T}oolkit for {A}ccurate {S}cientific {S}oftware.
\newblock {\em Mathematics in Computer Science}, 5(4):395--426, 2011.
\newblock \url{https://doi.org/10.1007/s11786-011-0100-7}.

\bibitem{10.1007/978-3-642-27940-9_27}
S.~F. Siegel and T.~K. Zirkel.
\newblock {L}oop {I}nvariant {S}ymbolic {E}xecution for {P}arallel {P}rograms.
\newblock In V.~Kuncak and A.~Rybalchenko, editors, {\em Verification, Model
  Checking, and Abstract Interpretation}, pages 412--427, Berlin, Heidelberg,
  2012. Springer Berlin Heidelberg.
\newblock \url{https://doi.org/10.1007/978-3-642-27940-9_27}.

\bibitem{Stark:1985:PTR:646823.706907}
E.~W. Stark.
\newblock A {P}roof {T}echnique for {R}ely/{G}uarantee {P}roperties.
\newblock In {\em Proceedings of the Fifth Conference on Foundations of
  Software Technology and Theoretical Computer Science}, pages 369--391,
  Berlin, Heidelberg, 1985. Springer-Verlag.

\bibitem{Strout:2006:DAM:1156433.1157634}
M.~M. Strout, B.~Kreaseck, and P.~D. Hovland.
\newblock {D}ata-{F}low {A}nalysis for {MPI} {P}rograms.
\newblock In {\em Proceedings of the 2006 International Conference on Parallel
  Processing}, ICPP '06, pages 175--184, Washington, DC, USA, 2006. IEEE
  Computer Society.
\newblock \url{http://dx.doi.org/10.1109/ICPP.2006.32}.

\bibitem{Takaoka:1994:PPV:326619.326811}
T.~Takaoka.
\newblock {P}arallel {P}rogram {V}erification with {D}irected {G}raphs.
\newblock In {\em Proceedings of the 1994 ACM Symposium on Applied Computing},
  SAC '94, pages 462--466, New York, NY, USA, 1994. ACM.
\newblock \url{http://doi.acm.org/10.1145/326619.326811}.

\bibitem{Thakur:2005:OCC:2747766.2747771}
R.~Thakur, R.~Rabenseifner, and W.~Gropp.
\newblock {O}ptimization of {C}ollective {C}ommunication {O}perations in
  {MPICH}.
\newblock {\em Int. J. High Perform. Comput. Appl.}, 19(1):49--66, Feb. 2005.

\bibitem{jesper2019optimal}
J.~L. {Träff}.
\newblock {O}n {O}ptimal {T}rees for {I}rregular {G}ather and {S}catter
  {C}ollectives.
\newblock {\em IEEE Transactions on Parallel and Distributed Systems},
  30(9):2060--2074, Sep. 2019.

\bibitem{vakkalanka2008dynamic}
S.~Vakkalanka, G.~Gopalakrishnan, and R.~M. Kirby.
\newblock {D}ynamic {V}erification of {MPI} {P}rograms with {R}eductions in
  {P}resence of {S}plit {O}perations and {R}elaxed {O}rderings.
\newblock In A.~Gupta and S.~Malik, editors, {\em Computer Aided Verification},
  pages 66--79, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg.
\newblock \url{https://doi.org/10.1007/978-3-540-70545-1\_9}.

\bibitem{valiev:2010:nwchem}
M.~Valiev, E.~Bylaska, N.~Govind, K.~Kowalski, T.~Straatsma, H.~V. Dam,
  D.~Wang, J.~Nieplocha, E.~Apra, T.~Windus, and W.~de~Jong.
\newblock {NWC}hem: {A} comprehensive and scalable open-source solution for
  large scale molecular simulations.
\newblock {\em Computer Physics Communications}, 181(9):1477 -- 1489, 2010.
\newblock
  \url{http://www.sciencedirect.com/science/article/pii/S0010465510001438}.

\bibitem{Valmari1992}
A.~Valmari.
\newblock A stubborn attack on state explosion.
\newblock {\em Formal Methods in System Design}, 1(4):297--322, Dec 1992.
\newblock https://doi.org/10.1007/BF00709154.

\bibitem{vandevoorde:1994:specializedprocedures}
M.~T. Vandevoorde and J.~V. Guttag.
\newblock Using specialized procedures and specification-based analysis to
  reduce the runtime costs of modularity.
\newblock In {\em In Proceedings of the 1994 ACM/SIGSOFT Foundations of
  Software Engineering Conference}, pages 121--127, 1994.
\newblock
  \url{https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.56.7940}.

\bibitem{Vo:2010:SDD:1884643.1884681}
A.~Vo, S.~Aananthakrishnan, G.~Gopalakrishnan, B.~R.~d. Supinski, M.~Schulz,
  and G.~Bronevetsky.
\newblock A scalable and distributed dynamic formal verifier for mpi programs.
\newblock In {\em Proceedings of the 2010 ACM/IEEE International Conference for
  High Performance Computing, Networking, Storage and Analysis}, SC '10, pages
  1--10, Washington, DC, USA, 2010. IEEE Computer Society.

\bibitem{yang-etal:2017:amg}
U.~Yang, R.~Falgout, and J.~Park.
\newblock {A}lgebraic {M}ultigrid {B}enchmark, {V}ersion 00, 8 2017.
\newblock \url{https://www.osti.gov//servlets/purl/1389816}.

\bibitem{ye:2018:detecting}
F.~Ye, J.~Zhao, and V.~Sarkar.
\newblock {D}etecting {MPI} {U}sage {A}nomalies via {P}artial {P}rogram
  {S}ymbolic {E}xecution.
\newblock In {\em Proceedings of the International Conference for High
  Performance Computing, Networking, Storage, and Analysis}, SC '18, pages
  63:1--63:5, Piscataway, NJ, USA, 2018. IEEE Press.
\newblock \url{https://doi.org/10.1109/SC.2018.00066}.

\bibitem{Yu:2018:CSE:3183440.3190336}
H.~Yu.
\newblock Combining symbolic execution and model checking to verify mpi
  programs.
\newblock In {\em Proceedings of the 40th International Conference on Software
  Engineering: Companion Proceeedings}, ICSE '18, pages 527--530, New York, NY,
  USA, 2018. ACM.
\newblock \url{http://doi.acm.org/10.1145/3183440.3190336}.

\bibitem{zheng-etal:2016:civl_tacas}
M.~Zheng, J.~G. Edenhofner, Z.~Luo, M.~J. Gerrard, M.~S. Rogers, M.~B. Dwyer, ,
  and S.~F. Siegel.
\newblock {CIVL}: Applying a general concurrency verification framework to
  c/pthreads programs (competition contribution).
\newblock In {\em TACAS 16: International Conference on Tools and Algorithms
  for the Construction and Analysis of Systems, Proceedings}, TACAS '16,
  Eindhoven, The Netherlands, Apr 2016. Springer-Verlag.

\bibitem{zheng-etal:2015:civl_ase}
M.~Zheng, M.~S. Rogers, Z.~Luo, M.~B. Dwyer, and S.~F. Siegel.
\newblock {CIVL}: Formal verification of parallel programs.
\newblock In {\em ASE 2015: 30th IEEE/ACM International Conference on Automated
  Software Engineering, Proceedings}, ASE '15, Piscataway, NJ, USA, Nov 2015.
  IEEE Press.

\bibitem{zheng:2008:test}
W.~{Zheng} and G.~{Bundell}.
\newblock {T}est by {C}ontract for {UML}-{B}ased {S}oftware {C}omponent
  {T}esting.
\newblock In {\em International Symposium on Computer Science and its
  Applications}, pages 377--382, Oct 2008.
\newblock \url{http://doi.org/10.1109/CSA.2008.66}.

\end{thebibliography}