%%%%%%%%%%%%%%%%%%% INTRODUCTION %%%%%%%%%%%%%%%%%%%%%% %% contract, assertion @inproceedings{araujo:2011:enabling, author = {Araujo, Wladimir and Briand, Lionel C. and Labiche, Yvan}, title = {{E}nabling the {R}untime {A}ssertion {C}hecking of {C}oncurrent {C}ontracts for the {J}ava {M}odeling {L}anguage}, booktitle = {Proceedings of the 33rd International Conference on Software Engineering}, series = {ICSE '11}, year = {2011}, isbn = {978-1-4503-0445-0}, location = {Waikiki, Honolulu, HI, USA}, pages = {786--795}, numpages = {10}, url = {http://doi.acm.org/10.1145/1985793.1985903}, note = {\url{http://doi.acm.org/10.1145/1985793.1985903}}, doi = {10.1145/1985793.1985903}, acmid = {1985903}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {concurrency, design by contract, java, jml, object-oriented programming}, } %% contract, runtime checking @inproceedings{rebelo:2014:aspectjml, author = {Reb\^{e}lo, Henrique and Leavens, Gary T. and Bagherzadeh, Mehdi and Rajan, Hridesh and Lima, Ricardo and Zimmerman, Daniel M. and Corn{\'e}lio, M\'{a}rcio and Th\"{u}m, Thomas}, title = {{A}spect{JML}: {M}odular {S}pecification and {R}untime {C}hecking for {C}rosscutting {C}ontracts}, booktitle = {Proceedings of the 13th International Conference on Modularity}, series = {MODULARITY '14}, year = {2014}, isbn = {978-1-4503-2772-5}, location = {Lugano, Switzerland}, pages = {157--168}, numpages = {12}, url = {http://doi.acm.org/10.1145/2577080.2577084}, note = {\url{http://doi.acm.org/10.1145/2577080.2577084}}, doi = {10.1145/2577080.2577084}, acmid = {2577084}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {aspect-oriented programming, aspectj, aspectjml, crosscutting contracts, design by contract, jml}, } %% contract, test case @INPROCEEDINGS{zheng:2008:test, author={W. {Zheng} and G. {Bundell}}, booktitle={International Symposium on Computer Science and its Applications}, title={{T}est by {C}ontract for {UML}-{B}ased {S}oftware {C}omponent {T}esting}, year={2008}, volume={}, number={}, pages={377-382}, keywords={program testing;Unified Modeling Language;test by contract;UML;software component testing;Contracts;Unified modeling language;Testing;Software;Control systems;Context modeling;Construction industry;Test by Contract;Contract for Testability;test contract;effectual contract scope;test criteria;contract-based test design}, doi={10.1109/CSA.2008.66}, note={\url{http://doi.org/10.1109/CSA.2008.66}}, ISSN={}, month={Oct},} %% contract, test case @article{krenn:2009:test, title = "{T}est {C}ase {G}eneration by {C}ontract {M}utation in {S}pec{\#}", journal = "Electronic Notes in Theoretical Computer Science", volume = "253", number = "2", pages = "71 - 86", year = "2009", booktitle = "Proceedings of Fifth Workshop on Model Based Testing (MBT 2009)", issn = "1571-0661", doi = "https://doi.org/10.1016/j.entcs.2009.09.052", url = "http://www.sciencedirect.com/science/article/pii/S157106610900406X", note = {\url{http://www.sciencedirect.com/science/article/pii/S157106610900406X}}, author = "Willibald Krenn and Bernhard K. Aichernig", keywords = "test case generation, mutation testing, contract mutation, Spec#, Boogie, Z3", abstract = "Mutation testing is a well known fault-based testing technique that is normally used to assess the quality of a test suite. In this paper we use the mutation operation to derive test cases that demonstrate the absence of certain faults in an implementation: In difference to conventional mutation testing, which mutates program code, we mutate program contracts and generate test-input data that is able to distinguish the mutated contract from the original one. We show how existing development tools can be used as a foundation for the presented methodology: In particular we rely on the counter-example generation capabilities of the Spec#/Boogie/Z3 system." } %% 1982dannenberg, @ARTICLE{dannenberg:1982:formal, author={R. B. {Dannenberg} and G. W. {Ernst}}, journal={IEEE Transactions on Software Engineering}, title={{F}ormal {P}rogram {V}erification {U}sing {S}ymbolic {E}xecution}, year={1982}, volume={SE-8}, number={1}, pages={43-52}, keywords={Control constructs;program proving;program verification;rules of inference;side effects;symbolic execution;verification conditions;Logic;Calculus;Computer science;Computer languages;Control constructs;program proving;program verification;rules of inference;side effects;symbolic execution;verification conditions}, doi={10.1109/TSE.1982.234773}, note={\url{10.1109/TSE.1982.234773}}, ISSN={}, month={Jan},} %% Leavens1999, @Inbook{leavens:1999:jml, author="Leavens, Gary T. and Baker, Albert L. and Ruby, Clyde", noe_editor="Kilov, Haim and Rumpe, Bernhard and Simmonds, Ian", title="{JML}: {A} {N}otation for {D}etailed {D}esign", bookTitle="Behavioral Specifications of Businesses and Systems", year="1999", publisher="Springer US", address="Boston, MA", pages="175--188", abstract="JML is a behavioral interface specification language tailored to Java. It is designed to be written and read by working software engineers, and should require only modest mathematical training. It uses Eiffel-style syntax combined with model-based semantics, as in VDM and Larch. JML supports quantifiers, specification-only variables, and other enhancements that make it more expressive for specification than Eiffel and easier to use than VDM and Larch.", isbn="978-1-4615-5229-1", doi="10.1007/978-1-4615-5229-1_12", url="https://doi.org/10.1007/978-1-4615-5229-1_12", note="\url{https://doi.org/10.1007/978-1-4615-5229-1_12}", } %% Vandevoorde94usingspecialized @INPROCEEDINGS{vandevoorde:1994:specializedprocedures, author = {Mark T. Vandevoorde and John V. Guttag}, title = {Using Specialized Procedures and Specification-Based Analysis to Reduce the Runtime Costs of Modularity}, booktitle = {In Proceedings of the 1994 ACM/SIGSOFT Foundations of Software Engineering Conference}, year = {1994}, pages = {121--127}, note={\url{https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.56.7940}}, } %% Mathuriya:2017:ENE:3126908.3126952 @inproceedings{mathuriya:2017:embracingquantum, author = {Mathuriya, Amrita and Luo, Ye and Clay,III, Raymond C. and Benali, Anouar and Shulenburger, Luke and Kim, Jeongnim}, title = {{E}mbracing a {N}ew {E}ra of {H}ighly {E}fficient and {P}roductive {Q}uantum {M}onte {C}arlo {S}imulations}, booktitle = {Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis}, series = {SC '17}, year = {2017}, isbn = {978-1-4503-5114-0}, location = {Denver, Colorado}, pages = {38:1--38:12}, articleno = {38}, numpages = {12}, url = {http://doi.acm.org/10.1145/3126908.3126952}, note = {\url{http://doi.acm.org/10.1145/3126908.3126952}}, doi = {10.1145/3126908.3126952}, acmid = {3126952}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {CPUs, QMC, optimizations, portability, vectorization}, } %% VALIEV20101477 @article{valiev:2010:nwchem, title = "{NWC}hem: {A} comprehensive and scalable open-source solution for large scale molecular simulations", journal = "Computer Physics Communications", volume = "181", number = "9", pages = "1477 - 1489", year = "2010", issn = "0010-4655", doi = "https://doi.org/10.1016/j.cpc.2010.04.018", url = "http://www.sciencedirect.com/science/article/pii/S0010465510001438", note = "\url{http://www.sciencedirect.com/science/article/pii/S0010465510001438}", author = "M. Valiev and E.J. Bylaska and N. Govind and K. Kowalski and T.P. Straatsma and H.J.J. Van Dam and D. Wang and J. Nieplocha and E. Apra and T.L. Windus and W.A. de Jong", keywords = "NWChem, DFT, Coupled cluster, QMMM, Plane wave methods", abstract = "The latest release of NWChem delivers an open-source computational chemistry package with extensive capabilities for large scale simulations of chemical and biological systems. Utilizing a common computational framework, diverse theoretical descriptions can be used to provide the best solution for a given scientific problem. Scalable parallel implementations and modular software design enable efficient utilization of current computational architectures. This paper provides an overview of NWChem focusing primarily on the core theoretical modules provided by the code and their parallel performance. Program summary Program title: NWChem Catalogue identifier: AEGI_v1_0 Program summary URL: http://cpc.cs.qub.ac.uk/summaries/AEGI_v1_0.html Program obtainable from: CPC Program Library, Queen's University, Belfast, N. Ireland Licensing provisions: Open Source Educational Community License No. of lines in distributed program, including test data, etc.: 11 709 543 No. of bytes in distributed program, including test data, etc.: 680 696 106 Distribution format: tar.gz Programming language: Fortran 77, C Computer: all Linux based workstations and parallel supercomputers, Windows and Apple machines Operating system: Linux, OS X, Windows Has the code been vectorised or parallelized?: Code is parallelized Classification: 2.1, 2.2, 3, 7.3, 7.7, 16.1, 16.2, 16.3, 16.10, 16.13 Nature of problem: Large-scale atomistic simulations of chemical and biological systems require efficient and reliable methods for ground and excited solutions of many-electron Hamiltonian, analysis of the potential energy surface, and dynamics. Solution method: Ground and excited solutions of many-electron Hamiltonian are obtained utilizing density-functional theory, many-body perturbation approach, and coupled cluster expansion. These solutions or a combination thereof with classical descriptions are then used to analyze potential energy surface and perform dynamical simulations. Additional comments: Full documentation is provided in the distribution file. This includes an INSTALL file giving details of how to build the package. A set of test runs is provided in the examples directory. The distribution file for this program is over 90 Mbytes and therefore is not delivered directly when download or Email is requested. Instead a html file giving details of how the program can be obtained is sent. Running time: Running time depends on the size of the chemical system, complexity of the method, number of cpu's and the computational task. It ranges from several seconds for serial DFT energy calculations on a few atoms to several hours for parallel coupled cluster energy calculations on tens of atoms or ab-initio molecular dynamics simulation on hundreds of atoms." } %% 8024093, @ARTICLE{johansen:2017:earthquake, author={H. {Johansen} and A. {Rodgers} and N. A. {Petersson} and D. {McCallen} and B. {Sjogreen} and M. {Miah}}, journal={Computing in Science Engineering}, title={{T}oward {E}xascale {E}arthquake {G}round {M}otion {S}imulations for {N}ear-{F}ault {E}ngineering {A}nalysis}, year={2017}, volume={19}, number={5}, pages={27-37}, keywords={critical infrastructures;digital simulation;earthquake engineering;faulting;geophysics computing;mesh generation;seismic waves;solid modelling;Lawrence Berkeley national laboratory;NERSC;national energy research scientific computing center;Cori Phase 2;SMR;surface-focused structured mesh refinement;critical infrastructure risk evaluations;ground motion estimates;3D earth models;massively parallel time-domain simulations;seismic waves 4th order;SW4 algorithm;near-fault engineering analysis;exascale earthquake ground motion simulations;Earthquakes;Solid modeling;Computational modeling;Three-dimensional displays;Geology;Analytical models;Motion control;computational seismology;structural mechanics;earthquake simulations;exascale computing;scientific computing}, doi={10.1109/MCSE.2017.3421558}, note={\url{http://doi.org/10.1109/MCSE.2017.3421558}}, ISSN={}, month={},} @ARTICLE{2017:johansen:toward, author={H. {Johansen} and A. {Rodgers} and N. A. {Petersson} and D. {McCallen} and B. {Sjogreen} and M. {Miah}}, journal={Computing in Science Engineering}, title={{T}oward {E}xascale {E}arthquake {G}round {M}otion {S}imulations for {N}ear-{F}ault {E}ngineering {A}nalysis}, year={2017}, volume={19}, number={5}, pages={27-37}, keywords={critical infrastructures;digital simulation;earthquake engineering;faulting;geophysics computing;mesh generation;seismic waves;solid modelling;Lawrence Berkeley national laboratory;NERSC;national energy research scientific computing center;Cori Phase 2;SMR;surface-focused structured mesh refinement;critical infrastructure risk evaluations;ground motion estimates;3D earth models;massively parallel time-domain simulations;seismic waves 4th order;SW4 algorithm;near-fault engineering analysis;exascale earthquake ground motion simulations;Earthquakes;Solid modeling;Computational modeling;Three-dimensional displays;Geology;Analytical models;Motion control;computational seismology;structural mechanics;earthquake simulations;exascale computing;scientific computing}, doi={10.1109/MCSE.2017.3421558}, note={\url{http://doi.org/10.1109/MCSE.2017.3421558}}, ISSN={}, month={},} @proceedings{correctness:2017:proceedings, title = {{C}orrectness'17: Proceedings of the First International Workshop on Software Correctness for HPC Applications}, year = {2017}, isbn = {978-1-4503-5127-0}, location = {Denver, CO, USA}, publisher = {ACM}, address = {New York, NY, USA}, note = {\url{https://correctness-workshop.github.io/2017/}}, key={correctness 17}, } @proceedings {correctness:2018:proceedings, author = {}, key={correctness 18}, booktitle = {2018 IEEE/ACM 2nd International Workshop on Software Correctness for HPC Applications (Correctness)}, title = {{C}orrectness'18: Proceedings of the Second International Workshop on Software Correctness for HPC Applications}, year = {2018}, volume = {}, issn = {}, pages = {5-6}, keywords = {}, doi = {10.1109/Correctness.2018.00004}, url = {https://doi.ieeecomputersociety.org/10.1109/Correctness.2018.00004}, note = {\url{https://doi.ieeecomputersociety.org/10.1109/Correctness.2018.00004}}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, month = {nov} } @article{hatton:1997:T_Experiments, Author = {Les Hatton}, Date-Added = {2008-07-13 16:40:50 -0400}, Date-Modified = {2008-07-13 16:40:51 -0400}, Journal = {IEEE Computational Science \& Engineering}, Month = apr, Number = 2, Pages = {27--38}, Publisher = {IEEE}, Title = {The {T} Experiments: Errors in Scientific Software}, Volume = 4, Year = 1997} @article{hatton-roberts:1994:accurate, Author = {Les Hatton and Andy Roberts}, Date-Added = {2008-07-13 16:40:50 -0400}, Date-Modified = {2008-07-13 16:40:51 -0400}, Journal = {{IEEE} {T}ransactions on {S}oftware {E}ngineering}, Month = oct, Number = 10, Pages = {785--797}, Publisher = {IEEE}, Title = {How Accurate is Scientific Software?}, Volume = 20, Year = 1994} @incollection{hatton:2012:defects, year={2012}, isbn={978-3-642-32676-9}, booktitle={Uncertainty Quantification in Scientific Computing}, volume={377}, series={IFIP Advances in Information and Communication Technology}, editor={Dienstfrey, Andrew M. and Boisvert, Ronald F.}, title={Defects, Scientific Computation and the Scientific Method}, publisher={Springer Berlin Heidelberg}, keywords={Scientific method; reproducibility; unquantifiable computation}, author={Hatton, Les}, pages={123--138} } @article{merali:2010:error, title={{E}rror: why scientific programming does not compute}, author={Merali, Zeeya}, journal={Nature}, volume={467}, number={7317}, pages={775--777}, year={2010}, } @misc{mpi-forum:2015:mpi31, Author = {{Message Passing Interface Forum}}, Howpublished = {\url{https://www.mpi-forum.org/docs/mpi-3.1/mpi31-report.pdf}}, Month = jun, Day = 4, Title = {{MPI}: A {M}essage-{P}assing {I}nterface Standard, Version 3.1}, Year = 2015, } %% Clarke:2000:MC:332656 @book{clarke:2000:modelchecking, author = {Clarke,Jr., Edmund M. and Grumberg, Orna and Peled, Doron A.}, title = {{M}odel {C}hecking}, year = {1999}, isbn = {0-262-03270-8}, publisher = {MIT Press}, address = {Cambridge, MA, USA}, } @TechReport{bernholdt-etal:2018:mpi_exascale, title = {{A} {S}urvey of {MPI} {U}sage in the {U.S.}\ {E}xascale {C}omputing {P}roject}, author = {Bernholdt, David E. and Boehm, Swen and Bosilca, George and Gorentla Venkata, Manjunath and Grant, Ryan E. and Naughton, III, Thomas J. and Pritchard, Howard P. and Schulz, Martin and Vallee, Geoffroy R.}, abstractNote = {The Exascale Computing Project (ECP) is currently the primary effort in the United States focused on developing “exascale” levels of computing capability, including hardware, software and applications. In order to obtain a more thorough understanding of how the software projects under the ECP are using, and planning to use the Message Passing Interface (MPI), and help guide the work of our own project within the ECP, we created a survey. Of the 97 ECP projects active at the time the survey was distributed, we received 77 responses, 56 of which reported that their projects were using MPI. This paper reports the results of that survey for the benefit of the broader community of MPI developers}, doi = {10.2172/1462877}, note = {\url{https://doi.org/10.2172/1462877}}, number = {790}, volume = {SPR-2018}, journal = {ORNL}, institution = {Oak Ridge National Lab.}, place = {United States}, year = {2018}, month = jun } @TechReport{gopalakrishnan-etal:2017:correctness, place={Washington, DC}, title={{R}eport of the {HPC} {C}orrectness {S}ummit}, journal={Report of the HPC Correctness Summit}, author={Gopalakrishnan, Ganesh and Hovland, Paul D. and Iancu, Costin and Krishnamoorthy, Sriram and Laguna, Ignacio and Lethin, Richard A. and Sen, Koushik and Siegel, Stephen F. and Solar-Lezama, Armando}, year={2017}, note = {\url{https://arxiv.org/abs/1705.07478}}, institution={USDOE Office of Science (SC)}, } %%petsc-user-ref @TechReport{balay:2019:petsc, author = {Satish Balay and Shrirang Abhyankar and Mark~F. Adams and Jed Brown and Peter Brune and Kris Buschelman and Lisandro Dalcin and Alp Dener and Victor Eijkhout and William~D. Gropp and Dmitry Karpeyev and Dinesh Kaushik and Matthew~G. Knepley and Dave~A. May and Lois Curfman McInnes and Richard Tran Mills and Todd Munson and Karl Rupp and Patrick Sanan and Barry~F. Smith and Stefano Zampini and Hong Zhang and Hong Zhang}, title = {{PETS}c {U}sers {M}anual}, institution = {Argonne National Laboratory}, year = 2019, number = {ANL-95/11 - Revision 3.12}, note = {\url{https://www.mcs.anl.gov/petsc}} } %% Drake2005OverviewOT @article{drake:2005:overview, title={{O}verview of the {S}oftware {D}esign of the {C}ommunity {C}limate {S}ystem {M}odel}, author={John B. Drake and Philip W. Jones and George R. Carr}, journal={IJHPCA}, year={2005}, volume={19}, pages={177-186}, note = {\url{https://journals.sagepub.com/doi/pdf/10.1177/1094342005056094}}, } @article{Pervez:2010:FMA:1712067.1712069, author = {Pervez, Salman and Gopalakrishnan, Ganesh and Kirby, Robert M. and Thakur, Rajeev and Gropp, William}, title = {{F}ormal {M}ethods {A}pplied to {H}igh-performance {C}omputing {S}oftware {D}esign: {A} {C}ase {S}tudy of {MPI} {O}ne-sided {C}ommunication-based {L}ocking}, journal = {Softw. Pract. Exper.}, issue_date = {January 2010}, volume = {40}, number = {1}, month = jan, year = {2010}, issn = {0038-0644}, pages = {23--43}, numpages = {21}, url = {http://dx.doi.org/10.1002/spe.v40:1}, note = {\url{http://dx.doi.org/10.1002/spe.v40:1}}, doi = {10.1002/spe.v40:1}, acmid = {1712069}, publisher = {John Wiley \& Sons, Inc.}, address = {New York, NY, USA}, keywords = {Message Passing Interface (MPI), SPIN, concurrent programming, dynamic analysis, formal verification, high-performance computing (HPC), model checking, one-sided communication, race condition}, } @techreport{godefroid2008concurrency, author = {Godefroid, Patrice and Nagappan, Nachi}, title = {Concurrency at Microsoft - An Exploratory Survey}, year = {2008}, month = {May}, url = {https://www.microsoft.com/en-us/research/publication/concurrency-at-microsoft-an-exploratory-survey/}, note = {\url{https://www.microsoft.com/en-us/research/publication/concurrency-at-microsoft-an-exploratory-survey/}}, pages = {4}, number = {MSR-TR-2008-75}, institution = {Microsoft}, } @book{Jackson:2006:SAL, author = {Jackson, Daniel}, title = {Software Abstractions: Logic, Language, and Analysis}, year = {2006}, isbn = {0262101149}, publisher = {The MIT Press}, } @InProceedings{godefroid:1993:refining, author="Godefroid, Patrice and Pirottin, Didier", editor="Courcoubetis, Costas", title="Refining dependencies improves partial-order verification methods (extended abstract)", booktitle="Computer Aided Verification", year="1993", publisher="Springer Berlin Heidelberg", address="Berlin, Heidelberg", pages="438--449", abstract="Partial-order verification methods exploit ``independency'' between transitions of a concurrent program to avoid parts of the state space explosion due to the modeling of concurrency by interleaving. In this paper, we study the influence of refining dependencies between transitions of the program on the effectiveness of these methods. We show that carefully tracking dependencies can yield substantial improvements for their performances. For instance, we were able to decrease the memory requirements needed for the verification of a real-size protocol with such a method from a factor of 5 to a factor of 25 by only refining dependencies.", isbn="978-3-540-47787-7" } @InProceedings{10.1007/BFb0013032, author="Katz, Shmuel and Peled, Doron", editor="de Bakker, J. W. and de Roever, W. -P. and Rozenberg, G.", title="{A}n efficient verification method for parallel and distributed programs", booktitle="Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency", year="1989", publisher="Springer Berlin Heidelberg", address="Berlin, Heidelberg", pages="489--507", abstract="We present a formal proof method which is based on a partial order semantics for parallel or distributed programs. In this view, a program's semantics is given by a collection of partial orders of the events which can occur during execution. Rather than using the partial orders directly, the basis of the method assumes the sets of (linear) execution sequences with global states which are consistent with each partial order (each such set is called an interleaving set). The proof rules allow concluding the correctness of certain classes of properties for all execution sequences, even though the property is only demonstrated directly for a subset of the execution sequences. The subset used must include a representative sequence from each interleaving set, and the proof rules guarantee that this is the case when they may be applied. The method employs proof lattices, and is expressed using the temporal logic ISTL*. By choosing a subset with appropriate sequences, simpler intermediate assertions can be used than in previous formal approaches. Moreover, since less direct checking must be done, the method is often much more efficient.", isbn="978-3-540-46147-0", note={\url{https://doi.org/10.1007/BFb0013032}}, } @Article{Valmari1992, author="Valmari, Antti", title="A stubborn attack on state explosion", journal="Formal Methods in System Design", year="1992", month="Dec", day="01", volume="1", number="4", pages="297--322", abstract="This article presents theLTL-preserving stubborn set method for reducing the amount of work needed in the automatic verification of concurrent systems with respect to linear-time temporal logic specifications. The method facilitates the generation ofreduced state spaces such that the truth values of linear temporal logic formulas are the same in the ordinary and reduced state spaces. The only restrictions posed by the method are 1) the formulas must be known before the reduced state-space generation is commenced; 2) the use of the temporal operator ``next state'' is prohibited; and 3) the (reduced) state space of the system must be finite. The method cuts down the number of states by utilizing the fact that in concurrent systems the net result of the occurrence of two events is often independent of the order of occurrence.", issn="1572-8102", doi="10.1007/BF00709154", url="https://doi.org/10.1007/BF00709154", note="https://doi.org/10.1007/BF00709154", } %% king1976symbolic @article{king:1976:symbolic, title={{S}ymbolic execution and program testing}, author={King, James C}, journal={Communications of the ACM}, volume={19}, number={7}, pages={385--394}, year={1976}, publisher={ACM}, note = {\url{https://doi.org/10.1145/360248.360252}}, } %% hoare1969axiomatic @article{hoare:1969:axiomatic, title={{A}n axiomatic basis for computer programming}, author={Hoare, Charles Antony Richard}, journal={Communications of the {ACM}}, volume={12}, number={10}, pages={576--580}, year={1969}, publisher={ACM} } %% Gordon1989, @Inbook{gordon:1989:mechanizing, author="Gordon, Michael J. C.", noe_editor="Birtwistle, Graham and Subrahmanyam, P. A.", title="Mechanizing Programming Logics in Higher Order Logic", bookTitle="Current Trends in Hardware Verification and Automated Theorem Proving", year="1989", publisher="Springer New York", address="New York, NY", pages="387--439", abstract="Formal reasoning about computer programs can be based directly on the semantics of the programming language, or done in a special purpose logic like Hoare logic. The advantage of the first approach is that it guarantees that the formal reasoning applies to the language being used (it is well known, for example, that Hoare's assignment axiom fails to hold for most programming languages). The advantage of the second approach is that the proofs can be more direct and natural.", isbn="978-1-4612-3658-0", doi="10.1007/978-1-4612-3658-0_10", url="https://doi.org/10.1007/978-1-4612-3658-0_10", note={\url{https://doi.org/10.1007/978-1-4612-3658-0_10}}, } %% Leino:1999:CJP:646779.704969 @inproceedings{leino:1999:checkingjava, author = {Leino, K. Rustan M. and Saxe, James B. and Stata, Raymie}, title = {Checking Java Programs via Guarded Commands}, booktitle = {Proceedings of the Workshop on Object-Oriented Technology}, year = {1999}, isbn = {3-540-66954-X}, pages = {110--111}, numpages = {2}, url = {http://dl.acm.org/citation.cfm?id=646779.704969}, note = {\url{http://dl.acm.org/citation.cfm?id=646779.704969}}, acmid = {704969}, publisher = {Springer-Verlag}, address = {London, UK, UK}, } %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%% %%%%%%% %%%%%%% related work %%%%%%% %%%%%%% %%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @book{armstrong:2013:programming, title={{P}rogramming {E}rlang: {S}oftware for a {C}oncurrent {W}orld}, author={Armstrong, Joe}, year={2013}, publisher={Pragmatic Bookshelf} } @book{Gosling:2014:JLS:2636997, author = {Gosling, James and Joy, Bill and Steele, Guy L. and Bracha, Gilad and Buckley, Alex}, title = {{T}he {J}ava {L}anguage {S}pecification, {J}ava {SE} 8 {E}dition}, year = {2014}, isbn = {013390069X, 9780133900699}, edition = {1st}, publisher = {Addison-Wesley Professional}, } @inproceedings{reynolds2002separation, author={J.\ C.\ {R}eynolds}, booktitle={Proceedings 17th Annual IEEE Symposium on Logic in Computer Science}, title={{S}eparation {L}ogic: a {L}ogic for {S}hared {M}utable {D}ata {S}tructures}, year={2002}, volume={}, number={}, pages={55-74}, keywords={formal logic;computational complexity;data structures;separation logic;shared mutable data structures;Hoare logic;reasoning;low-level imperative programs;imperative programming language;heap;program logic;address arithmetic;recursive procedures;Data structures;Computer science;Programmable logic arrays;Reflection;Logic programming;Computer languages;Logic arrays;Arithmetic;Artificial intelligence;Bibliographies}, doi={10.1109/LICS.2002.1029817}, note={\url{http://doi.org/10.1109/LICS.2002.1029817}}, ISSN={}, month={July},} @inproceedings{Jacobs:2010:QTV:1947873.1947902, author = {Jacobs, Bart and Smans, Jan and Piessens, Frank}, title = {A Quick Tour of the VeriFast Program Verifier}, booktitle = {Proceedings of the 8th Asian Conference on Programming Languages and Systems}, series = {APLAS'10}, year = {2010}, isbn = {3-642-17163-X, 978-3-642-17163-5}, location = {Shanghai, China}, pages = {304--311}, numpages = {8}, url = {http://dl.acm.org/citation.cfm?id=1947873.1947902}, note = {\url{http://dl.acm.org/citation.cfm?id=1947873.1947902}}, acmid = {1947902}, publisher = {Springer-Verlag}, address = {Berlin, Heidelberg}, } %% Leino2009verification @Inbook{leino:2009:verification, author="Leino, K. Rustan M. and M{\"u}ller, Peter and Smans, Jan", note_editor="Aldini, Alessandro and Barthe, Gilles and Gorrieri, Roberto", title="{V}erification of {C}oncurrent {P}rograms with {C}halice", bookTitle="Foundations of Security Analysis and Design V: FOSAD 2007/2008/2009 Tutorial Lectures", year="2009", publisher="Springer Berlin Heidelberg", address="Berlin, Heidelberg", pages="195--222", abstract="A program verifier is a tool that allows developers to prove that their code satisfies its specification for every possible input and every thread schedule. These lecture notes describe a verifier for concurrent programs called Chalice.", isbn="978-3-642-03829-7", doi="10.1007/978-3-642-03829-7_7", url="https://doi.org/10.1007/978-3-642-03829-7_7", note={\url{https://doi.org/10.1007/978-3-642-03829-7_7}}, } %% Amani:2017:CVF:3018610.3018627 @inproceedings{amani:2017:complex, author = {Amani, Sidney and Andronick, June and Bortin, Maksym and Lewis, Corey and Rizkallah, Christine and Tuong, Joseph}, title = {{COMPLEX}: {A} {V}erification {F}ramework for {C}oncurrent {I}mperative {P}rograms}, booktitle = {Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs}, series = {CPP 2017}, year = {2017}, isbn = {978-1-4503-4705-1}, location = {Paris, France}, pages = {138--150}, numpages = {13}, url = {http://doi.acm.org/10.1145/3018610.3018627}, note = {\url{http://doi.acm.org/10.1145/3018610.3018627}}, doi = {10.1145/3018610.3018627}, acmid = {3018627}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {Isabelle/HOL, Owicki-Gries, concurrency, formal verification, imperative code, programming languages}, } @Inbook{Floyd1993, author="Floyd, Robert W.", note_editor="Colburn, Timothy R. and Fetzer, James H. and Rankin, Terry L.", title="{A}ssigning {M}eanings to {P}rograms", bookTitle="Program Verification: Fundamental Issues in Computer Science", year="1993", publisher="Springer Netherlands", address="Dordrecht", pages="65--81", abstract="This paper attempts to provide an adequate basis for formal definitions of the meanings of programs in appropriately defined programming languages, in such a way that a rigorous standard is established for proofs about computer programs, including proofs of correctness, equivalence, and termination. The basis of our approach is the notion of an interpretation of a program: that is, an association of a proposition with each connection in the flow of control through a program, where the proposition is asserted to hold whenever that connection is taken. To prevent an interpretation from being chosen arbitrarily, a condition is imposed on each command of the program. This condition guarantees that whenever a command is reached by way of a connection whose associated proposition is then true, it will be left (if at all) by a connection whose associated proposition will be true at that time. Then by induction on the number of commands executed, one sees that if a program is entered by a connection whose associated proposition is then true, it will be left (if at all) by a connection whose associated proposition will be true at that time. By this means, we may prove certain properties of programs, particularly properties of the form: `If the initial values of the program variables satisfy the relation Rl, the final values on completion will satisfy the relation R2'.", isbn="978-94-011-1793-7", doi="10.1007/978-94-011-1793-7_4", url="https://doi.org/10.1007/978-94-011-1793-7_4", note={\url{https://doi.org/10.1007/978-94-011-1793-7\_4}}, } %% ball:2010:towards @InProceedings{ball:2010:towards, author = {Ball, Tom and Hackett, Brian and Lahiri, Shuvendu and Qadeer, Shaz and Vanegue, Julien}, title = {{T}owards {S}calable {M}odular {C}hecking of {U}ser-{D}efined {P}roperties}, booktitle = {Verified Software: Theories, Tools and Experiments (VSTTE 2010)}, year = {2010}, month = {August}, abstract = {Theorem-prover based modular checkers have the potential to perform scalable and precise checking of user-defined properties by combining path-sensitive intraprocedural reasoning with user-defined procedure abstractions. However, such tools have seldom been deployed on large software applications of industrial relevance due to the annotation burden required to provide the procedure abstractions. In this work, we present two case studies of applying a modular checker HAVOC to check properties on large modules in the Microsoft Windows operating system. The first detailed case study describes checking the synchronization protocol of a core Microsoft Windows component with more than 300 thousand lines of code and 1500 procedures. The effort found 45 serious bugs in the component with modest annotation effort and low false alarms; most of these bugs have since been fixed by the developers of the module. The second case study reports preliminary user experience in using the tool for checking security related properties in several Windows components. We describe our experience in using a modular checker to create various property checkers for finding errors in a well-tested applications of this scale, and our design decisions to find them with low false alarms, modest annotation burden and high coverage.}, publisher = {Springer Verlag}, url = {https://www.microsoft.com/en-us/research/publication/towards-scalable-modular-checking-of-user-defined-properties-2/}, note = {\url{https://www.microsoft.com/en-us/research/publication/towards-scalable-modular-checking-of-user-defined-properties-2/}}, edition = {Verified Software: Theories, Tools and Experiments (VSTTE 2010)}, } @techreport{lahiri2012security, author = {Lahiri, Shuvendu}, title = {{S}ecurity audit using extended static checking: Is it cost-effective yet?}, year = {2012}, month = {October}, abstract = {This paper describes our experience of doing variation analysis of known security vulnerabilities in C++ projects including core OS and browser COM components, using an extended static checker HAVOC-LITE. We describe the extensions made to the tool to be applicable on such large components, along with our experience of using an extended static checker in the large. We argue that the use of such checkers as a configurable static analysis in the hands of security auditors can be quite cost-effective tool for finding variations of known vulnerabilities.}, url = {https://www.microsoft.com/en-us/research/publication/security-audit-using-extended-static-checking-is-it-cost-effective-yet/}, note = {\url{https://www.microsoft.com/en-us/research/publication/security-audit-using-extended-static-checking-is-it-cost-effective-yet/}}, number = {MSR-TR-2012-103}, institution={microsoft}, } @misc{spark, key = {AdaCore and Altran UK Ltd.}, title = {{SPARK} 2014 {R}eference {M}anual}, howpublished = {\url{http://docs.adacore.com/spark2014- docs/html/lrm/}}, note = {Accessed Sep.\ 6, 2019} } @book{Barnes:2012:SPA, author = {Barnes, John}, title = {{S}park: {T}he {P}roven {A}pproach to {H}igh {I}ntegrity {S}oftware}, year = {2012}, isbn = {0957290500, 9780957290501}, publisher = {Altran Praxis}, address = {http://www.altran.co.uk, UK}, note = {\url{http://www.altran.co.uk, UK}}, } %% Cuoq2011functional @Article{cuoq:2011:wp, author="Cuoq, Pascal and Monate, Benjamin and Pacalet, Anne and Prevosto, Virgile", title="Functional dependencies of C functions via weakest pre-conditions", journal="International Journal on Software Tools for Technology Transfer", year="2011", month="Oct", day="01", volume="13", number="5", pages="405--417", abstract="We present functional dependencies, a convenient, formal, but high-level, specification format for a piece of procedural software (function). Functional dependencies specify the set of memory locations, which may be modified by the function, and for each modified location, the set of memory locations that influence its final value. Verifying that a function respects pre-defined functional dependencies can be tricky: the embedded world uses C and Ada, which have arrays and pointers. Existing systems we know of that manipulate functional dependencies, Caveat and SPARK, are restricted to pointer-free subsets of these languages. This article deals with the functional dependencies in a programming language with full aliasing. We show how to use a weakest pre-condition calculus to generate a verification condition for pre-existing functional dependencies requirements. This verification condition can then be checked using automated theorem provers or proof assistants. With our approach, it is possible to verify the specification as it was written beforehand. We assume little about the implementation of the verification condition generator itself. Our study takes place inside the C analysis framework Frama-C, where an experimental implementation of the technique described here has been implemented on top of the WP plug-in in the development version of the tool.", issn="1433-2787", doi="10.1007/s10009-011-0192-z", url="https://doi.org/10.1007/s10009-011-0192-z", note={\url{"https://doi.org/10.1007/s10009-011-0192-z"}}, } %% 10.1007/978-3-540-30569-9_3 @InProceedings{barnett:2005:specsharp, author="Barnett, Mike and Leino, K. Rustan M. and Schulte, Wolfram", editor="Barthe, Gilles and Burdy, Lilian and Huisman, Marieke and Lanet, Jean-Louis and Muntean, Traian", title="The {S}pec{\#} {P}rogramming {S}ystem: {A}n {O}verview", booktitle="Construction and Analysis of Safe, Secure, and Interoperable Smart Devices", year="2005", publisher="Springer Berlin Heidelberg", address="Berlin, Heidelberg", pages="49--69", abstract="The Spec{\#} programming system is a new attempt at a more cost effective way to develop and maintain high-quality software. This paper describes the goals and architecture of the Spec{\#} programming system, consisting of the object-oriented Spec{\#} programming language, the Spec{\#} compiler, and the Boogie static program verifier. The language includes constructs for writing specifications that capture programmer intentions about how methods and data are to be used, the compiler emits run-time checks to enforce these specifications, and the verifier can check the consistency between a program and its specifications.", isbn="978-3-540-30569-9", note={\url{https://doi.org/10.1007/978-3-540-30569-9\_3}}, } @article{Owicki:1982:PLP:357172.357178, author = {Owicki, Susan and Lamport, Leslie}, title = {{P}roving {L}iveness {P}roperties of {C}oncurrent {P}rograms}, journal = {ACM Trans. Program. Lang. Syst.}, issue_date = {July 1982}, volume = {4}, number = {3}, month = jul, year = {1982}, issn = {0164-0925}, pages = {455--495}, numpages = {41}, url = {http://doi.acm.org/10.1145/357172.357178}, doi = {10.1145/357172.357178}, acmid = {357178}, publisher = {ACM}, address = {New York, NY, USA}, } @article{Lamport:1984:HLC:2993.357247, author = {Lamport, Leslie and Schneider, Fred B.}, title = {{T}he ``{H}oare {L}ogic'' of {CSP}, and {A}ll {T}hat}, journal = {ACM Trans. Program. Lang. Syst.}, issue_date = {April 1984}, volume = {6}, number = {2}, month = apr, year = {1984}, issn = {0164-0925}, pages = {281--296}, numpages = {16}, url = {http://doi.acm.org/10.1145/2993.357247}, doi = {10.1145/2993.357247}, acmid = {357247}, publisher = {ACM}, address = {New York, NY, USA}, } @article{lipton:reduction, author = {Lipton, Richard J.}, title = {{R}eduction: {A} {M}ethod of {P}roving {P}roperties of {P}arallel {P}rograms}, journal = {Commun. ACM}, issue_date = {Dec. 1975}, volume = {18}, number = {12}, month = dec, year = {1975}, issn = {0001-0782}, pages = {717--721}, numpages = {5}, url = {http://doi.acm.org/10.1145/361227.361234}, doi = {10.1145/361227.361234}, acmid = {361234}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {computation sequence, deadlock free, indivisible, interruptible, parallel program, process, reduction, semaphore, verification method}, } @inproceedings{Stark:1985:PTR:646823.706907, author = {Stark, Eugene W.}, title = {A {P}roof {T}echnique for {R}ely/{G}uarantee {P}roperties}, booktitle = {Proceedings of the Fifth Conference on Foundations of Software Technology and Theoretical Computer Science}, year = {1985}, isbn = {3-540-16042-6}, pages = {369--391}, numpages = {23}, url = {http://dl.acm.org/citation.cfm?id=646823.706907}, acmid = {706907}, publisher = {Springer-Verlag}, address = {Berlin, Heidelberg}, } @Article{Newton1975, author="Newton, Glen", title="{P}roving {P}roperties of {I}nteracting {P}rocesses", journal="Acta Informatica", year="1975", month="Jun", day="01", volume="4", number="2", pages="117--126", abstract="The Set of Interacting Procedures (SIP) model, a graph model suitable for representing interacting computations, is presented. It includes n{\'o}tation for creating and destroying processes, permits well-defined critical sections, and facilitates examining the logical properties of the modeled procedures. The essential parts of a theory of correctness of interacting processes are informally presented. These include a definition of correctness with respect to an assertion, a non-interference condition which justifies the use of the SIP model, and a set of sufficient conditions for correctness. To illustrate the use of the model and theory, a solution to the reader-writer problem is presented and modeled. An assertion expressing the correctness of the solution is formulated, and the SIP model of the solution is shown to be correct with respect to the assertion. Finally, the non-interference condition shows that the conclusions about the model also apply to the solution itself.", issn="1432-0525", doi="10.1007/BF00288744", url="https://doi.org/10.1007/BF00288744" } @article{Manna:1984:APP:2731.2734, author = {Manna, Zohar and Pnueli, Amir}, title = {{A}dequate {P}roof {P}rinciples for {I}nvariance and {L}iveness {P}roperties of {C}oncurrent {P}rograms}, journal = {Sci. Comput. Program.}, issue_date = {Dec. 1984}, volume = {4}, number = {3}, month = dec, year = {1984}, issn = {0167-6423}, pages = {257--289}, numpages = {33}, url = {http://dx.doi.org/10.1016/0167-6423(84)90003-0}, doi = {10.1016/0167-6423(84)90003-0}, acmid = {2734}, publisher = {Elsevier North-Holland, Inc.}, address = {Amsterdam, The Netherlands, The Netherlands}, } @article{board:1993:ieee, title={{I}eee {S}tandard {C}lassification for {S}oftware {A}nomalies}, author={Board, I}, journal={IEEE Std}, volume={1044}, year={1993} } @inproceedings{ye:2018:detecting, author = {Ye, Fangke and Zhao, Jisheng and Sarkar, Vivek}, title = {{D}etecting {MPI} {U}sage {A}nomalies via {P}artial {P}rogram {S}ymbolic {E}xecution}, booktitle = {Proceedings of the International Conference for High Performance Computing, Networking, Storage, and Analysis}, series = {SC '18}, year = {2018}, location = {Dallas, Texas}, pages = {63:1--63:5}, articleno = {63}, numpages = {5}, url = {https://doi.org/10.1109/SC.2018.00066}, note = {\url{https://doi.org/10.1109/SC.2018.00066}}, doi = {10.1109/SC.2018.00066}, acmid = {3291740}, publisher = {IEEE Press}, address = {Piscataway, NJ, USA}, keywords = {MPI, anomaly detection, symbolic execution}, } @InProceedings{christakis:2011:detection, author="Christakis, Maria and Sagonas, Konstantinos", editor="Rocha, Ricardo and Launchbury, John", title="Detection of Asynchronous Message Passing Errors Using Static Analysis", booktitle="Practical Aspects of Declarative Languages", year="2011", publisher="Springer Berlin Heidelberg", address="Berlin, Heidelberg", pages="5--18", abstract="Concurrent programming is hard and prone to subtle errors. In this paper we present a static analysis that is able to detect some commonly occurring kinds of message passing errors in languages with dynamic process creation and communication based on asynchronous message passing. Our analysis is completely automatic, fast, and strikes a proper balance between soundness and completeness: it is effective in detecting errors and avoids false alarms by computing a close approximation of the interprocess communication topology of programs. We have integrated our analysis in dialyzer, a widely used tool for detecting software defects in Erlang programs, and demonstrate its effectiveness on libraries and applications of considerable size. Despite the fact that these applications have been developed over a long period of time and are reasonably well-tested, our analysis has managed to detect a significant number of previously unknown message passing errors in their code.", isbn="978-3-642-18378-2" } @inproceedings{Takaoka:1994:PPV:326619.326811, author = {Takaoka, Tadao}, title = {{P}arallel {P}rogram {V}erification with {D}irected {G}raphs}, booktitle = {Proceedings of the 1994 ACM Symposium on Applied Computing}, series = {SAC '94}, year = {1994}, isbn = {0-89791-647-6}, location = {Phoenix, Arizona, USA}, pages = {462--466}, numpages = {5}, url = {http://doi.acm.org/10.1145/326619.326811}, note = {\url{http://doi.acm.org/10.1145/326619.326811}}, doi = {10.1145/326619.326811}, acmid = {326811}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {axiomatic method, logical independence, parallel program, verification directed graph}, } @Article{Owicki1976, author="Owicki, Susan and Gries, David", title="{A}n {A}xiomatic {P}roof {T}echnique for {P}arallel {P}rograms {I}$^*$", journal="Acta Informatica", year="1976", month="Dec", day="01", volume="6", number="4", pages="319--340", abstract="A language for parallel programming, with a primitive construct for synchronization and mutual exclusion, is presented. Hoare's deductive system for proving partial correctness of sequential programs is extended to include the parallelism described by the language. The proof method lends insight into how one should understand and present parallel programs. Examples are given using several of the standard problems in the literature. Methods for proving termination and the absence of deadlock are also given.", issn="1432-0525", doi="10.1007/BF00268134", url="https://doi.org/10.1007/BF00268134" } @InProceedings{vakkalanka2008dynamic, author="Vakkalanka, Sarvani and Gopalakrishnan, Ganesh and Kirby, Robert M.", editor="Gupta, Aarti and Malik, Sharad", title="{D}ynamic {V}erification of {MPI} {P}rograms with {R}eductions in {P}resence of {S}plit {O}perations and {R}elaxed {O}rderings", booktitle="Computer Aided Verification", year="2008", publisher="Springer Berlin Heidelberg", address="Berlin, Heidelberg", pages="66--79", abstract="Dynamic verification methods are the natural choice for debugging real world programs when model extraction and maintenance are expensive. Message passing programs written using the MPI library fall under this category. Partial order reduction can be very effective for MPI programs because for each process, all its local computational steps, as well as many of its MPI calls, commute with the corresponding steps of all other processes. However, when dependencies arise among MPI calls, they are often a function of the runtime state. While this suggests the use of dynamic partial order reduction (DPOR), three aspects of MPI make previous DPOR algorithms inapplicable: (i) many MPI calls are allowed to complete out of program order; (ii) MPI has global synchronization operations (e.g., barrier) that have a special weak semantics; and (iii) the runtime of MPI cannot, without intrusive modifications, be forced to pursue a specific interleaving because of MPI's liberal message matching rules, especially pertaining to `wildcard receives'. We describe our new dynamic verification algorithm `POE' that exploits the out of order completion semantics of MPI by delaying the issuance of MPI calls, issuing them only according to the formation of match-sets, which are ample `big-step' moves. POE guarantees to manifest any feasible interleaving by dynamically rewriting wildcard receives by specific-source receives. This is the first dynamic model-checking algorithm with reductions for (a large subset of) MPI that guarantees to catch all deadlocks and local assertion violations, and is found to work well in practice.", isbn="978-3-540-70545-1", note={\url{https://doi.org/10.1007/978-3-540-70545-1\_9}}, url={\url{https://doi.org/10.1007/978-3-540-70545-1\_9}}, } @inproceedings{Vo:2010:SDD:1884643.1884681, author = {Vo, Anh and Aananthakrishnan, Sriram and Gopalakrishnan, Ganesh and Supinski, Bronis R. de and Schulz, Martin and Bronevetsky, Greg}, title = {A Scalable and Distributed Dynamic Formal Verifier for MPI Programs}, booktitle = {Proceedings of the 2010 ACM/IEEE International Conference for High Performance Computing, Networking, Storage and Analysis}, series = {SC '10}, year = {2010}, isbn = {978-1-4244-7559-9}, pages = {1--10}, numpages = {10}, url = {https://doi.org/10.1109/SC.2010.7}, doi = {10.1109/SC.2010.7}, acmid = {1884681}, publisher = {IEEE Computer Society}, address = {Washington, DC, USA}, } @inproceedings{Yu:2018:CSE:3183440.3190336, author = {Yu, Hengbiao}, title = {Combining Symbolic Execution and Model Checking to Verify MPI Programs}, booktitle = {Proceedings of the 40th International Conference on Software Engineering: Companion Proceeedings}, series = {ICSE '18}, year = {2018}, isbn = {978-1-4503-5663-3}, location = {Gothenburg, Sweden}, pages = {527--530}, numpages = {4}, url = {http://doi.acm.org/10.1145/3183440.3190336}, note = {\url{http://doi.acm.org/10.1145/3183440.3190336}}, doi = {10.1145/3183440.3190336}, acmid = {3190336}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {MPI, model checking, symbolic execution, verification}, } @book{Hoare:1985:CSP:3921, author = {Hoare, C. A. R.}, title = {Communicating Sequential Processes}, year = {1985}, isbn = {0-13-153271-5}, publisher = {Prentice-Hall, Inc.}, address = {Upper Saddle River, NJ, USA}, } @article{Forejt:2017:PPA:3133234.3095075, author = {Forejt, Vojt\v{a}ch and Joshi, Saurabh and Kroening, Daniel and Narayanaswamy, Ganesh and Sharma, Subodh}, title = {Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs}, journal = {ACM Trans. Program. Lang. Syst.}, issue_date = {September 2017}, volume = {39}, number = {4}, month = aug, year = {2017}, issn = {0164-0925}, pages = {15:1--15:27}, articleno = {15}, numpages = {27}, url = {http://doi.acm.org/10.1145/3095075}, doi = {10.1145/3095075}, acmid = {3095075}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {MPI programs, Single-path verification, deadlock discovery}, } @InProceedings{khanna2018dynamic, author="Khanna, Dhriti and Sharma, Subodh and Rodr{\'i}guez, C{\'e}sar and Purandare, Rahul", editor="Havelund, Klaus and Peleska, Jan and Roscoe, Bill and de Vink, Erik", title="Dynamic {S}ymbolic {V}erification of {MPI} {P}rograms", booktitle="Formal Methods", year="2018", publisher="Springer International Publishing", address="Cham", pages="466--484", abstract="The success of dynamic verification techniques for Message Passing Interface (MPI) programs rests on their ability to address communication nondeterminism. As the number of processes in the program grows, the dynamic verification techniques suffer from the problem of exponential growth in the size of the reachable state space. In this work, we provide a hybrid verification technique for message passing programs that combines explicit-state dynamic verification with symbolic analysis. The dynamic verification component deterministically replays the execution runs of the program, while the symbolic component encodes a set of interleavings of the observed run of the program in a quantifier-free first order logic formula and verifies it for communication deadlocks. In the absence of property violations, it performs analysis to generate a different run of the program that does not fall in the set of already verified runs. We demonstrate the effectiveness of our approach, which is sound and complete, using our prototype tool Hermes. Our evaluation indicates that Hermes performs significantly better than the state-of-the-art verification tools for multi-path MPI programs.", isbn="978-3-319-95582-7", note={\url{https://doi.org/10.1007/978-3-319-95582-7\_28}}, } @article{siegel2011tass, title={{TASS}: The {T}oolkit for {A}ccurate {S}cientific {S}oftware}, author={Siegel, Stephen F and Zirkel, Timothy K}, journal={Mathematics in Computer Science}, volume={5}, number={4}, pages={395--426}, year={2011}, publisher={Springer}, note={\url{https://doi.org/10.1007/s11786-011-0100-7}}, url={\url{https://doi.org/10.1007/s11786-011-0100-7}}, } @inproceedings{Luo:2017:VMP:3127024.3127032, author = {Luo, Ziqing and Zheng, Manchun and Siegel, Stephen F.}, title = {Verification of MPI Programs Using CIVL}, booktitle = {Proceedings of the 24th European MPI Users' Group Meeting}, series = {EuroMPI '17}, year = {2017}, isbn = {978-1-4503-4849-2}, location = {Chicago, Illinois}, pages = {6:1--6:11}, articleno = {6}, numpages = {11}, url = {http://doi.acm.org/10.1145/3127024.3127032}, note = {\url{http://doi.acm.org/10.1145/3127024.3127032}}, doi = {10.1145/3127024.3127032}, acmid = {3127032}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {CIVL, MPI, model checking, symbolic execution, verification}, } @InProceedings{siegel2007verifying, author="Siegel, Stephen F.", editor="Cappello, Franck and Herault, Thomas and Dongarra, Jack", title="Verifying Parallel Programs with MPI-Spin", booktitle="Recent Advances in Parallel Virtual Machine and Message Passing Interface", year="2007", publisher="Springer Berlin Heidelberg", address="Berlin, Heidelberg", pages="13--14", abstract="Standard testing and debugging techniques are notoriously ineffective when applied to parallel programs, due to the numerous sources of nondeterminism arising from parallelism. MPI-Spin, an extension of the model checker Spin for verifying and debugging MPI-based parallel programs, overcomes many of the limitations associated with the standard techniques. By exploring all possible executions of an MPI program, MPI-Spin can conclude, for example, that a program cannot deadlock on any execution. If the program can deadlock, MPI-Spin can exhibit a trace showing exactly how the program fails, greatly facilitating debugging.", isbn="978-3-540-75416-9" } @ARTICLE{holzmann1997spin, author={G. J. {Holzmann}}, journal={IEEE Transactions on Software Engineering}, title={The model checker SPIN}, year={1997}, volume={23}, number={5}, pages={279-295}, keywords={formal verification;formal specification;distributed processing;SPIN model checker;efficient verification system;distributed software system models;design error detection;high-level distributed algorithm descriptions;detailed code;telephone exchange control;verifier design;verifier structure;Software systems;Application software;Distributed algorithms;Control system synthesis;Algorithm design and analysis;Error correction codes;Telephony;Design methodology;Concurrent computing;Message passing}, doi={10.1109/32.588521}, ISSN={0098-5589}, month={May},} @inproceedings{Droste:2015:MSA:2833157.2833159, author = {Droste, Alexander and Kuhn, Michael and Ludwig, Thomas}, title = {{MPI}-{C}hecker: {S}tatic {A}nalysis for {MPI}}, booktitle = {Proceedings of the Second Workshop on the LLVM Compiler Infrastructure in HPC}, series = {LLVM '15}, year = {2015}, isbn = {978-1-4503-4005-2}, location = {Austin, Texas}, pages = {3:1--3:10}, articleno = {3}, numpages = {10}, url = {http://doi.acm.org/10.1145/2833157.2833159}, note = {\url{http://doi.acm.org/10.1145/2833157.2833159}}, doi = {10.1145/2833157.2833159}, acmid = {2833159}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {MPI, clang static analyzer, high performance computing, static analysis}, } @misc{clangstaticanalyzer, howpublished={\url{http://clang-analyzer.llvm.org}}, title={Clang Static Analyzer}, note = {Accessed Sep.\ 6, 2019}, key={clang 16} } @inproceedings{Bronevetsky:2009:CSD:1545006.1545049, author = {Bronevetsky, Greg}, title = {Communication-Sensitive Static Dataflow for Parallel Message Passing Applications}, booktitle = {Proceedings of the 7th Annual IEEE/ACM International Symposium on Code Generation and Optimization}, series = {CGO '09}, year = {2009}, isbn = {978-0-7695-3576-0}, pages = {1--12}, numpages = {12}, url = {http://dx.doi.org/10.1109/CGO.2009.32}, note = {\url{http://dx.doi.org/10.1109/CGO.2009.32}}, doi = {10.1109/CGO.2009.32}, acmid = {1545049}, publisher = {IEEE Computer Society}, address = {Washington, DC, USA}, keywords = {message-passing, compiler analysis, static analysis, parallel processing, multi-core}, } @inproceedings{Strout:2006:DAM:1156433.1157634, author = {Strout, Michelle Mills and Kreaseck, Barbara and Hovland, Paul D.}, title = {{D}ata-{F}low {A}nalysis for {MPI} {P}rograms}, booktitle = {Proceedings of the 2006 International Conference on Parallel Processing}, series = {ICPP '06}, year = {2006}, isbn = {0-7695-2636-5}, pages = {175--184}, numpages = {10}, url = {http://dx.doi.org/10.1109/ICPP.2006.32}, note = {\url{http://dx.doi.org/10.1109/ICPP.2006.32}}, doi = {10.1109/ICPP.2006.32}, acmid = {1157634}, publisher = {IEEE Computer Society}, address = {Washington, DC, USA}, keywords = {MPI, data-flow analysis, activity analysis, SPMD, MPI-ICFG}, } @InProceedings{huchant2019multivalued, author="Huchant, Pierre and Saillard, Emmanuelle and Barthou, Denis and Carribault, Patrick", editor="Yahyapour, Ramin", title="Multi-valued Expression Analysis for Collective Checking", booktitle="Euro-Par 2019: Parallel Processing", year="2019", publisher="Springer International Publishing", address="Cham", pages="29--43", abstract="Determining if a parallel program behaves as expected on any execution is challenging due to non-deterministic executions. Static analyses help to detect all execution paths that can be executed concurrently by identifying multi-valued expressions, i.e. expressions evaluated differently among processes. This can be used to find collective errors in parallel programs. In this paper, we propose a new method that combines a control-flow analysis with a multi-valued expressions detection to find such errors. We implemented our method in the PARCOACH framework and successfully analyzed parallel applications using MPI, OpenMP, UPC and CUDA.", isbn="978-3-030-29400-7", note={\url{https://doi.org/10.1007/978-3-030-29400-7_3}}, } @incollection{krammer2004marmot, title={MARMOT: An MPI analysis and checking tool}, author={Krammer, Bettina and Bidmon, Katrin and M{\"u}ller, Matthias S and Resch, Michael M}, booktitle={Advances in Parallel Computing}, volume={13}, pages={493--500}, year={2004}, publisher={Elsevier}, note={\url{https://doi.org/10.1016/S0927-5452(04)80063-7}}, } @inproceedings{Hilbrich:2012:MRE:2388996.2389037, author = {Hilbrich, Tobias and Protze, Joachim and Schulz, Martin and de Supinski, Bronis R. and M\"{u}ller, Matthias S.}, title = {MPI Runtime Error Detection with MUST: Advances in Deadlock Detection}, booktitle = {Proceedings of the International Conference on High Performance Computing, Networking, Storage and Analysis}, series = {SC '12}, year = {2012}, isbn = {978-1-4673-0804-5}, location = {Salt Lake City, Utah}, pages = {30:1--30:11}, articleno = {30}, numpages = {11}, url = {http://dl.acm.org/citation.cfm?id=2388996.2389037}, note = {\url{http://dl.acm.org/citation.cfm?id=2388996.2389037}}, acmid = {2389037}, publisher = {IEEE Computer Society Press}, address = {Los Alamitos, CA, USA}, } @incollection{cohen-etal:2009:vcc, Abstract = {VCC is an industrial-strength verification environment for low-level concurrent system code written in C. VCC takes a program (annotated with function contracts, state assertions, and type invariants) and attempts to prove the correctness of these annotations. It includes tools for monitoring proof attempts and constructing partial counterexample executions for failed proofs. This paper motivates VCC, describes our verification methodology, describes the architecture of VCC, and reports on our experience using VCC to verify the Microsoft Hyper-V hypervisor.}, Affiliation = {Microsoft Corporation Redmond WA USA}, Author = {Cohen, Ernie and Dahlweid, Markus and Hillebrand, Mark and Leinenbach, Dirk and Moskal, Micha{\l} and Santen, Thomas and Schulte, Wolfram and Tobies, Stephan}, Booktitle = {Theorem Proving in Higher Order Logics}, Date-Added = {2011-08-20 01:20:33 +0000}, Date-Modified = {2011-08-20 01:27:39 +0000}, Editor = {Berghofer, Stefan and Nipkow, Tobias and Urban, Christian and Wenzel, Makarius}, Isbn = {978-3-642-03358-2}, Keyword = {Computer Science}, Pages = {23-42}, Publisher = {Springer Berlin / Heidelberg}, Series = {Lecture Notes in Computer Science}, Title = {{VCC}: {A} {P}ractical {S}ystem for {V}erifying {C}oncurrent {C}}, Volume = {5674}, Year = {2009}, note = {\url{http://dx.doi.org/10.1007/978-3-642-03359-9_2}}} @inproceedings{oortwijn2016future, title = "Future-based {S}tatic {A}nalysis of {M}essage {P}assing {P}rograms", abstract = "Message passing is widely used in industry to develop programs consisting of several distributed communicating components. Developing functionally correct message passing software is very challenging due to the concurrent nature of message exchanges. Nonetheless, many safety-critical applications rely on the message passing paradigm, including air traffic control systems and emergency services, which makes proving their correctness crucial. We focus on the modular verification of MPI programs by statically verifying concrete Java code. We use separation logic to reason about local correctness and define abstractions of the communication protocol in the process algebra used by mCRL2. We call these abstractions futures as they predict how components will interact during program execution. We establish a provable link between futures and program code and analyse the abstract futures via model checking to prove global correctness. Finally, we verify a leader election protocol to demonstrate our approach.", keywords = "IR-104114, EWI-27672", author = "Oortwijn, {Wytse Hendrikus Marinus} and Stefan Blom and Marieke Huisman", year = "2016", month = "4", doi = "10.4204/EPTCS.211.7", note = "\url{https://doi.org/10.4204/EPTCS.211.7}", language = "English", pages = "65--72", editor = "Dominic Orchard and Nobuko Yoshida", booktitle = "Proceedings PLACES 2016", } @inproceedings{Lopez:2015:PVM:2814270.2814302, author = {L\'{o}pez, Hugo A. and Marques, Eduardo R. B. and Martins, Francisco and Ng, Nicholas and Santos, C{\'e}sar and Vasconcelos, Vasco Thudichum and Yoshida, Nobuko}, title = {Protocol-based {V}erification of {M}essage-passing {P}arallel {P}rograms}, booktitle = {Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications}, series = {OOPSLA 2015}, year = {2015}, isbn = {978-1-4503-3689-5}, location = {Pittsburgh, PA, USA}, pages = {280--298}, numpages = {19}, url = {http://doi.acm.org/10.1145/2814270.2814302}, note = {\url{http://doi.acm.org/10.1145/2814270.2814302}}, doi = {10.1145/2814270.2814302}, acmid = {2814302}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {Dependent types, MPI, Parallel programming, Program verification, Session types}, } @book{bergstra2001handbook, title={Handbook of process algebra}, author={Bergstra, Jan A and Ponse, Alban and Smolka, Scott A}, year={2001}, publisher={Elsevier} } @inproceedings{Cranen:2013:OMT:2450387.2450410, author = {Cranen, Sjoerd and Groote, Jan Friso and Keiren, Jeroen J. A. and Stappers, Frank P. M. and de Vink, Erik P. and Wesselink, Wieger and Willemse, Tim A. C.}, title = {An Overview of the mCRL2 Toolset and Its Recent Advances}, booktitle = {Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems}, series = {TACAS'13}, year = {2013}, isbn = {978-3-642-36741-0}, location = {Rome, Italy}, pages = {199--213}, numpages = {15}, url = {http://dx.doi.org/10.1007/978-3-642-36742-7_15}, doi = {10.1007/978-3-642-36742-7_15}, acmid = {2450410}, publisher = {Springer-Verlag}, address = {Berlin, Heidelberg}, } @INPROCEEDINGS{luo2018towards, author={Z. {Luo} and S. F. {Siegel}}, booktitle={2018 IEEE/ACM 2nd International Workshop on Software Correctness for HPC Applications (Correctness)}, title={Towards Deductive Verification of Message-Passing Parallel Programs}, year={2018}, volume={}, number={}, pages={59-68}, keywords={inference mechanisms;message passing;parallel programming;program verification;message-passing parallel programs;deductive reasoning;message-passing programs;annotated sequential program;deductive verification;program verification;Tools;System recovery;Contracts;Software;Cognition;Data structures;Concurrent computing;deductive-verification;message-passing}, doi={10.1109/Correctness.2018.00012}, ISSN={}, month={Nov}, note={\url{https://doi.org/10.1109/Correctness.2018.00012}}, } @misc{ACSL:Reference, key = {ACSL}, title = {{ACSL}: {ANSI}/{ISO} {C} {S}pecification {L}anguage}, howpublished = {\url{http://frama-c.com/acsl.html}}, note = {Accessed Sep.\ 6, 2019} } @article{Meyer:1992:ADC, author = {Meyer, Bertrand}, title = {Applying "{D}esign by {C}ontract"}, journal = {Computer}, issue_date = {October 1992}, volume = {25}, number = {10}, month = oct, year = {1992}, issn = {0018-9162}, pages = {40--51}, numpages = {12}, url = {http://dx.doi.org/10.1109/2.161279}, eitherdoiorurl = {10.1109/2.161279}, acmid = {619797}, publisher = {IEEE Computer Society Press}, address = {Los Alamitos, CA, USA}, } @article{Ashcroft:1975:PAP:1739967.1740302, author = {Ashcroft, E. A.}, title = {Proving Assertions About Parallel Programs}, journal = {J. Comput. Syst. Sci.}, issue_date = {February, 1975}, volume = {10}, number = {1}, month = feb, year = {1975}, issn = {0022-0000}, pages = {110--135}, numpages = {26}, url = {http://dx.doi.org/10.1016/S0022-0000(75)80018-3}, doi = {10.1016/S0022-0000(75)80018-3}, acmid = {1740302}, publisher = {Academic Press, Inc.}, address = {Orlando, FL, USA}, } @inproceedings{Pham:2017:VMA:3145344.3145345, author = {Pham, Anh and J{\'e}ron, Thierry and Quinson, Martin}, title = {Verifying MPI Applications with SimGridMC}, booktitle = {Proceedings of the First International Workshop on Software Correctness for HPC Applications}, series = {Correctness'17}, year = {2017}, isbn = {978-1-4503-5127-0}, location = {Denver, CO, USA}, pages = {28--33}, numpages = {6}, url = {http://doi.acm.org/10.1145/3145344.3145345}, doi = {10.1145/3145344.3145345}, acmid = {3145345}, publisher = {ACM}, address = {New York, NY, USA}, } %% Meyer:1988:ELE:46869.46873 @article{Meyer:1988:eiffel, author = {Meyer, Bertrand}, title = {Eiffel: A Language and Environment for Software Engineering}, journal = {J. Syst. Softw.}, issue_date = {June, 1988}, volume = {8}, number = {3}, month = jun, year = {1988}, issn = {0164-1212}, pages = {199--246}, numpages = {48}, url = {http://dx.doi.org/10.1016/0164-1212(88)90022-2}, doi = {10.1016/0164-1212(88)90022-2}, acmid = {46873}, publisher = {Elsevier Science Inc.}, address = {New York, NY, USA}, } %% leino2010dafny @InProceedings{leino:2010:dafny, author="Leino, K. Rustan M.", editor="Clarke, Edmund M. and Voronkov, Andrei", title="{D}afny: {A}n {A}utomatic {P}rogram {V}erifier for {F}unctional {C}orrectness", booktitle="Logic for Programming, Artificial Intelligence, and Reasoning", year="2010", publisher="Springer Berlin Heidelberg", address="Berlin, Heidelberg", pages="348--370", abstract="Traditionally, the full verification of a program's functional correctness has been obtained with pen and paper or with interactive proof assistants, whereas only reduced verification tasks, such as extended static checking, have enjoyed the automation offered by satisfiability-modulo-theories (SMT) solvers. More recently, powerful SMT solvers and well-designed program verifiers are starting to break that tradition, thus reducing the effort involved in doing full verification.", isbn="978-3-642-17511-4", note={\url{https://doi.org/10.1007/978-3-642-17511-4_20}}, } %%filliatre2013why3 @InProceedings{filliatre:2013:why3, author="Filli{\^a}tre, Jean-Christophe and Paskevich, Andrei", editor="Felleisen, Matthias and Gardner, Philippa", title="{W}hy3 --- {W}here {P}rograms {M}eet {P}rovers", booktitle="Programming Languages and Systems", year="2013", publisher="Springer Berlin Heidelberg", address="Berlin, Heidelberg", pages="125--128", abstract="We present Why3, a tool for deductive program verification, and WhyML, its programming and specification language. WhyML is a first-order language with polymorphic types, pattern matching, and inductive predicates. Programs can make use of record types with mutable fields, type invariants, and ghost code. Verification conditions are discharged by Why3 with the help of various existing automated and interactive theorem provers. To keep verification conditions tractable and comprehensible, WhyML imposes a static control of aliases that obviates the use of a memory model. A user can write WhyML programs directly and get correct-by-construction OCaml programs via an automated extraction mechanism. WhyML is also used as an intermediate language for the verification of C, Java, or Ada programs. We demonstrate the benefits of Why3 and WhyML on non-trivial examples of program verification.", isbn="978-3-642-37036-6", note={\url{https://doi.org/10.1007/978-3-642-37036-6_8}}, } %% Beckert:2007:VOS:1808999 @book{beckert:2007:KeY, author = {Beckert, Bernhard and H\"{a}hnle, Reiner and Schmitt, Peter H.}, title = {Verification of Object-oriented Software: The KeY Approach}, year = {2007}, isbn = {3-540-68977-X, 978-3-540-68977-5}, publisher = {Springer-Verlag}, address = {Berlin, Heidelberg}, note = {\url{http://doi.org/10.1007/978-3-540-69061-0}}, } %% blom2017vercors @InProceedings{blom:2017:vercors, author="Blom, Stefan and Darabi, Saeed and Huisman, Marieke and Oortwijn, Wytse", editor="Polikarpova, Nadia and Schneider, Steve", title="The VerCors Tool Set: Verification of Parallel and Concurrent Software", note="\url{https://doi.org/10.1007/978-3-319-66845-1_7}", booktitle="Integrated Formal Methods", year="2017", publisher="Springer International Publishing", address="Cham", pages="102--110", abstract="This paper reports on the VerCors tool set for verifying parallel and concurrent software. Its main characteristics are (i) that it can verify programs under different concurrency models, written in high-level programming languages, such as for example in Java, OpenCL and OpenMP; and (ii) that it can reason not only about race freedom and memory safety, but also about functional correctness. VerCors builds on top of existing verification technology, notably the Viper framework, by transforming the verification problem of programs written in a high-level programming language into a verification problem in the intermediate language of Viper. This paper presents three examples that illustrate how VerCors support verifying functional correctness of three different concurrency features: heterogeneous concurrency, kernels using barriers and atomic operations, and compiler directives for parallelisation.", isbn="978-3-319-66845-1" } @InProceedings{cuoq2012framac, author="Cuoq, Pascal and Kirchner, Florent and Kosmatov, Nikolai and Prevosto, Virgile and Signoles, Julien and Yakobowski, Boris", editor="Eleftherakis, George and Hinchey, Mike and Holcombe, Mike", title="{F}rama-{C}", booktitle="Software Engineering and Formal Methods", year="2012", publisher="Springer Berlin Heidelberg", address="Berlin, Heidelberg", pages="233--247", abstract="Frama-C is a source code analysis platform that aims at conducting verification of industrial-size C programs. It provides its users with a collection of plug-ins that perform static analysis, deductive verification, and testing, for safety- and security-critical software. Collaborative verification across cooperating plug-ins is enabled by their integration on top of a shared kernel and datastructures, and their compliance to a common specification language. This foundational article presents a consolidated view of the platform, its main and composite analyses, and some of its industrial achievements.", isbn="978-3-642-33826-7", note={\url{https://doi.org/10.1007/978-3-642-33826-7_16}}, } %% barnett2006boogie @InProceedings{barnett:2006:boogie, author="Barnett, Mike and Chang, Bor-Yuh Evan and DeLine, Robert and Jacobs, Bart and Leino, K. Rustan M.", editor="de Boer, Frank S. and Bonsangue, Marcello M. and Graf, Susanne and de Roever, Willem-Paul", title="{B}oogie: {A} {M}odular {R}eusable {V}erifier for {O}bject-{O}riented {P}rograms", booktitle="Formal Methods for Components and Objects", year="2006", publisher="Springer Berlin Heidelberg", address="Berlin, Heidelberg", pages="364--387", abstract="A program verifier is a complex system that uses compiler technology, program semantics, property inference, verification-condition generation, automatic decision procedures, and a user interface. This paper describes the architecture of a state-of-the-art program verifier for object-oriented programs.", isbn="978-3-540-36750-5", note={\url{https://doi.org/10.1007/11804192_17}}, } %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%% MiniMP Spec %%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @INPROCEEDINGS{dwyer:1999:patterns, author={M. B. {Dwyer} and G. S. {Avrunin} and J. C. {Corbett}}, booktitle={Proceedings of the 1999 International Conference on Software Engineering (IEEE Cat. No.99CB37002)}, title={{P}atterns in property specifications for finite-state verification}, year={1999}, volume={}, number={}, pages={411-420}, keywords={formal specification;formal verification;object-oriented methods;property specification patterns;finite-state verification;model checkers;automatic error detection;formal methods;property specification presentation;property specification codification;property specification reuse;Formal specifications;Permission;Logic;Mathematics;Statistics;Computer science;Computer errors;NASA;System testing;Automation}, doi={10.1145/302405.302672}, note={\url{http://doi.org/10.1145/302405.302672}}, ISSN={0270-5257}, month={May},} @Article{lamport:1980:hoare, author="Lamport, Leslie", title="{T}he `{H}oare logic' of concurrent programs", journal="Acta Informatica", year="1980", month="Jun", day="01", volume="14", number="1", pages="21--37", abstract="Hoare's logical system for specifying and proving partial correctness properties of sequential programs is generalized to concurrent programs. The basic idea is to define the assertion {\{}P{\}} S {\{}Q{\}} to mean that if execution is begun anywhere in S with P true, then P will remain true until S terminates, and Q will be true if and when S terminates. The predicates P and Q may depend upon program control locations as well as upon the values of variables. A system of inference rules and axiom schemas is given, and a formal correctness proof for a simple program is outlined. We show that by specifying certain requirements for the unimplemented parts, correctness properties can be proved without completely implementing the program. The relation to Pnueli's temporal logic formalism is also discussed.", issn="1432-0525", doi="10.1007/BF00289062", url="https://doi.org/10.1007/BF00289062", note={\url{https://doi.org/10.1007/BF00289062}}, } %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%% Decompose rules %%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @article{Kleymann:1999:HLA:2769784.2769811, author = {Kleymann, Thomas}, title = {{H}oare {L}ogic and {A}uxiliary {V}ariables}, journal = {Form. Asp. Comput.}, issue_date = {December 1999}, volume = {11}, number = {5}, month = dec, year = {1999}, issn = {0934-5043}, pages = {541--566}, numpages = {26}, url = {http://dx.doi.org/10.1007/s001650050057}, doi = {10.1007/s001650050057}, acmid = {2769811}, publisher = {Springer-Verlag}, address = {London, UK, UK}, keywords = {Keywords: Hoare Logic; Auxiliary variables; Adaptation Completeness; Most General Formula; VDM}, } %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%% contract system for MiniMP %%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @article{Hentschel2018, title = {{T}he {S}ymbolic {E}xecution {D}ebugger ({SED}): a platform for interactive symbolic execution, debugging, verification and more}, author = {Martin Hentschel and Richard Bubel and Reiner H\"{a}hnle}, url = {https://doi.org/10.1007/s10009-018-0490-9}, doi = {10.1007/s10009-018-0490-9}, issn = {1433-2787}, year = {2018}, date = {2018-03-03}, journal = {International Journal on Software Tools for Technology Transfer}, abstract = {The Symbolic Execution Debugger (SED), is an extension of the debug platform for interactive debuggers based on symbolic execution. The SED comes with a static symbolic execution engine for sequential programs, but any third-party symbolic execution engine can be integrated into the SED. An interactive debugger based on symbolic execution allows one like a traditional debugger to locate defects in the source code. The difference is that all feasible execution paths are explored at once, and thus there is no need to know input values resulting in an execution that exhibits the failure. In addition, such a debugger can be used in code reviews and to guide and present results of an analysis based on symbolic execution such as, in our case, correctness proofs. Experimental evaluations proved that the SED increases the effectiveness of code reviews and proof understanding tasks.}, keywords = {}, pubstate = {published}, tppubtype = {article} } @inproceedings{McMillan:2010:LAP:2144310.2144323, author = {McMillan, Kenneth L.}, title = {{L}azy {A}nnotation for {P}rogram {T}esting and {V}erification}, booktitle = {Proceedings of the 22Nd International Conference on Computer Aided Verification}, series = {CAV'10}, year = {2010}, isbn = {3-642-14294-X, 978-3-642-14294-9}, location = {Edinburgh, UK}, pages = {104--118}, numpages = {15}, url = {http://dx.doi.org/10.1007/978-3-642-14295-6_10}, doi = {10.1007/978-3-642-14295-6_10}, acmid = {2144323}, publisher = {Springer-Verlag}, address = {Berlin, Heidelberg}, } @MISC{Sankaranarayanan04non-linearloop, author = {Sriram Sankaranarayanan and Henny B. Sipma and Zohar Manna}, title = {{N}on-linear {L}oop {I}nvariant {G}eneration using {G}r\"{o}bner {B}ases}, year = {2004} } @article{Kauer:2010:MII:1860141.1860452, author = {Kauer, Stefan and Winkler, J\"{u}rgen F. H.}, title = {{M}echanical {I}nference of {I}nvariants for {FOR}-loops}, journal = {J. Symb. Comput.}, issue_date = {November, 2010}, volume = {45}, number = {11}, month = nov, year = {2010}, issn = {0747-7171}, pages = {1101--1113}, numpages = {13}, url = {http://dx.doi.org/10.1016/j.jsc.2008.11.008}, doi = {10.1016/j.jsc.2008.11.008}, acmid = {1860452}, publisher = {Academic Press, Inc.}, address = {Duluth, MN, USA}, keywords = {FOR-loop, Mechanical inference of loop invariants, Mechanical verification, RCPV}, } %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%% HOW IS MPI MODELED IN CIVL %%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @Inproceedings{zheng-etal:2015:civl_ase, author = {Manchun Zheng and Michael S.\ Rogers and Ziqing Luo and Matthew B.\ Dwyer and Stephen F.\ Siegel}, title = {{CIVL}: Formal Verification of Parallel Programs}, booktitle = {ASE 2015: 30th IEEE/ACM International Conference on Automated Software Engineering, Proceedings}, series = {ASE '15}, year = {2015}, month = {Nov}, publisher = {IEEE Press}, address = {Piscataway, NJ, USA}, page = {830-835} } @Inproceedings{zheng-etal:2016:civl_tacas, author = {Manchun Zheng and John G.\ Edenhofner and Ziqing Luo and Mitchell J.\ Gerrard and Michael S.\ Rogers and Matthew B.\ Dwyer and and Stephen F.\ Siegel}, title = {{CIVL}: Applying a General Concurrency Verification Framework to C/Pthreads Programs (Competition Contribution)}, booktitle = {TACAS 16: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Proceedings}, series = {TACAS '16}, year = {2016}, month = {Apr}, publisher = {Springer-Verlag}, address = {Eindhoven, The Netherlands}, } @inproceedings{siegel-etal:2015:civl_sc, author = {Siegel, Stephen F. and Zheng, Manchun and Luo, Ziqing and Zirkel, Timothy K. and Marianiello, Andre V. and Edenhofner, John G. and Dwyer, Matthew B. and Rogers, Michael S.}, title = {{CIVL}: The {C}oncurrency {I}ntermediate {V}erification {L}anguage}, booktitle = {Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis}, series = {SC '15}, year = {2015}, isbn = {978-1-4503-3723-6}, location = {Austin, Texas}, pages = {61:1--61:12}, articleno = {61}, numpages = {12}, url = {http://doi.acm.org/10.1145/2807591.2807635}, note = {\url{http://doi.acm.org/10.1145/2807591.2807635}}, eitherdoiorurl = {10.1145/2807591.2807635}, acmid = {2807635}, publisher = {ACM}, address = {New York}, keywords = {CUDA, MPI, OpenMP, concurrency, intermediate representation, model checking, parallel programming, program transformation, pthreads, symbolic execution, verification} } @inproceedings{barrett-etal:2011:cvc4, author = {Barrett, Clark and Conway, Christopher L. and Deters, Morgan and Hadarean, Liana and Jovanovi\'{c}, Dejan and King, Tim and Reynolds, Andrew and Tinelli, Cesare}, title = {{CVC4}}, booktitle={International Conference on Computer Aided Verification}, pages = {171--177}, numpages = {7}, year={2011}, url = {http://dl.acm.org/citation.cfm?id=2032305.2032319}, acmid = {2032319}, } @INPROCEEDINGS{alt-ergo, author={S. {Conchon} and M. {Iguernelala} and A. {Mebsout}}, booktitle={2013 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing}, title={{A} {C}ollaborative {F}ramework for {N}on-{L}inear {I}nteger {A}rithmetic {R}easoning in {A}lt-{E}rgo}, year={2013}, volume={}, number={}, pages={161-168}, keywords={arithmetic;computability;groupware;inference mechanisms;integration;mathematics computing;program verification;theorem proving;collaborative framework;nonlinear integer arithmetic reasoning;AC(X) combination method;linear integer arithmetic;associativity properties;commutativity properties;nonlinear multiplication;interval calculus component;linear operations;SAT solver;judicious case-splits;bounded intervals;Alt-Ergo theorem prover;deductive program verification;modulo simple properties;Calculus;Equations;Collaboration;Standards;Inference algorithms;Cognition;Context;smt;satisfiability modulo theories;non-linear arithmetic;ground completion modulo;interval analysis}, doi={10.1109/SYNASC.2013.29}, note={\url{http://doi.org/10.1109/SYNASC.2013.29}}, ISSN={}, month={Sep.},} @inproceedings{kovacs:2013:firstorder, author = {Kov\'{a}cs, Laura and Voronkov, Andrei}, title = {{F}irst-{O}rder {T}heorem {P}roving and {V}ampire}, booktitle = {Proceedings of the 25th International Conference on Computer Aided Verification - Volume 8044}, series = {CAV 2013}, year = {2013}, isbn = {978-3-642-39798-1}, location = {Saint Petersburg, Russia}, pages = {1--35}, numpages = {35}, url = {http://dx.doi.org/10.1007/978-3-642-39799-8_1}, note = {\url{http://dx.doi.org/10.1007/978-3-642-39799-8_1}}, doi = {10.1007/978-3-642-39799-8_1}, acmid = {2958033}, publisher = {Springer-Verlag New York, Inc.}, address = {New York, NY, USA}, } @Inbook{mcmillan:1993:symbolic, author="McMillan, Kenneth L.", title="{S}ymbolic {M}odel {C}hecking", bookTitle="Symbolic Model Checking", year="1993", publisher="Springer US", address="Boston, MA", pages="25--60", abstract="In the previous chapter, we equated a CTL formula with the set of states in which the formula is true. We showed how the CTL operators can thus be characterized as fixed points of certain continuous functionals in the lattice of subsets, and how these fixed points can be computed iteratively. This provides us with a model checking algorithm for CTL, but requires us to build a finite Kripke model for our system and hence leads us to the state explosion problem. In this chapter, we will explore a method of model checking that avoids the state explosion problem in some cases by representing the Kripke model implicitly with a Boolean formula. This allows the CTL model checking algorithm to be implemented using well developed automatic techniques for manipulating Boolean formulas. Since the Kripke model is symbolically represented, there is no need to actually construct it as an explicit data structure. Hence, the state explosion problem can be avoided.", isbn="978-1-4615-3190-6", doi="10.1007/978-1-4615-3190-6_3", url="https://doi.org/10.1007/978-1-4615-3190-6_3", note={\url{https://doi.org/10.1007/978-1-4615-3190-6_3}}, } @article{biere:2003:bounded, title={{B}ounded {M}odel {C}hecking}, author={Biere, Armin and Cimatti, Alessandro and Clarke, Edmund M and Strichman, Ofer and Zhu, Yunshan and others}, journal={Advances in computers}, volume={58}, number={11}, pages={117--148}, year={2003} } @InProceedings{kroening:2014:cbmc, author="Kroening, Daniel and Tautschnig, Michael", editor="{\'A}brah{\'a}m, Erika and Havelund, Klaus", title="CBMC -- C Bounded Model Checker", booktitle="Tools and Algorithms for the Construction and Analysis of Systems", year="2014", publisher="Springer Berlin Heidelberg", address="Berlin, Heidelberg", pages="389--391", abstract="CBMC implements bit-precise bounded model checking for C programs and has been developed and maintained for more than ten years. CBMC verifies the absence of violated assertions under a given loop unwinding bound. Other properties, such as SV-COMP's ERROR labels or memory safety properties are reduced to assertions via automated instrumentation. Only recently support for efficiently checking concurrent programs, including support for weak memory models, has been added. Thus, CBMC is now capable of finding counterexamples in all of SV-COMP's categories. As back end, the competition submission of CBMC uses MiniSat 2.2.0.", isbn="978-3-642-54862-8" } @ARTICLE{clarke:1976:symbolically, author={L. A. {Clarke}}, journal={IEEE Transactions on Software Engineering}, title={{A} {S}ystem to {G}enerate {T}est {D}ata and {S}ymbolically {E}xecute {P}rograms}, year={1976}, volume={SE-2}, number={3}, pages={215-222}, keywords={Program validation;software reliability;symbolic execution;test data generation;System testing;Humans;Programming profession;Input variables;Linear programming;Documentation;Software reliability;Software testing;Automatic testing;Computer errors;Program validation;software reliability;symbolic execution;test data generation}, doi={10.1109/TSE.1976.233817}, note={\url{http://doi.org/10.1109/TSE.1976.233817}}, ISSN={}, month={Sep.},} @InProceedings{Z3Prover, author="de Moura, Leonardo and Bj{\o}rner, Nikolaj", editor="Ramakrishnan, C. R. and Rehof, Jakob", title="Z3: An {E}fficient {SMT} {S}olver", booktitle="Tools and Algorithms for the Construction and Analysis of Systems", year="2008", publisher="Springer Berlin Heidelberg", address="Berlin, Heidelberg", pages="337--340", abstract="Satisfiability Modulo Theories (SMT) problem is a decision problem for logical first order formulas with respect to combinations of background theories such as: arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 is a new and efficient SMT Solver freely available from Microsoft Research. It is used in various software verification and analysis applications.", isbn="978-3-540-78800-3" } @misc{iso:2011:c11, author={{International Organization for Standardization} and {International Electrotechnical Commission}}, title = {{ISO/IEC 989:2011 N1570: Programming Languages -- C}}, year={2011}, month=apr, day=12, howpublished={\url{http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1570.pdf}}, } %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%% From MiniMP to MPI %%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @article{tramm2014xsbench, title={{XSB}ench-the development and verification of a performance abstraction for {M}onte {C}arlo reactor analysis}, author={Tramm, John R and Siegel, Andrew R and Islam, Tanzima and Schulz, Martin}, year={2014}, journal={The Role of Reactor Physics toward a Sustainable Future (PHYSOR)}, } %%6702617, @INPROCEEDINGS{soumagne:2013:mercury, author={J. {Soumagne} and D. {Kimpe} and J. {Zounmevo} and M. {Chaarawi} and Q. {Koziol} and A. {Afsahi} and R. {Ross}}, booktitle={2013 IEEE International Conference on Cluster Computing (CLUSTER)}, title={{M}ercury: {E}nabling remote procedure call for high-performance computing}, year={2013}, volume={}, number={}, pages={1-8}, keywords={application program interfaces;data handling;parallel processing;remote procedure calls;Mercury;remote procedure call;high-performance computing;distributed services;HPC;socket-based network interface;API;large data arguments;asynchronous RPC interface;asynchronous transfer;native transport mechanisms;Servers;Pipeline processing;Data transfer;Protocols;Registers;Memory management}, doi={10.1109/CLUSTER.2013.6702617}, note={\url{https://10.1109/CLUSTER.2013.6702617}}, ISSN={}, month={Sep.},} %%ROMANO201590 @article{romano-etal:2015:openmc, title = "{O}pen{MC}: {A} state-of-the-art {M}onte {C}arlo code for research and development", journal = "Annals of Nuclear Energy", volume = "82", pages = "90 - 97", year = "2015", issn = "0306-4549", doi = "https://doi.org/10.1016/j.anucene.2014.07.048", url = "http://www.sciencedirect.com/science/article/pii/S030645491400379X", note = "\url{http://www.sciencedirect.com/science/article/pii/S030645491400379X}", author = "Paul K. Romano and Nicholas E. Horelik and Bryan R. Herman and Adam G. Nelson and Benoit Forget and Kord Smith", keywords = "Monte Carlo, Neutron transport, OpenMC, Parallel, XML, HDF5", abstract = "This paper gives an overview of OpenMC, an open source Monte Carlo particle transport code recently developed at the Massachusetts Institute of Technology. OpenMC uses continuous-energy cross sections and a constructive solid geometry representation, enabling high-fidelity modeling of nuclear reactors and other systems. Modern, portable input/output file formats are used in OpenMC: XML for input, and HDF5 for output. High performance parallel algorithms in OpenMC have demonstrated near-linear scaling to over 100,000 processors on modern supercomputers. Other topics discussed in this paper include plotting, CMFD acceleration, variance reduction, eigenvalue calculations, and software development processes." } %%osti_1389816, @misc{yang-etal:2017:amg, title = {{A}lgebraic {M}ultigrid {B}enchmark, {V}ersion 00}, author = {Yang, Ulrike and Falgout, Robert and Park, Jongsoo}, abstractNote = {AMG is a parallel algebraic multigrid solver for linear systems arising from problems on unstructured grids. It has been derived directly from the BoomerAMG solver in the hypre library, a large linear solvers library that is being developed in the Center for Applied Scientific Computing (CASC) at LLNL and is very similar to the AMG2013 benchmark with additional optimizations. The driver provided in the benchmark can build various test problems. The default problem is a Laplace type problem with a 27-point stencil, which can be scaled up and is designed to solve a very large problem. A second problem simulates a time dependent problem, in which successively various smnllcr systems are solved.}, url = {https://www.osti.gov//servlets/purl/1389816}, note = {\url{https://www.osti.gov//servlets/purl/1389816}}, doi = {}, year = {2017}, month = {8}, } %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%% MPI Contract Impl %%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @misc{java8, key = {JAVA 8}, title = {{J}ava {SE} 8}, howpublished = {\url{https://www.oracle.com/technetwork/java/javase/overview/java8-2100321.html}}, note = {Accessed Sep.\ 6, 2019} } @misc{ada2012, key = {ADA}, title = {{A}da {R}eference {M}anual 2012}, howpublished = {\url{http://docs.adacore.com/live/wave/arm12/html/arm12/arm12.html}}, note = {Accessed Sep.\ 6, 2019} } @article{Thakur:2005:OCC:2747766.2747771, author = {Thakur, Rajeev and Rabenseifner, Rolf and Gropp, William}, title = {{O}ptimization of {C}ollective {C}ommunication {O}perations in {MPICH}}, journal = {Int. J. High Perform. Comput. Appl.}, issue_date = {February 2005}, volume = {19}, number = {1}, month = feb, year = {2005}, issn = {1094-3420}, pages = {49--66}, numpages = {18}, url = {http://dx.doi.org/10.1177/1094342005051521}, doi = {10.1177/1094342005051521}, acmid = {2747771}, publisher = {Sage Publications, Inc.}, address = {Thousand Oaks, CA, USA}, keywords = {Collective communication, MPI, message passing, reduction}, } @ARTICLE{jesper2019optimal, author={J. L. {Träff}}, journal={IEEE Transactions on Parallel and Distributed Systems}, title={{O}n {O}ptimal {T}rees for {I}rregular {G}ather and {S}catter {C}ollectives}, year={2019}, volume={30}, number={9}, pages={2060-2074}, keywords={computational complexity;dynamic programming;trees (mathematics);optimal trees;k-ported communication networks;linear-time transmission cost model;root processor;processor order;nonordered communication trees;ordered communication trees;one-ported communication;distributed problem-adaptive tree construction algorithm;nonbinomial trees;dynamic programming algorithms;irregular gather and scatter collective communication operations;problem-adaptive tree construction algorithm;Program processors;Communication networks;Heuristic algorithms;Dynamic programming;Data models;Computational modeling;Complexity theory;Gather and scatter collective operations;irregular collective operations;communication trees; $k$ k -ported communication networks;dynamic programming;NP-hardness}, doi={10.1109/TPDS.2019.2899843}, ISSN={}, month={Sep.},} @article{KANG2019220, title = "Scalable Algorithms for MPI Intergroup Allgather and Allgatherv", journal = "Parallel Computing", volume = "85", pages = "220 - 230", year = "2019", issn = "0167-8191", doi = "https://doi.org/10.1016/j.parco.2019.04.015", url = "http://www.sciencedirect.com/science/article/pii/S016781911830320X", author = "Qiao Kang and Jesper Larsson Träff and Reda Al-Bahrani and Ankit Agrawal and Alok Choudhary and Wei-keng Liao", keywords = "Intergroup collective communication, All-to-all broadcast, Allgather, Allgatherv", abstract = "MPI intergroup collective communication defines message transfer patterns between two disjoint groups of MPI processes. Such patterns occur in coupled applications, and in modern scientific application workflows, mostly with large data sizes. However, current implementations in MPI production libraries adopt the “root gathering algorithm”, which does not achieve optimal communication transfer time. In this paper, we propose algorithms for the intergroup Allgather and Allgatherv communication operations under single-port communication constraints. We implement the new algorithms using MPI point-to-point and standard intra-communicator collective communication functions. We evaluate their performance on the Cori supercomputer at NERSC. Using message sizes per compute node ranging from 64KBytes to 8MBytes, our experiments show significant performance improvements of up to 23.67 times on 256 compute nodes compared with the implementations of production MPI libraries." } @article{Ruefenacht:2017:GRD:3163938.3164013, author = {Ruefenacht, Martin and Bull, Mark and Booth, Stephen}, title = {{G}eneralisation of {R}ecursive {D}oubling for {A}llReduce}, journal = {Parallel Comput.}, issue_date = {November 2017}, volume = {69}, number = {C}, month = nov, year = {2017}, issn = {0167-8191}, pages = {24--44}, numpages = {21}, url = {https://doi.org/10.1016/j.parco.2017.08.004}, doi = {10.1016/j.parco.2017.08.004}, acmid = {3164013}, publisher = {Elsevier Science Publishers B. V.}, address = {Amsterdam, The Netherlands, The Netherlands}, keywords = {AllReduce, Collective, MPI, Message pipelining, Recursive doubling, Scalability, n-way}, } %%10.1007/3-540-47789-6_66 @InProceedings{falgout:2002:hypre, author="Falgout, Robert D. and Yang, Ulrike Meier", editor="Sloot, Peter M. A. and Hoekstra, Alfons G. and Tan, C. J. Kenneth and Dongarra, Jack J.", title="\emph{hypre}: {A} {L}ibrary of {H}igh {P}erformance {P}reconditioners", booktitle="Computational Science --- ICCS 2002", year="2002", publisher="Springer Berlin Heidelberg", address="Berlin, Heidelberg", pages="632--641", abstract="hypre is a software library for the solution of large, sparse linear systems on massively parallel computers. Its emphasis is on modern powerful and scalable preconditioners. hypre provides various conceptual interfaces to enable application users to access the library in the way they naturally think about their problems. This paper presents the conceptual interfaces in hypre. An overview of the preconditioners that are available in hypre is given, including some numerical results that show the efficiency of the library.", isbn="978-3-540-47789-1", note="\url{https://doi.org/10.1007/3-540-47789-6\_66}", } @InProceedings{10.1007/978-3-030-03421-4_12, author="Luo, Ziqing and Siegel, Stephen F.", editor="Margaria, Tiziana and Steffen, Bernhard", title="{S}ymbolic {E}xecution and {D}eductive {V}erification {A}pproaches to {V}erify{T}his 2017 {C}hallenges", booktitle="Leveraging Applications of Formal Methods, Verification and Validation. Verification", year="2018", publisher="Springer International Publishing", address="Cham", pages="160--178", abstract="We present solutions to the VerifyThis 2017 program verification challenges using the symbolic execution tool CIVL. Comparing these to existing solutions using deductive verification tools such as Why3 and KeY, we analyze the advantages and disadvantages of the two approaches. The issues include scalability; the ability to handle challenging programming language constructs, such as expressions with side-effects, pointers, and concurrency; the ability to specify complex properties; and usability and automation. We conclude with a presentation of a new CIVL feature that attempts to bridge the gap between the two approaches by allowing a user to incorporate loop invariants incrementally into a symbolic execution framework.", isbn="978-3-030-03421-4" } @inproceedings{Bernaschi:2002:EIR:1895489.1895529, author = {Bernaschi, Massimo and Iannello, Giulio and Lauria, Mario}, title = {{E}fficient {I}mplementation of {R}educe-scatter in {MPI}}, booktitle = {Proceedings of the 10th Euromicro Conference on Parallel, Distributed and Network-based Processing}, series = {EUROMICRO-PDP'02}, year = {2002}, isbn = {0-7695-1444-8, 978-0-7695-1444-4}, location = {Canary Islands, Spain}, pages = {301--308}, numpages = {8}, url = {http://dl.acm.org/citation.cfm?id=1895489.1895529}, acmid = {1895529}, publisher = {IEEE Computer Society}, address = {Washington, DC, USA}, } @InProceedings{10.1007/978-3-642-27940-9_27, author="Siegel, Stephen F. and Zirkel, Timothy K.", editor="Kuncak, Viktor and Rybalchenko, Andrey", title="{L}oop {I}nvariant {S}ymbolic {E}xecution for {P}arallel {P}rograms", booktitle="Verification, Model Checking, and Abstract Interpretation", year="2012", publisher="Springer Berlin Heidelberg", address="Berlin, Heidelberg", pages="412--427", abstract="Techniques for verifying program assertions using symbolic execution exhibit a significant limitation: they typically require that (small) bounds be imposed on the number of loop iterations. For sequential programs, there is a way to overcome this limitation using loop invariants. The basic idea is to assign new symbolic constants to the variables modified in the loop body, add the invariant to the path condition, and then explore two paths: one which executes the loop body and checks that the given invariant is inductive, the other which jumps to the location just after the loop. For parallel programs, the situation is more complicated: the invariant may relate the state of multiple processes, these processes may enter and exit the loop at different times, and they may be at different iteration counts at the same time. In this paper, we show how to overcome these obstacles. Specifically, we introduce the notion of collective loop invariant and a symbolic execution technique that uses it to verify assertions in message-passing parallel programs with unbounded loops, generalizing the sequential technique.", isbn="978-3-642-27940-9", note="\url{https://doi.org/10.1007/978-3-642-27940-9_27}", } @inproceedings{Palmer:2007:SDD:1273647.1273657, author = {Palmer, Robert and Gopalakrishnan, Ganesh and Kirby, Robert M.}, title = {{S}emantics {D}riven {D}ynamic {P}artial-order {R}eduction of {MPI}-based {P}arallel {P}rograms}, booktitle = {Proceedings of the 2007 ACM Workshop on Parallel and Distributed Systems: Testing and Debugging}, series = {PADTAD '07}, year = {2007}, isbn = {978-1-59593-748-3}, location = {London, United Kingdom}, pages = {43--53}, numpages = {11}, url = {http://doi.acm.org/10.1145/1273647.1273657}, note = {\url{http://doi.acm.org/10.1145/1273647.1273657}}, doi = {10.1145/1273647.1273657}, acmid = {1273657}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {MPI, concurrent program semantics, model checking, partial-order reduction, transition independence}, } @InProceedings{10.1007/978-3-540-30579-8_27, author="Siegel, Stephen F.", editor="Cousot, Radhia", title="Efficient Verification of Halting Properties for MPI Programs with Wildcard Receives", booktitle="Verification, Model Checking, and Abstract Interpretation", year="2005", publisher="Springer Berlin Heidelberg", address="Berlin, Heidelberg", pages="413--429", note={\url{https://doi.org/10.1007/978-3-540-30579-8_27}}, abstract="We are concerned with the verification of certain properties, such as freedom from deadlock, for parallel programs that are written using the Message Passing Interface (MPI). It is known that for MPI programs containing no ``wildcard receives'' (and restricted to a certain subset of MPI) freedom from deadlock can be established by considering only synchronous executions. We generalize this by presenting a model checking algorithm that deals with wildcard receives by moving back and forth between a synchronous and a buffering mode as the search of the state space progresses. This approach is similar to that taken by partial order reduction (POR) methods, but can dramatically reduce the number of states explored even when the standard POR techniques do not apply.", isbn="978-3-540-30579-8" } @inproceedings{Siegel:2005:MWM:1065944.1065957, author = {Siegel, Stephen F. and Avrunin, George S.}, title = {Modeling Wildcard-free MPI Programs for Verification}, booktitle = {Proceedings of the Tenth ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming}, series = {PPoPP '05}, year = {2005}, isbn = {1-59593-080-9}, location = {Chicago, IL, USA}, pages = {95--106}, numpages = {12}, url = {http://doi.acm.org/10.1145/1065944.1065957}, note = {\url{http://doi.acm.org/10.1145/1065944.1065957}}, doi = {10.1145/1065944.1065957}, acmid = {1065957}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {MPI, SPIN, analysis, concurrent systems, deadlock, finite-state verification, formal methods, message passing interface, model checking, parallel computation}, }