% Insert your bib items in this file. % Separate the conference entries from the article entries % using crossref. The article entries go at the beginning % and the conference entries all go at the end. % To avoid conflicts, do not keep uncommitted changes in your local % copy of this file. Update, edit, and commit in one almost-atomic % step. %%%%%%%%%%%%%%%%%%%%%%%%%%% ARTICLE ENTRIES %%%%%%%%%%%%%%%%%%%%%%%%%%%% % Keep the article entries alphabetized in the same way they will appear % in the final document, i.e., by author's last name, then first name, % then next author, ..., then date. % AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA @InProceedings{europvm09-sriram, author = "Sriram Aananthakrishnan and Michael Delisi and Sarvani S. Vakkalanka and Anh Vo and Ganesh Gopalakrishnan and Robert M. Kirby and Rajeev Thakur", title = "How Formal Dynamic Verification Tools Facilitate Novel Concurrency Visualizations", booktitle = "EuroPVM/MPI", pages = "261--270", year = "2009", } @misc{abc:2014:web, title={{ABC}: {ANTLR}-{B}ased {C} front-end}, howpublished={\url{http://vsl.cis.udel.edu/abc}}, key={ABC}, year={accessed Feb.\ 6, 2014} } @Article{Adve:1996:SMC, author = "Sarita V. Adve and Kourosh Gharachorloo", title = "Shared memory consistency models: {A} tutorial", journal = "Computer", volume = "29", number = "12", pages = "66--76", month = dec, year = "1996", coden = "CPTRB4", ISSN = "0018-9162", bibdate = "Mon Jan 6 14:08:32 MST 1997", acknowledgement = ack-nhfb, } @inproceedings{adve:90a, author = {Sarita V. Adve and Mark D. Hill}, title = {Weak Ordering --- A New Definition}, year = {1990}, pages = {2-14}, ee = {http://doi.acm.org/10.1145/325164.325100}, crossref = {DBLP:conf/isca/1990}, bibsource = {DBLP, http://dblp.uni-trier.de} } @article{fences-fmsd-2012-jade, author = {Jade Alglave and Luc Maranget and Susmit Sarkar and Peter Sewell}, title = {Fences in weak memory models (extended version)}, journal = {Formal Methods in System Design}, volume = 40, number =2, pages = {170-205}, year = 2012} @misc{opencl-sdk, author = {AMD}, title = {{AMD} Accelerated Parallel Processing ({APP}) {SDK}}, howpublished = {\url{http://developer.amd.com/sdks/amdappsdk/pages/default.aspx}} } @book{allen-kennedy:2001:compilers, author = {Randy Allen and Ken Kennedy}, title = {Optimizing Compilers for Modern Architectures: A Dependence-based Approach}, publisher = {Morgan Kaufmann}, year = {2001}, isbn = {1-55860-286-0}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{andrews-etal:2004:zing, year={2004}, isbn={978-3-540-22940-7}, booktitle={CONCUR 2004 - Concurrency Theory}, volume={3170}, series={Lecture Notes in Computer Science}, editor={Gardner, Philippa and Yoshida, Nobuko}, doi={10.1007/978-3-540-28644-8_1}, title={Zing: Exploiting Program Structure for Model Checking Concurrent Software}, url={http://dx.doi.org/10.1007/978-3-540-28644-8_1}, publisher={Springer Berlin Heidelberg}, author={Andrews, Tony and Qadeer, Shaz and Rajamani, Sriram K. and Rehof, Jakob and Xie, Yichen}, pages={1-15} } @book{armstrong-etal:1996:erlang, author={Armstrong, J. and Virding, R. and Wikstr\"om, C. and Williams, M.}, year={1996}, title={Concurrent Programming in {E}rlang}, edition = {second}, publisher={Prentice Hall Europe}, address={Herfordshire, UK} } @misc{isp-takes-steves-exam, author = {Simone Atzeni and Chris Derrick}, title = {{ISP} {T}akes {S}teve's {M}idterm {E}xam}, note = {\url{http://www.cs.utah.edu/~simone/Steve_Midterm_Exam}}, year = 2009 } @inproceedings{auerbach-etal:2010:lime, author = {Auerbach, Joshua and Bacon, David F. and Cheng, Perry and Rabbah, Rodric}, title = {Lime: a {Java}-compatible and synthesizable language for heterogeneous architectures}, booktitle = {Proceedings of the ACM international conference on Object oriented programming systems languages and applications}, series = {OOPSLA '10}, year = {2010}, isbn = {978-1-4503-0203-6}, location = {Reno/Tahoe, Nevada, USA}, pages = {89--108}, numpages = {20}, url = {http://doi.acm.org/10.1145/1869459.1869469}, doi = {10.1145/1869459.1869469}, acmid = {1869469}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {fpga, functional programming, high level synthesis, object oriented, reconfigurable architecture, streaming, value type}, } @inproceedings{avgustinov-tibble-demoor:2007:tracematches, author = {Pavel Avgustinov and Julian Tibble and Oege de Moor}, title = {Making trace monitors feasible}, year = {2007}, pages = {589-608}, ee = {http://doi.acm.org/10.1145/1297027.1297070}, crossref = {DBLP:conf/oopsla/2007}, bibsource = {DBLP, http://dblp.uni-trier.de} } % BBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBB @inproceedings{babic-hu:2007:shared, author = {Domagoj Babi\'c and Alan J. Hu}, title = {Exploiting Shared Structure in Software Verification Conditions}, booktitle = {Haifa Verification Conference}, year = {2007}, pages = {169-184}, ee = {http://dx.doi.org/10.1007/978-3-540-77966-7_15}, crossref = {hvc2007}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{babic-hu:2008:calysto, author = {Domagoj Babi\'c and Alan J. Hu}, title = {Calysto: scalable and precise extended static checking}, year = {2008}, pages = {211-220}, ee = {http://doi.acm.org/10.1145/1368088.1368118}, crossref = {icse2008}, bibsource = {DBLP, http://dblp.uni-trier.de} } @book{baier-katoen:2008:model-checking, Author = {Baier, Christel and Katoen, Joost-Pieter}, Date-Added = {2010-07-30 02:49:00 -0400}, Date-Modified = {2010-08-28 23:00:47 -0400}, Isbn = {026202649X, 9780262026499}, Publisher = {The MIT Press}, Title = {Principles of Model Checking}, Year = {2008}} @misc{balaji-etal:2013:sctut, author = {Pavan Balaji and James Dinan and Torsten Hoefler and Rajeev Thakur}, title = {Advanced {MPI} Programming}, howpublished = {Tutorial at {SC13}: {I}nternational {C}onference on {H}igh {P}erformance {C}omputing, {N}etworking, {S}torage, and {A}nalysis, {D}enver, {C}olorado, {N}ovember 2013}, url = {http://www.mcs.anl.gov/~thakur/sc13-mpi-tutorial/} } @InProceedings{barnat-etal:2010:divine, author = "J. Barnat and L. Brim and M. \v{C}e\v{s}ka and P. Ro\v{c}kai", title = "{DiVinE}: {P}arallel Distributed Model Checker (Tool paper)", booktitle = "Parallel and Distributed Methods in Verification and High Performance Computational Systems Biology (HiBi/PDMC 2010)", pages = "4--7", year = "2010", publisher = "IEEE" } @InProceedings{barnat-etal:2013:divine, author = {Jiri Barnat and Lubos Brim and Vojtech Havel and Jan Havl\'{\i}cek and Jan Kriho and Milan Lenco and Petr Rockai and Vladim\'{\i}r Still and Jir\'{\i} Weiser}, title = "{DiVinE 3.0 -- An Explicit-State Model Checker for Multithreaded C \& C++ Programs}", pages = "863--868", crossref = {cav2013} } @article{backus-etal:1960:algol, author = {Backus, J. W. and Bauer, F. L. and Green, J. and Katz, C. and McCarthy, J. and Perlis, A. J. and Rutishauser, H. and Samelson, K. and Vauquois, B. and Wegstein, J. H. and van Wijngaarden, A. and Woodger, M.}, editor = {Naur, Peter}, title = {Report on the algorithmic language {ALGOL} 60}, journal = {Commun. ACM}, issue_date = {May 1960}, volume = {3}, number = {5}, month = may, year = {1960}, issn = {0001-0782}, pages = {299--314}, numpages = {16}, url = {http://doi.acm.org/10.1145/367236.367262}, doi = {10.1145/367236.367262}, acmid = {367262}, publisher = {ACM}, address = {New York, NY, USA}, } @inproceedings{barnett-leino:2005:wp, author = {Michael Barnett and K. Rustan M. Leino}, title = {Weakest-precondition of unstructured programs}, year = {2005}, pages = {82-87}, ee = {http://doi.acm.org/10.1145/1108792.1108813}, crossref = {paste2005}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{barnett-etal:2005:boogie, author = {Michael Barnett and Bor-Yuh Evan Chang and Robert DeLine and Bart Jacobs and K. Rustan M. Leino}, title = {Boogie: A Modular Reusable Verifier for Object-Oriented Programs}, year = {2005}, pages = {364-387}, ee = {http://dx.doi.org/10.1007/11804192_17}, crossref = {fmco2005}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{barrett-tinelli:2007:cvc3, Author = {Clark Barrett and Cesare Tinelli}, Bibsource = {DBLP, http://dblp.uni-trier.de}, Crossref = {cav2007}, Ee = {http://dx.doi.org/10.1007/978-3-540-73368-3_34}, Pages = {298--302}, Title = {{CVC3}}, Year = {2007}} @inproceedings{bauer-etal:2012:legion, author = {Michael Bauer and Sean Treichler and Elliott Slaughter and Alex Aiken}, title = {Legion: Expressing Locality and Independence with Logical Regions}, booktitle = {SC '12: Proc. Conference on High Performance Computing Networking, Storage and Analysis}, month = nov, year = 2012, note = {To appear}, } @ARTICLE{begstra-klop:1984:process-algebras, author = {J. A. Bergstra and J. W. Klop}, title = {Process algebra for synchronous communication}, journal = {Inform. and Control}, year = {1984}, pages = {109--137} } @inproceedings{TGRID10MB, author = {Martin Berzins and Justin Luitjens and Qingyu Meng and Todd Harman and Charles A. Wight and J. Peterson}, title = {Uintah: a scalable framework for hazard analysis}, booktitle = {Proc. of 2010 Teragrid Conf}, month = jul, year = 2010} @inproceedings{uintah-blue-waters, author = {Martin Berzins and, John Schmidt and Qingyu Meng and Alan Humphrey}, title = {Past, Present, and Future Scalability of the {Uintah} Software}, booktitle={Blue Waters Workshop}, year = 2012} @article{beyer-henzinger-etal:2007:blast, Annote = {BLAST is available at: \url{http://www.cs.sfu.ca/~dbeyer/Blast} }, Author = {Dirk Beyer and Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar}, Date-Added = {2012-02-03 17:40:43 +0000}, Date-Modified = {2012-02-03 17:40:43 +0000}, Journal = {International Journal on Software Tools for Technology Transfer (STTT)}, Keyword = {Software Model Checking}, Number = {5-6}, Pages = {505--525}, Pdf = {../../2007-STTT.The_Software_Model_Checker_BLAST.pdf}, Title = {The Software Model Checker {{\sc Blast}}: {Applications} to Software Engineering}, Volume = {9}, Year = {2007} } @inproceedings{beyer-keremogly:2011:cpa-tool, author = {Dirk Beyer and M. Erkan Keremoglu}, title = {{CPAchecker}: A Tool for Configurable Software Verification}, year = {2011}, pages = {184-190}, ee = {http://dx.doi.org/10.1007/978-3-642-22110-1_16}, crossref = {cav2011} } @inproceedings{beyer-henzinger-theoduloz:2007:cpa, author = {Dirk Beyer and Thomas A. Henzinger and Gr{\'e}gory Th{\'e}oduloz}, title = {Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis}, year = {2007}, pages = {504-518}, ee = {http://dx.doi.org/10.1007/978-3-540-73368-3_51}, crossref = {cav2007} } @inproceedings{bingham-rakamaric:2006:dp, author = {Jesse D. Bingham and Zvonimir Rakamari\'c}, title = {A Logic and Decision Procedure for Predicate Abstraction of Heap-Manipulating Programs}, year = {2006}, pages = {207-221}, ee = {http://dx.doi.org/10.1007/11609773_14}, crossref = {vmcai2006}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{bobo-etal:2011:boogie11why3, author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and Claude March\'e and Andrei Paskevich}, title = {Why3: Shepherd Your Herd of Provers}, booktitle = {Boogie 2011: First International Workshop on Intermediate Verification Languages}, year = 2011, hal = {http://hal.inria.fr/hal-00790310}, address = {Wroc\l{}aw, Poland}, month = {August}, pages = {53--64}, url = {http://proval.lri.fr/publications/boogie11final.pdf}, keywords = {Why3}, abstract = {Why3 is the next generation of the Why software verification platform. Why3 clearly separates the purely logical specification part from generation of verification conditions for programs. This article focuses on the former part. Why3 comes with a new enhanced language of logical specification. It features a rich library of proof task transformations that can be chained to produce a suitable input for a large set of theorem provers, including SMT solvers, TPTP provers, as well as interactive proof assistants.} } @article{bodden-lam-hendren:2012:typestate-partialeval, author = {Eric Bodden and Patrick Lam and Laurie J. Hendren}, title = {Partially Evaluating Finite-State Runtime Monitors Ahead of Time}, journal = {ACM Trans. Program. Lang. Syst.}, volume = {34}, number = {2}, year = {2012}, pages = {7}, ee = {http://doi.acm.org/10.1145/2220365.2220366}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{C++:MemoryModel, author = {Hans-Juergen Boehm and Sarita V. Adve}, title = {Foundations of the {C}++ concurrency memory model}, booktitle = {ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)}, year = {2008} } @article{boehm-adve-cacm-2012, author = {Hans-Juergen Boehm and Sarita V. Adve}, title = {You don't know jack about shared variables or memory models}, journal = {Commun. ACM}, volume = 55, number = 2, pages = {48-54}, year = 2012} @inproceedings{bouajjani-emmi:2012:bounded-phase, author = {Ahmed Bouajjani and Michael Emmi}, title = {Bounded Phase Analysis of Message-Passing Programs}, year = {2012}, pages = {451-465}, crossref = {tacas2012}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{bronevetsky:2009:dataflow, 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}, 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}, } @article{bronevetsky-supinski-omp, author = {Greg Bronevetsky and Bronis R. de Supinski}, title = {Complete Formal Specification of the {OpenMP} Memory Model}, journal = {International Journal of Parallel Programming}, volume = 35, number = 4, pages = {335-392}, year = 2007} % CCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCC @article{carlsson-etal:2006:toplas, author = {Carlsson, Richard and Sagonas, Konstantinos and Wilhelmsson, Jesper}, title = {Message analysis for concurrent programs using message passing}, journal = {ACM Trans. Program. Lang. Syst.}, issue_date = {July 2006}, volume = {28}, number = {4}, month = jul, year = {2006}, issn = {0164-0925}, pages = {715--746}, numpages = {32}, url = {http://doi.acm.org/10.1145/1146809.1146813}, doi = {10.1145/1146809.1146813}, acmid = {1146813}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {Erlang, Static analysis, concurrent languages, message passing, runtime systems}, } @inproceedings{chaki-etal:2006:tacas, author = {Sagar Chaki and Edmund M. Clarke and Nicholas Kidd and Thomas W. Reps and Tayssir Touili}, title = {Verifying Concurrent Message-Passing C Programs with Recursive Calls}, year = {2006}, pages = {334--349}, crossref = {tacas2006} } @article{chakrabarti-banerjee:2001:cssa-message, author = {Dhruva R. Chakrabarti and Prithviraj Banerjee}, title = {Static Single Assignment Form for Message-Passing Programs}, journal = {International Journal of Parallel Programming}, volume = {29}, number = {2}, year = {2001}, pages = {139-184}, ee = {http://dx.doi.org/10.1023/A:1007633018973}, bibsource = {DBLP, http://dblp.uni-trier.de} } @book{chapman-etal:2008:using-openmp, author = {Barbara Chapman and Gabriele Jost and Ruud van der Pas}, title = {Using {OpenMP}: Portable Shared Memory Parallel Programming}, year = {2008}, publisher = {MIT Press}, address = {Cambridge, Massachusetts}, url = {http://openmp.org/examples/Using-OpenMP-Examples-Distr.zip}, note = {(examples)} } @inproceedings{charles:2005:x10, author = {Charles, Philippe and Grothoff, Christian and Saraswat, Vijay and Donawa, Christopher and Kielstra, Allan and Ebcioglu, Kemal and von Praun, Christoph and Sarkar, Vivek}, title = {X10: an object-oriented approach to non-uniform cluster computing}, booktitle = {Proceedings of the 20th annual ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications}, series = {OOPSLA '05}, year = {2005}, isbn = {1-59593-031-0}, location = {San Diego, CA, USA}, pages = {519--538}, numpages = {20}, url = {http://doi.acm.org/10.1145/1094811.1094852}, doi = {10.1145/1094811.1094852}, acmid = {1094852}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {Java, X10, atomic blocks, clocks, data distribution, multithreading, non-uniform cluster computing (NUCC), partitioned global address space (PGAS), places, productivity, scalability}, } @inproceedings{chatterjee-etal:2007:havoc, author = {Shaunak Chatterjee and Shuvendu K. Lahiri and Shaz Qadeer and Zvonimir Rakamari\'c}, title = {A Reachability Predicate for Analyzing Low-Level Software}, year = {2007}, pages = {19-33}, ee = {http://dx.doi.org/10.1007/978-3-540-71209-1_4}, crossref = {tacas2007}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{chen-krishnamurthy-yelick, author = {W. Chen and A. Krishnamurthy and K. Yelick}, title = {Polynomial-time Algorithms for Enforcing Sequential Consistency in SPMD Programs with Arrays}, booktitle = {16th International Workshop on Languages and Compilers for Parallel Computing (LCPC)}, year = 2003} @inproceedings{christakis-sagonas:2011:padl, author = {Christakis, Maria and Sagonas, Konstantinos}, title = {Detection of asynchronous message passing errors using static analysis}, booktitle = {Proceedings of the 13th International Conference on Practical Aspects of Declarative Languages}, series = {PADL'11}, year = {2011}, isbn = {978-3-642-18377-5}, location = {Austin, TX, USA}, pages = {5--18}, numpages = {14}, url = {http://dl.acm.org/citation.cfm?id=1946313.1946318}, acmid = {1946318}, publisher = {Springer-Verlag}, address = {Berlin, Heidelberg}, } @misc{clang, howpublished={\url{http://clang.llvm.org}}, title={clang: a {C} language family front-end for {LLVM}}, year={2012}, key={clang} } @article{clarke:1976:symbolic, Acmid = {1313532}, Address = {Piscataway, NJ, USA}, Author = {Clarke, L. A.}, Date-Added = {2012-01-31 21:38:27 -0500}, Date-Modified = {2012-01-31 21:38:27 -0500}, Doi = {10.1109/TSE.1976.233817}, Issn = {0098-5589}, Issue = {3}, Journal = {IEEE Trans. Softw. Eng.}, Keywords = {test data generation, Program validation, software reliability, symbolic execution}, Month = {May}, Numpages = {8}, Pages = {215--222}, Publisher = {IEEE Press}, Title = {A System to Generate Test Data and Symbolically Execute Programs}, Url = {http://portal.acm.org/citation.cfm?id=1313320.1313532}, Volume = {2}, Year = {1976}, Bdsk-Url-1 = {http://portal.acm.org/citation.cfm?id=1313320.1313532}, Bdsk-Url-2 = {http://dx.doi.org/10.1109/TSE.1976.233817} } @incollection{clarke-etal:2004:cbmc, year={2004}, isbn={978-3-540-21299-7}, booktitle={Tools and Algorithms for the Construction and Analysis of Systems}, volume={2988}, series={Lecture Notes in Computer Science}, editor={Jensen, Kurt and Podelski, Andreas}, doi={10.1007/978-3-540-24730-2_15}, title={A Tool for Checking {ANSI-C} Programs}, url={http://dx.doi.org/10.1007/978-3-540-24730-2_15}, publisher={Springer Berlin Heidelberg}, author={Clarke, Edmund and Kroening, Daniel and Lerda, Flavio}, pages={168-176} } @misc{clj-ds:2014:web, title={clj-ds: {C}lojure's data structures modified for use outside of {C}lojure}, howpublished={\url{https://github.com/krukow/clj-ds}}, key={clj-ds}, year = {accessed Feb.\ 6, 2014} } @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 Practical System for Verifying Concurrent {C}}, Volume = {5674}, Year = {2009}, Bdsk-Url-1 = {http://dx.doi.org/10.1007/978-3-642-03359-9_2}} @inproceedings{condit-etal:2009:types, author = {Jeremy Condit and Brian Hackett and Shuvendu K. Lahiri and Shaz Qadeer}, title = {Unifying type checking and property checking for low-level code}, year = {2009}, pages = {302-314}, ee = {http://doi.acm.org/10.1145/1480881.1480921}, crossref = {popl2009}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{corbett-dwyer-hatcliff:2000:bandera, Address = {New York, NY, USA}, Author = {James C. Corbett and Matthew B. Dwyer and John Hatcliff and Shawn Laubach and Corina S. P\u{a}s\u{a}reanu and Robby and Hongjun Zheng}, Booktitle = {ICSE '00: Proceedings of the 22nd International Conference on Software Engineering}, Date-Added = {2008-07-13 16:40:50 -0400}, Date-Modified = {2008-07-13 17:10:42 -0400}, Doi = {http://doi.acm.org/10.1145/337180.337234}, Isbn = {1-58113-206-9}, Location = {Limerick, Ireland}, Pages = {439--448}, Publisher = {ACM}, Title = {Bandera: Extracting Finite-State Models from {Java} Source Code}, Year = {2000}, Bdsk-Url-1 = {http://doi.acm.org/10.1145/337180.337234}} @InProceedings{Corella:chdl97, author = {Francisco Corella}, title = {Verifying Memory Ordering Model of {I/O} Systems}, booktitle = {International Conference on Computer Hardware Description Languages and their Applications (CHDL)}, year = {1997}, optaddress = {Toledo, Spain}, optmonth = {apr}, note = {Invited Talk} } @InProceedings{cousot-cousot:1980:csp, author = {Cousot, P{.} and Cousot, R{.}}, title = {Semantic analysis of communicating sequential processes}, pages = {119--133}, editor = {de Bakker, J{.}W{.} and van Leeuwen, J{.}}, booktitle = {Seventh International Colloquium on Automata, Languages and Programming}, series = {Lecture Notes in Computer Science 85}, publisher = {Springer-Verlag, Berlin, Germany}, month = jul, year = 1980, } @misc{cpu-center, key = {cpu-center}, title = {{Center for Parallel Computing at Utah (CPU)}}, howpublished = {\url{http://www.parallel.utah.edu}}} @misc{cray:2012:chapel-spec, Author = {{Cray, Inc.}}, address = {Seattle, WA}, Howpublished = {\url{http://chapel.cray.com/spec/spec-0.92.pdf}}, Month = oct, day = 18, Title = {Chapel Language Specification, Version 0.92}, Year = {2012}} @misc{chapel, key = {chapel}, title = {The {Chapel} Parallel Programming Language}, howpublished = {\url{http://chapel.cray.com/}} } Misc{cuda-programming-guide, key = {cuda-programming-guide}, title = {{CUDA Programming Guide Version 4.0}}, howpublished = {\url{http://developer.download.nvidia.com/compute/cuda/4_0/toolkit/docs/CUDA_C_Programming_Guide.pdf}} } @Misc{cuda-programming-guide, author={NVIDIA}, title = {{CUDA C Programming Guide Version 5.0.}}, howpublished = {\url{http://docs.nvidia.com/cuda/cuda-c-programming-guide/}}, note = {accessed March 3, 2014} } @misc{cuda-sdk, author = {NVIDIA}, title = {{CUDA} Toolkit Release Archive}, howpublished = {\url{http://developer.nvidia.com/cuda-toolkit-archive}} } @inproceedings{cypher-leu:1995:races, author = {Cypher, R. and Leu, E.}, title = {Efficient race detection for message-passing programs with nonblocking sends and receives}, booktitle = {Proceedings of the 7th IEEE Symposium on Parallel and Distributeed Processing}, series = {SPDP '95}, year = {1995}, isbn = {0-8186-7195-5}, pages = {534--541}, url = {http://dl.acm.org/citation.cfm?id=829516.830632}, acmid = {830632}, publisher = {IEEE Computer Society}, address = {Washington, DC, USA}, keywords = {communication events, hazards and race conditions, logical clocks, message passing, message-passing programs, ordering relations, parallel message-passing programs, parallel programming, race detection, traced program}, } @inproceedings{cytron-ferrante-rosen-wegman-zadeck:1989:ssa, author = {Ron Cytron and Jeanne Ferrante and Barry K. Rosen and Mark N. Wegman and F. Kenneth Zadeck}, title = {An Efficient Method of Computing Static Single Assignment Form}, year = {1989}, pages = {25-35}, ee = {http://doi.acm.org/10.1145/75277.75280}, crossref = {DBLP:conf/popl/1989}, bibsource = {DBLP, http://dblp.uni-trier.de} } % DDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDD @inproceedings{danalis-etal:2010:gpgpu, author = {Anthony Danalis and Gabriel Marin and Collin McCurdy and Jeremy S. Meredith and Philip C. Roth and Kyle Spafford and Vinod Tipparaju and Jeffrey S. Vetter}, title = {The Scalable Heterogeneous Computing ({SHOC}) benchmark suite}, year = {2010}, pages = {63-74}, crossref = {2010gpgpu}, } @inproceedings{demartini-etal:1999:dspin, author = {Demartini, Claudio and Iosif, Radu and Sisto, Riccardo}, title = {{dSPIN}: A Dynamic Extension of {SPIN}}, booktitle = {Proceedings of the 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking}, year = {1999}, isbn = {3-540-66499-8}, pages = {261--276}, numpages = {16}, url = {http://dl.acm.org/citation.cfm?id=645879.672057}, acmid = {672057}, publisher = {Springer-Verlag}, address = {London, UK}, } @article{dijkstra:1975:guards, author = {Dijkstra, Edsger W.}, title = {Guarded commands, nondeterminacy and formal derivation of programs}, journal = {Commun. ACM}, issue_date = {Aug. 1975}, volume = {18}, number = {8}, month = aug, year = {1975}, issn = {0001-0782}, pages = {453--457}, numpages = {5}, url = {http://doi.acm.org/10.1145/360933.360975}, doi = {10.1145/360933.360975}, acmid = {360975}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {case-construction, correctness proof, derivation of programs, nondeterminancy, program semantics, programming language semantics, programming languages, programming methodology, repetition, sequencing primitives, termination}, } @inproceedings{dolbeau:2007:hmpp, title={{HMPP}: {A} hybrid multi-core parallel programming environment}, author={Dolbeau, R. and Bihan, S. and Bodin, F.}, booktitle={Workshop on General Purpose Processing on Graphics Processing Units (GPGPU 2007)}, year={2007} } @article{dwyer-clarke-cobleigh-naumovich:2004:flavers, author = {Matthew B. Dwyer and Lori A. Clarke and Jamieson M. Cobleigh and Gleb Naumovich}, title = {Flow analysis for verifying properties of concurrent software systems}, journal = {ACM Trans. Softw. Eng. Methodol.}, volume = {13}, number = {4}, year = {2004}, pages = {359-430}, ee = {http://doi.acm.org/10.1145/1040291.1040292}, bibsource = {DBLP, http://dblp.uni-trier.de} } @INPROCEEDINGS{dwyer-avrunin-corbett:1999:specpatterns, AUTHOR = {M.B.~Dwyer and G.~Avrunin and J.~Corbett}, TITLE = {Patterns in Property Specifications for Finite-State Verification}, booktitle = {{Int'l. Conf. on Soft. Eng.}}, month = may, year = {1999}, pages = {411--420}, } @article{dwyer-etal:2004:por, Acmid = {1017112}, Address = {Hingham, MA, USA}, Author = {Dwyer, Matthew B. and Hatcliff, John and Robby and Ranganath, Venkatesh Prasad}, Date-Added = {2011-05-14 21:47:58 -0400}, Date-Modified = {2011-05-14 21:49:01 -0400}, Issue = {2-3}, Journal = {Form. Methods Syst. Des.}, Keywords = {escape analysis, locking discipline, partial order reduction, software model checking, software verifcation}, Month = {September}, Numpages = {42}, Pages = {199--240}, Publisher = {Kluwer Academic Publishers}, Title = {Exploiting Object Escape and Locking Information in Partial-Order Reductions for Concurrent Object-Oriented Programs}, Volume = {25}, Year = {2004}, Bdsk-Url-1 = {http://portal.acm.org/citation.cfm?id=1017107.1017112}, Bdsk-Url-2 = {http://dx.doi.org/10.1023/B:FORM.0000040028.49845.67}} % EEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEE @inproceedings{emmi-qadeer-rakamaric:2011:delay-bounding, author = {Michael Emmi and Shaz Qadeer and Zvonimir Rakamari\'c}, title = {Delay-bounded scheduling}, year = {2011}, pages = {411-422}, ee = {http://doi.acm.org/10.1145/1926385.1926432}, crossref = {popl2011}, bibsource = {DBLP, http://dblp.uni-trier.de} } % FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF @article{felker-etal:2012:nuclear, author = {Kyle G. Felker and Andrew R. Siegel and Stephen F. Siegel}, title = {Optimizing Memory Constrained Environments in {M}onte {C}arlo Nuclear Reactor Simulations}, journal = {International Journal of High Performance Computing Applications}, publisher = {SAGE Publications}, year = {2012}, month = jun, day = 4, note = {Online first, \url{http://hpc.sagepub.com/content/early/2012/06/04/1094342012445627}} } @inproceedings{filliatre-paskevich:2013:why3-esop, author = {Filli\^{a}tre, Jean-Christophe and Paskevich, Andrei}, title = {Why3: Where Programs Meet Provers}, crossref = {esop2013}, pages = {125--128}, numpages = {4}, url = {http://dx.doi.org/10.1007/978-3-642-37036-6_8}, doi = {10.1007/978-3-642-37036-6_8} } @article{fink-yahav-dor-ramalingam-geay:2008:typestate-aliasing, author = {Stephen J. Fink and Eran Yahav and Nurit Dor and G. Ramalingam and Emmanuel Geay}, title = {Effective typestate verification in the presence of aliasing}, journal = {ACM Trans. Softw. Eng. Methodol.}, volume = {17}, number = {2}, year = {2008}, ee = {http://doi.acm.org/10.1145/1348250.1348255}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{fischer-etal:2013:cseq, author = {Fischer, Bernd and Inverso, Omar and Parlato, Gennaro}, title = {{CSeq}: A Sequentialization Tool for {C}}, pages = {616--618}, numpages = {3}, url = {http://dx.doi.org/10.1007/978-3-642-36742-7_46}, doi = {10.1007/978-3-642-36742-7_46}, acmid = {2450453}, crossref={tacas2013} } @inproceedings{flanagan-etal:2002:esc-java, author = {Cormac Flanagan and K. Rustan M. Leino and Mark Lillibridge and Greg Nelson and James B. Saxe and Raymie Stata}, title = {Extended Static Checking for {Java}}, year = {2002}, pages = {234-245}, ee = {http://doi.acm.org/10.1145/512529.512558}, crossref = {pldi2002}, bibsource = {DBLP, http://dblp.uni-trier.de} } @misc{flatt-etal:2012:racket, howpublished={\url{http://docs.racket-lang.org/reference/}}, note={retrieved Nov.\ 19, 2012}, author={Matthew Flatt and PLT}, title={The {Racket} Reference, version 5.3.1} } @InProceedings{frigo-etal:1998:cilk, author = {Matteo Frigo and Charles E. Leiserson and Keith H. Randall}, address = {Montreal, Quebec, Canada}, booktitle = {Proceedings of the ACM SIGPLAN '98 Conference on Programming Language Design and Implementation (PLDI)}, month = jun, note = {Proceedings published ACM SIGPLAN Notices, Vol. 33, No. 5, May, 1998.}, year = {1998}, pages = {212--223}, title = {The Implementation of the {C}ilk-5 Multithreaded Language} } % GGGGGGGGGGGGGGGGGGGGGGGGGGGGGGGGGGGGGGGGGGGGGGGGGGGGGGGGGGGGGGGGGGGGGG @inproceedings{ganai-gupta:2008:csbmc, author = {Malay K. Ganai and Aarti Gupta}, title = {Efficient Modeling of Concurrent Systems in BMC}, year = {2008}, pages = {114-133}, crossref = {spin2008}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{garland-kudlur-zheng:2012:phalanx, author = {Michael Garland and Manjunath Kudlur and Yili Zheng}, title = {Designing a Unified Programming Model for Heterogeneous Machines}, booktitle = {SC '12: Proc. Conference on High Performance Computing Networking, Storage and Analysis}, month = nov, year = 2012, note = {To appear}, } @inproceedings{ghafari-etal:2010:empirical, author = {Naghmeh Ghafari and Alan J. Hu and Zvonimir Rakamari\'c}, title = {Context-Bounded Translations for Concurrent Software: An Empirical Evaluation}, year = {2010}, pages = {227-244}, crossref = {spin2010}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{giannakopoulou-etal:2012:psyco, author = {Dimitra Giannakopoulou and Zvonimir Rakamari\'c and Vishwanath Raman}, title = {Symbolic Learning of Component Interfaces}, year = {2012}, pages = {248-264}, ee = {http://dx.doi.org/10.1007/978-3-642-33125-1_18}, crossref = {sas2012}, bibsource = {DBLP, http://dblp.uni-trier.de} } @misc{brandon-gibson-sc11-poster, title = {{GEM}: A Formal Dynamic Verification Environment for HPC Pedagogy}, author = {Brandon L. Gibson}, booktitle = {Supercomputing}, year = 2011, note = {{\sl Student Research Poster Competition Entry}}} @misc{godefroid-nagappan:2008:bugs, title={Concurrency at Microsoft--An exploratory survey}, author={Godefroid, Patrice and Nagappan, Nachiappan}, booktitle={CAV Workshop on Exploiting Concurrency Efficiently and Correctly}, year={2008}, howpublished={\url{http://www.cs.utah.edu/old-ec2-dir/2008/papers/ec2-pp1.pdf}} } @inproceedings{verisoft-popl97, author = {Patrice Godefroid}, title = {Model checking for programming languages using {VeriSoft}}, booktitle = {Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages}, year = 1997, pages = {174--186}} @book{godefroid:1996:por-book, Author = {Patrice Godefroid}, Bibsource = {DBLP, http://dblp.uni-trier.de}, Date-Added = {2010-08-28 23:09:36 -0400}, Date-Modified = {2010-08-28 23:09:57 -0400}, Isbn = {3-540-60761-7}, Publisher = {Springer}, Series = {Lecture Notes in Computer Science}, Title = {Partial-Order Methods for the Verification of Concurrent Systems - An Approach to the State-Explosion Problem}, Volume = {1032}, Year = {1996}} @article{godefroid-etal:2012:sage, author = {Patrice Godefroid and Michael Y. Levin and David A. Molnar}, title = {{SAGE}: whitebox fuzzing for security testing}, journal = {Commun. ACM}, volume = {55}, number = {3}, year = {2012}, pages = {40-44}, ee = {http://doi.acm.org/10.1145/2093548.2093564}, bibsource = {DBLP, http://dblp.uni-trier.de} } @Misc{fm09-tut, author = "Ganesh Gopalakrishnan", month = nov, year = "2009", note = "FM 2009, Eindhoven", title = "Tutorial 03: Practical {MPI} and {Pthread} Dynamic Verification", } @Misc{fm08-tut, month = may, year = "2008", note = "Tutorial: Runtime Model Checking of Multithreaded C Programs using Automated Instrumentation Dynamic Partial Order Reduction and Distributed Checking (half day) (T6), Turku", author = "Ganesh Gopalakrishnan and Yu Yang", } @Misc{ppopp10-tut, author = "Ganesh Gopalakrishnan", year = "2010", title = "Tutorial: Dynamic Verification of Message Passing and Threading", note = "PPoPP, Bangalore", month = jan, } @Misc{europvm09-tut, author = "Ganesh Gopalakrishnan", key = "europvm09-tut", title = "Invited Full-Day Tutorial: Practical Formal Verification of {MPI} and Thread Programs", note = "EuroPVM/MPI, Espoo", year = "2009", month = nov, } @misc{fm2012-tut, author = {Ganesh Gopalakrishnan}, title = {{S}ymbolic Analysis of {GPU} Programs for Correctness and Performance}, note = {FM 2012 Conference, Paris, June}} @Misc{ics09-tut, note = "ICS, Yorktown Heights", year = "2009", month = jun, title = "Tutorial {T8}: Practical Formal Verification of {MPI} and Thread Programs", author = "Ganesh Gopalakrishnan", } @inproceedings{qb-or-not-qb, author = {Ganesh Gopalakrishnan and Yue Yang and Hemanthkumar Sivaraj}, title = {{QB} or not {QB}: An Efficient Execution Verification Tool for Memory Orderings}, booktitle = {CAV (Computer Aided Verification)}, pages = {401-413}, note = {LNCS 3113}, year = 2004} @article{gopalakrishnan-etal:2011:cacm, Acmid = {2043194}, Address = {New York, NY, USA}, Author = {Gopalakrishnan, Ganesh and Kirby, Robert M. and Siegel, Stephen and Thakur, Rajeev and Gropp, William and Lusk, Ewing and De Supinski, Bronis R. and Schulz, Martin and Bronevetsky, Greg}, Doi = {10.1145/2043174.2043194}, Issn = {0001-0782}, Issue_Date = {December 2011}, Journal = {Communications of the ACM}, Month = dec, Number = {12}, Numpages = {10}, Pages = {82--91}, Publisher = {ACM}, Title = {Formal analysis of {MPI}-based parallel programs}, Url = {http://doi.acm.org/10.1145/2043174.2043194}, Volume = {54}, Year = {2011}, Bdsk-Url-1 = {http://doi.acm.org/10.1145/2043174.2043194}, Bdsk-Url-2 = {http://dx.doi.org/10.1145/2043174.2043194}} @misc{sc10-ganesh-half-day-tut, title = {Scalable Dynamic Formal Verification and Correctness Checking of {MPI} Applications}, author = {Ganesh Gopalakrishnan and Matthias S. {M\"uller} and Bronis R. {de Supinski}}, note = {Half Day Tutorial at SC'10, New Orleans, November 2010}} @inproceedings{grossman:2002:cyclone, author = {Grossman, Dan and Morrisett, Greg and Jim, Trevor and Hicks, Michael and Wang, Yanling and Cheney, James}, title = {Region-based memory management in {Cyclone}}, booktitle = {Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation}, series = {PLDI '02}, year = {2002}, isbn = {1-58113-463-0}, location = {Berlin, Germany}, pages = {282--293}, numpages = {12}, url = {http://doi.acm.org/10.1145/512529.512563}, doi = {10.1145/512529.512563}, acmid = {512563}, publisher = {ACM}, address = {New York, NY, USA}, } % HHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHH @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} } @book{herlihy-shavit, author = {Maurice Herlihy and Nir Shavit}, title = {The Art of Multiprocessor Programming}, publisher = {Morgan Kaufmann}, year = 2008} @inproceedings{hickey:2008:clojure, author = {Hickey, Rich}, title = {The {C}lojure programming language}, booktitle = {Proceedings of the 2008 Symposium on Dynamic languages}, series = {DLS '08}, year = {2008}, isbn = {978-1-60558-270-2}, location = {Paphos, Cyprus}, pages = {1:1--1:1}, articleno = {1}, numpages = {1}, url = {http://doi.acm.org/10.1145/1408681.1408682}, doi = {10.1145/1408681.1408682}, acmid = {1408682}, publisher = {ACM}, address = {New York, NY, USA}, } @article{hoare:1978:csp, author = {Hoare, C. A. R.}, title = {Communicating sequential processes}, journal = {Commun. ACM}, issue_date = {Aug. 1978}, volume = {21}, number = {8}, month = aug, year = {1978}, issn = {0001-0782}, pages = {666--677}, numpages = {12}, url = {http://doi.acm.org/10.1145/359576.359585}, doi = {10.1145/359576.359585}, acmid = {359585}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {classes, concurrency, conditional critical regions, coroutines, data representations, guarded commands, input, iterative arrays, monitors, multiple entries, multiple exits, nondeterminacy, output, parallel programming, procedures, program structures, programming, programming languages, programming primitives, recursion}, } @article{hochstein-basili:2008:parallel, author = {Hochstein, Lorin and Basili, Victor R.}, title = {The {ASC-Alliance} Projects: A Case Study of Large-Scale Parallel Scientific Code Development}, journal = {Computer}, issue_date = {March 2008}, volume = {41}, number = {3}, month = mar, year = {2008}, issn = {0018-9162}, pages = {50--58}, numpages = {9}, url = {http://dx.doi.org/10.1109/MC.2008.101}, doi = {10.1109/MC.2008.101}, acmid = {1399158}, publisher = {IEEE Computer Society Press}, address = {Los Alamitos, CA, USA}, keywords = {computing methodologies, scientific code development, simulation, software engineering, software engineering, computing methodologies, scientific code development, simulation}, } @book{holzmann:2004:spin_book, Address = {Boston}, Author = {Gerard J. Holzmann}, Publisher = {Addison-Wesley}, Title = {The {\textsc{Spin}} Model Checker}, Year = 2004} @article{fmsd-ravi, author = {Ravi Hosabettu and Ganesh Gopalakrishnan and Mandayam Srivas}, title = {Formal Verification of a Complex Pipelined Processor}, journal = {Formal Methods in System Design}, Volume = 23, Number = 2, month = sep, year = 2003, pages = {171-213}} @misc{alan-humphrey-sc10-poster, author = {Alan Humphrey}, title = {An Integration of Dynamic {MPI} Formal Verification Within {Eclipse} {PTP}}, booktitle = {Supercomputing - ACM Student Research Poster Competition}, year = 2010, note = {{\sl Won 2nd place}}} @inproceedings{GEM-psti-paper, author = {Alan Humphrey and Christopher Derrick and Ganesh Gopalakrishnan and Beth R. Tibbitts}, title = {{GEM}: Graphical Explorer for {MPI} Programs}, booktitle = {{Parallel Software Tools and Tool Infrastructures (ICPP workshop)}}, note = {\url{http://www.cs.utah.edu/fv/GEM}}, year = 2010} @inproceeedings{alan-humphrey:xsede2012, author = {Alan Humphrey and Qingyu Meng and Martin Berzins and Todd Harman}, title = {Radiation Modeling Using the {Uintah} Heterogeneous {CPU/GPU} Runtime System}, booktitle = {Extreme Science and Engineering Discovery Environment (XSEDE 2012)}, year = 2012} % IIIIIIIIIIIIIIIIIIIIIIIIIIIIIIIIIIIIIIIIIIIIIIIIIIIIIIIIIIIIIIIIIIIIII @book{ieee:2008:posix, author={{Institute of Electrical and Electronics Engineers, Inc.}}, title={{IEEE} {S}tandard for {I}nformation {T}echnology---{P}ortable {O}perating {S}ystem {I}nterface ({POSIX}) {B}ase {S}pecifications, Issue 7, {IEEE Std 1003.1-2008} ({R}evision of {IEEE Std 1003.1-2004})}, publisher={IEEE}, year={2008}, month=dec, day=1, address={3 Park Avenue, New York, NY 10016-5997, USA} } @Misc{Inspect-release, key = "inspect-release", title = "Release Information for {Inspect}", note = "\url{http://www.cs.utah.edu/fv/Inspect}", } @book{iso-iee:2011:C, author = {{ISO/IEC}}, title = {{ISO/IEC} 9899:2011: International Standard: Programming Languages --- {C}}, publisher = {American National Standards Institute}, year = 2011, month = apr, day = 12, notes = {\url{http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1570.pdf}} } @misc{isp-release, key = "ISP release", title = "Release Information for {ISP}", note={\url{http://www.cs.utah.edu/fv/ISP}} } @misc{isp-eclipse, key = "GEM release", title = "Release Information for {GEM}", note={\url{http://www.cs.utah.edu/fv/GEM}} } @misc{isp-tests-against-marmot, key = "ISP Tests", title = "{LLNL} {U}mpire {T}est {S}uite {E}xecuted {U}sing {N}atively, {ISP}, and {M}armot", note ={\url{http://www.cs.utah.edu/fv/ISP_Tests/}}} % JJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJ @ARTICLE{Jacobson99, author = "Hans M. Jacobson and Ganesh Gopalakrishnan", title = "Application-Specific Programmable Control for High-Performance Asynchronous Circuits", pages = "319--331", journal= "Proceedings of {IEEE}", volume = 87, number = 2, month = feb, year = 1999 } @inproceedings{jenista-eom-demsky:2011:disjointreachability, author = {James Christopher Jenista and Yong Hun Eom and Brian Demsky}, title = {Using Disjoint Reachability for Parallelization}, year = {2011}, pages = {198-224}, ee = {http://dx.doi.org/10.1007/978-3-642-19861-8_12}, crossref = {DBLP:conf/cc/2011}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{sen:cav2009, author = {Pallavi Joshi and Mayur Naik and {C.-S} Park and Koushik Sen}, title = {An Extensible Active Testing Framework for Concurrent Programs}, crossref = {cav2009}, pages = {675-681}, year = 2009} @misc{json, howpublished={\url{http://www.json.org}}, title={{JavaScript} {O}bject {N}otation ({JSON})}, year={2012}, key={json} } % KKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKK @article{keller:1976:transitions, author = {Keller, Robert M.}, title = {Formal verification of parallel programs}, journal = {Commun. ACM}, issue_date = {July 1976}, volume = {19}, number = {7}, month = jul, year = {1976}, issn = {0001-0782}, pages = {371--384}, numpages = {14}, url = {http://doi.acm.org/10.1145/360248.360251}, doi = {10.1145/360248.360251}, acmid = {360251}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {Petri nets, assertions, correctness, deadlock, mutual exclusion, parallel program, verification}, } @misc{opencl:2011:standard:1.2.15, author={Khronos Group}, year = 2011, month = nov, title = {{OpenCL} - {T}he open standard for parallel programming of heterogeneous systems {A}pplication {P}rogram {I}nterface, {V}ersion 3.1}, howpublished = {\url{http://www.khronos.org/registry/cl/specs/opencl-1.2.pdf}} } @inproceedings{khurshid-pasareanu-visser:2003:tacas, Author = {Sarfraz Khurshid and Corina S. P\v{a}s\v{a}reanu and Willem Visser}, Bibsource = {DBLP, http://dblp.uni-trier.de}, Crossref = {tacas2003}, Date-Added = {2012-01-31 21:39:30 -0500}, Date-Modified = {2012-01-31 21:40:02 -0500}, Ee = {http://link.springer.de/link/service/series/0558/bibs/2619/26190553.htm}, Pages = {553-568}, Title = {{Generalized Symbolic Execution for Model Checking and Testing}}, Year = {2003}} @inproceedings{kim:2012:opencl, author = {Kim, Jungwon and Seo, Sangmin and Lee, Jun and Nah, Jeongho and Jo, Gangwon and Lee, Jaejin}, title = {{OpenCL} as a unified programming model for heterogeneous {CPU/GPU} clusters}, booktitle = {Proceedings of the 17th ACM SIGPLAN symposium on Principles and Practice of Parallel Programming}, series = {PPoPP '12}, year = {2012}, isbn = {978-1-4503-1160-1}, location = {New Orleans, Louisiana, USA}, pages = {299--300}, numpages = {2}, url = {http://doi.acm.org/10.1145/2145816.2145863}, doi = {10.1145/2145816.2145863}, acmid = {2145863}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {OpenCL, clusters, heterogeneous computing, programming models}, } @inproceedings{kimpe:aesop:2012, author = {Dries Kimpe and Philip Carns and Kevin Harms and Justin M Wozniak and Samuel Lang and Robert Ross}, title = {{AESOP}: {E}xpressing {C}oncurrency in {H}igh-{P}erformance {S}ystem {S}oftware}, booktitle = {2012 IEEE 7th International Conference on Networking, Architecture and Storage (NAS)}, pages = {303-312}, publisher = {IEEE}, year = 2012} @article{king:1976:symbolic, Address = {New York, NY, USA}, Author = {James C. King}, Date-Added = {2012-01-31 21:37:26 -0500}, Date-Modified = {2012-01-31 21:37:26 -0500}, Doi = {http://doi.acm.org/10.1145/360248.360252}, Issn = {0001-0782}, Journal = {Communications of the ACM}, Number = {7}, Pages = {385--394}, Publisher = {ACM}, Title = {{Symbolic Execution and Program Testing}}, Volume = {19}, Year = {1976}, Bdsk-Url-1 = {http://doi.acm.org/10.1145/360248.360252} } @article{krishnamurthy-yelick, author = {Arvind Krishnamurthy and Katherine Yelick}, title = {Analyses and optimizations for shared address space programs}, journal = {Jorunal of Parallel and Distributed Computing}, year = 1996} @misc{paul-e-mckenney, title = {Is Parallel Programming Hard, And, If So, What Can You Do}, author = {Paul E. McKenney}, note = {\url{http://kernel.org/pub/linux/kernel/people/paulmck/perfbook/perfbook.html}}, year = 2012, month = aug} % LLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLL @inproceedings{lahiri-qadeer-rakamaric:2009:storm, author = {Shuvendu K. Lahiri and Shaz Qadeer and Zvonimir Rakamari\'c}, title = {Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers}, year = {2009}, pages = {509-524}, crossref = {cav2009}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{lal-reps:2008:seq, author = {Akash Lal and Thomas W. Reps}, title = {Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis}, year = {2008}, pages = {37-51}, crossref = {cav2008}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{lal-etal:2008:npcomp, author = {Akash Lal and Tayssir Touili and Nicholas Kidd and Thomas W. Reps}, title = {Interprocedural Analysis of Concurrent Programs Under a Context Bound}, year = {2008}, pages = {282-298}, crossref = {tacas2008}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{lal-etal:2012:corral, author = {Akash Lal and Shaz Qadeer and Shuvendu K. Lahiri}, title = {A Solver for Reachability Modulo Theories}, year = {2012}, pages = {427--443}, ee = {http://dx.doi.org/10.1007/978-3-642-31424-7_32}, crossref = {cav2012} } @inproceedings{lattner-adve:2005:poolallocation, author = {Chris Lattner and Vikram S. Adve}, title = {Automatic pool allocation: improving performance by controlling data structure layout in the heap}, year = {2005}, pages = {129-142}, ee = {http://doi.acm.org/10.1145/1065010.1065027}, crossref = {pldi2005}, bibsource = {DBLP, http://dblp.uni-trier.de} } @article{lee-midkiff-padua:1998:cssa-cobegin, author = {Jaejin Lee and Samuel P. Midkiff and David A. Padua}, title = {A Constant Propagation Algorithm for Explicitly Parallel Programs}, journal = {International Journal of Parallel Programming}, volume = {26}, number = {5}, year = {1998}, pages = {563-589}, ee = {http://dx.doi.org/10.1023/A:1018772514882}, bibsource = {DBLP, http://dblp.uni-trier.de} } @misc{leino:2008:boogie, title = {This is {B}oogie 2}, howpublished={\url{http://research.microsoft.com/apps/pubs/default.aspx?id=147643}}, author={K. Rustan M. Leino}, year = 2008, day = 24, month = jun, pubisher = {Microsoft Research} } @inproceedings{fse10-guodong, author = {Guodong Li and Ganesh Gopalakrishnan}, title = {Scalable {SMT}-based verification of {GPU} kernel functions}, booktitle = {{\em Foundations of Software Engineering}}, year = 2010, note = {\url{http://www.cs.utah.edu/fv/PUG} tool}} @InProceedings{Gklee:PPoPP12, author = {Guodong Li and Peng Li and Geof Sawaya and Ganesh Gopalakrishnan and Indradeep Ghosh and Sreeranga P. Rajan}, title = {{GKLEE}: {C}oncolic Verification and Test Generation for {GPUs}}, booktitle = {{PPoPP}}, year = 2012, note = {http://www.cs.utah.edu/fv/GKLEE} } @article{ligd09-science-comp-prog, author = { Guodong Li and Robert Palmer and Michael DeLisi and Ganesh Gopalakrishnan and Robert M. Kirby}, title = {Formal Specification of {MPI} 2.0: Case Study in Specifying a Practical Concurrent Programming {API}}, journal = {Science of Computer Programming}, year = 2010, url = {http://dx.doi.org/10.1016/j.scico.2010.03.007} } @inproceedings{gklee-sc12, author = { Peng Li and Guodong Li and Ganesh Gopalakrishnan}, title = {{P}arametric {F}lows: Automated Behavior Equivalencing for Symbolic Analysis of Races in CUDA Programs}, booktitle = { Supercomputing }, year = 2012 } @article{lusk-etal:2010:adlb, author = "Ewing Lusk and Steven Pieper and Ralph Butler", title = {More Scalability, Less Pain}, journal = {SciDAC Review}, volume = "17", pages = "30--37", year = "2010", url = "http://www.scidacreview.org/1002/html/adlb.html" } % MMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMM @inproceedings{sela-cav2012, author = {Sela Mador-Haim and Luc Maranget and Susmit Sarkar and Kayvan Memarian and Jade Alglave and Scott Owens and Rajeev Alur and Milo M. K. Martin and Peter Sewell and Derek Williams}, title = {An Axiomatic Memory Model for POWER Multiprocessors}, booktitle = {CAV}, year = 2012, pages = {495-512}} @book{manna-pnueli:1992:temporal, author = {Manna, Zohar and Pnueli, Amir}, title = {The temporal logic of reactive and concurrent systems}, year = {1992}, isbn = {0-387-97664-7}, publisher = {Springer-Verlag}, address = {New York, NY, USA} } @inproceedings{jmm-popl-2005, author = {Jeremy Manson and William Pugh and Sarita V. Adve}, title = {The {Java} memory model}, booktitle = {POPL}, year = 2005, pages = {378-391}} @inproceedings{marron-kapur-hermenegildo:2009:relatedheap, author = {Mark Marron and Deepak Kapur and Manuel V. Hermenegildo}, title = {Identification of logically related heap regions}, booktitle = {ISMM}, year = {2009}, pages = {89-98}, ee = {http://doi.acm.org/10.1145/1542431.1542445}, crossref = {DBLP:conf/iwmm/2009}, bibsource = {DBLP, http://dblp.uni-trier.de} } @InProceedings{techcon09-meakin, author = "Ben Meakin and Ganesh Gopalakrishnan", title = "Hardware Design, Synthesis, and Verification of a Multicore Communication {API}", month = sep, year = "2009", booktitle = "SRC Techcon, Austin, TX", } @misc{meng2012uintah, title={The {Uintah} Framework: A Unified Heterogeneous Task Scheduling and Runtime System}, author={Meng, Q. and Humphrey, A. and Berzins, M.}, year={2012}, note={Extended Abstract} } @misc{mpi-forum:2012:mpi30, author = {{Message Passing Interface Forum}}, title = {{MPI}: A Message-Passing Interface Standard, Version 3.0}, month = sep, day = 21, year = 2012, howpublished = {\url{http://www.mpi-forum.org/docs/docs.html}} } @misc{mpich2, key = {MPICH2}, title = {{MPICH2}}, howpublished = {\url{http://www.mcs.anl.gov/mpi/mpich2}}, } @misc{microsoft:2005:zingspec, howpublished={\url{http://research.microsoft.com/en-us/projects/zing/zinglanguagespecification.pdf}}, year = 2005, title = {Zing Language Specification, {M}icrosoft {C}orporation}, key = {Zing} } @article{midkiff-lee-padua, title= {A compiler for multiple memory models}, author = {Sam P. Midkiff and Jaejin Lee and David A. Padua}, journal = {Concurrency, Practice and Experience}, pages = {197-220}, volume = 16, number = 2, month = feb, year = 2004} @book{milner:1989:cc, author = {Milner, Robin}, title = {Communication and concurrency}, year = {1989}, isbn = {0-13-115007-3}, publisher = {Prentice-Hall, Inc.}, address = {Upper Saddle River, NJ, USA} } @book{milner:1999:pi, author = {Milner, Robin}, title = {Communicating and mobile systems: the $\pi$-calculus}, year = {1999}, isbn = {0-521-65869-1}, publisher = {Cambridge University Press}, address = {New York, NY, USA} } @misc{mpich, key = {MPICH}, title = {{MPICH}}, howpublished = {\url{http://www.mpich.org}} } @misc{sc11-ganesh-tut, author = {Matthias M\"{u}ller and Bronis de Supinski and Ganesh Gopalakrishnan and Tobias Hilbrich and David Lecomber}, title = {{Dealing with {MPI} Bugs at Scale: Best Practices, Automatic Detection, Debugging, and Formal Verification}}, note = {Full-day Tutorial at Supercomputing}, howpublished = {Slides presented in this tutorial, integrating presentations from Dresden, Allinea, LLNL, and Utah: \url{http://www.cs.utah.edu/fv/publications/sc11_with_handson.pptx}}, month = nov, year = 2011} @misc{sc12-ganesh-tut, author = {Matthias M\"{u}ller and Bronis de Supinski and Ganesh Gopalakrishnan and Tobias Hilbrich and David Lecomber}, title = {Debugging {MPI} and {CUDA} at Scale}, note = {Full-day Tutorial at Supercomputing}, howpublished = {Slides presented in this tutorial, integrating presentations from Dresden, Allinea, LLNL, and Utah: \url{http://www.cs.utah.edu/fv/publications/sc12_with_handson.pptx}}, month = nov, year = 2012} @inproceedings{musuvathi-qadeer:2007:chess, author = {Madanlal Musuvathi and Shaz Qadeer}, title = {Iterative context bounding for systematic testing of multithreaded programs}, year = {2007}, pages = {446-455}, ee = {http://doi.acm.org/10.1145/1250734.1250785}, crossref = {pldi2007}, bibsource = {DBLP, http://dblp.uni-trier.de} } % NNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNN @article{nickolls:2008:cuda, author = {Nickolls, John and Buck, Ian and Garland, Michael and Skadron, Kevin}, title = {Scalable Parallel Programming with CUDA}, journal = {Queue}, issue_date = {March/April 2008}, volume = {6}, number = {2}, month = mar, year = {2008}, issn = {1542-7730}, pages = {40--53}, numpages = {14}, url = {http://doi.acm.org/10.1145/1365490.1365500}, doi = {10.1145/1365490.1365500}, acmid = {1365500}, publisher = {ACM}, address = {New York, NY, USA}, } @inproceedings{naeem-lhotak:2008:typestate-multi, author = {Nomair A. Naeem and Ondrej Lhot{\'a}k}, title = {Typestate-like analysis of multiple interacting objects}, year = {2008}, pages = {347-366}, ee = {http://doi.acm.org/10.1145/1449764.1449792}, crossref = {DBLP:conf/oopsla/2008}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{naumovich-avrunin:1998:mhp, author = {Gleb Naumovich and George S. Avrunin}, title = {A Conservative Data Flow Algorithm for Detecting All Pairs of Statement That May Happen in Parallel}, booktitle = {SIGSOFT FSE}, year = {1998}, pages = {24-34}, ee = {http://doi.acm.org/10.1145/288195.288213}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{novillo-unrau-schaeffer:1998:cssa-mutex, author = {Diego Novillo and Ronald C. Unrau and Jonathan Schaeffer}, title = {Concurrent {SSA} Form in the Presence of Mutual Exclusion}, year = {1998}, pages = {356-}, ee = {http://computer.org/proceedings/icpp/8650/86500356abs.htm}, crossref = {DBLP:conf/icpp/1998}, bibsource = {DBLP, http://dblp.uni-trier.de} } @article{numrich:1998:coarrayfortran, author = {Numrich, Robert W. and Reid, John}, title = {Co-array Fortran for parallel programming}, journal = {SIGPLAN Fortran Forum}, issue_date = {Aug. 1998}, volume = {17}, number = {2}, month = aug, year = {1998}, issn = {1061-7264}, pages = {1--31}, numpages = {31}, url = {http://doi.acm.org/10.1145/289918.289920}, doi = {10.1145/289918.289920}, acmid = {289920}, publisher = {ACM}, address = {New York, NY, USA}, } % OOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOO @article{olender-osterweil:1992:cesar, author = {Kurt M. Olender and Leon J. Osterweil}, title = {Interprocedural Static Analysis of Sequencing Constraints}, journal = {ACM Trans. Softw. Eng. Methodol.}, volume = {1}, number = {1}, year = {1992}, pages = {21-52}, ee = {http://doi.acm.org/10.1145/125489.122822}, bibsource = {DBLP, http://dblp.uni-trier.de} } @misc{openacc:2011:standard1.0, author={OpenACC-Standard.org}, year={2011}, title={The {OpenACC\textsuperscript{\texttrademark}} {A}pplication {P}rogramming {I}nterface: Version 1.0}, month=nov, howpublished={\url{http://www.openacc.org/sites/default/files/OpenACC.1.0_0.pdf}} } @misc{OpenMC, key = {OpenMC}, title={The {OpenMC} {Monte} {Carlo} Code}, howpublished = {\url{http://mit-crpg.github.com/openmc/}} } @misc{openmp:2011:standard31, author={{OpenMP Architecture Review Board}}, year = 2011, month = jul, title = {{OpenMP} Application Program Interface, Version 3.1}, howpublished = {\url{http://www.openmp.org/mp-documents/OpenMP3.1.pdf}} } @misc{openmp-standard, author={{OpenMP Architecture Review Board}}, title = {{OpenMP} {API} {S}pecification for {P}arallel {P}rogramming}, howpublished = {\url{http://openmp.org/wp/}}, note = {accessed Feb.\ 8, 2014} } @misc{opencl-standard, author = {{Khronos Group}}, title = {{OpenCL}: The open standard for parallel programming of heterogeneous systems}, howpublished = {\url{https://www.khronos.org/opencl/}} } % PPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPPP @InProceedings{fmics07, author = "Robert Palmer and Michael Delisi and Ganesh Gopalakrishnan and Robert M. Kirby", title = "An Approach to Formalization and Analysis of Message Passing Libraries", booktitle = "Formal Methods for Industry Critical Systems (FMICS 2007)", note = "LNCS 4916, EASST Best Paper Award", editor = "S. Leue and P. Merino", pages = "164--181", year = "2008", } @InProceedings{palmer-padtad, author = "Robert Palmer and Ganesh Gopalakrishnan and Robert M. Kirby", title = "Semantics Driven Dynamic Partial-order Reduction of {MPI}-based Parallel Programs", booktitle = "Parallel and Distributed Systems: Testing and Debugging (PADTAD - V)", year = "2007", pages = "43--53", note = "{\em Best Paper Award}", } @inproceedings{pankratius:2012:scala, author = {Pankratius, Victor and Schmidt, Felix and Garret\'{o}n, Gilda}, title = {Combining functional and imperative programming for multicore software: an empirical study evaluating {Scala} and {Java}}, booktitle = {Proceedings of the 2012 International Conference on Software Engineering}, series = {ICSE 2012}, year = {2012}, isbn = {978-1-4673-1067-3}, location = {Zurich, Switzerland}, pages = {123--133}, numpages = {11}, url = {http://dl.acm.org/citation.cfm?id=2337223.2337238}, acmid = {2337238}, publisher = {IEEE Press}, address = {Piscataway, NJ, USA}, } @misc{parasail:2014:web, title = {{P}ara{S}ail {P}rogramming {L}anguage}, howpublished = {\url{http://www.parasail-lang.org}}, year = {accessed Feb.\ 7, 2014}, key = {ParaSail} } % this needs to be fixed... % number = 1, @inproceedings{uintah2:steve-parker, author = {Stephen G. Parker}, title = {A component-based architecture for parallelmulti-physics PDE simulation}, booktitle = {Future Generation Computing Systems}, year = 2006, volume = 22, pages = {204-216}} @incollection {pascual-hascoet:2012:dataflow, author = {Pascual, Val\'erie and Hasco\"et, Laurent}, affiliation = {INRIA, Sophia-Antipolis, France}, title = {Native Handling of Message-Passing Communication in Data-Flow Analysis}, booktitle = {Recent Advances in Algorithmic Differentiation}, series = {Lecture Notes in Computational Science and Engineering}, editor = {Forth, Shaun and Hovland, Paul and Phipps, Eric and Utke, Jean and Walther, Andrea and Barth, Timothy J. and Griebel, Michael and Keyes, David E. and Nieminen, Risto M. and Roose, Dirk and Schlick, Tamar}, publisher = {Springer Berlin Heidelberg}, isbn = {978-3-642-30023-3}, keyword = {Mathematics and Statistics}, pages = {83-92}, volume = {87}, year = {2012} } @inproceedings{pasareanu-rungta:2010:jpf-symb, author = {Corina S. Pasareanu and Neha Rungta}, title = {Symbolic {PathFinder}: symbolic execution of {Java} bytecode}, booktitle = {ASE}, year = {2010}, pages = {179-180}, ee = {http://doi.acm.org/10.1145/1858996.1859035}, crossref = {DBLP:conf/kbse/2010}, bibsource = {DBLP, http://dblp.uni-trier.de} } @Article{my-spe-paper-of-2010, author = "Salman Pervez and Ganesh Gopalakrishnan and Robert M. Kirby and Rajeev Thakur and William Gropp", title = "Formal methods applied to high performance computing software design: a case study of {MPI} one-sided communication based locking", journal = "Software: Practice and Experience", month = dec, year = "2009", volume = "40", pages = "23--43", } @InProceedings{pervez-europvm07, author = "Salman Pervez and Ganesh Gopalakrishnan and Robert M. Kirby and Robert Palmer and Rajeev Thakur and William Gropp", title = "Practical Model Checking Method for Verifying Correctness of {MPI} Programs", booktitle = "Proc. of the 14th European PVM/MPI Users' Group Meeting (Euro PVM/MPI 2007)", month = sep, year = "2007", pages = "344--353", } @InProceedings{onesided-europvm06, author = "Salman Pervez and Ganesh Gopalakrishnan and Robert {M.} Kirby and Rajeev Thakur and William Gropp", title = "Formal Verification of Programs that use {MPI} One-sided Communication", booktitle = "Recent Advances in Parallel Virtual Machine and Message Passing Interface (EuroPVM/{MPI}), LNCS 4192", note = "Outstanding Paper", pages = "30--39", year = "2006", } @article{peterson:1977:petri, author = {Peterson, James L.}, title = {Petri Nets}, journal = {ACM Comput. Surv.}, issue_date = {Sept. 1977}, volume = {9}, number = {3}, month = sep, year = {1977}, issn = {0360-0300}, pages = {223--252}, numpages = {30}, url = {http://doi.acm.org/10.1145/356698.356702}, doi = {10.1145/356698.356702}, acmid = {356702}, publisher = {ACM}, address = {New York, NY, USA}, } % QQQQQQQQQQQQQQQQQQQQQQQQQQQQQQQQQQQQQQQQQQQQQQQQQQQQQQQQQQQQQQQQQQQQQQ @misc{Q-verifier:2014:web, title = {{Q} {P}rogram {V}erifier --- {M}icrosoft {R}esearch}, howpublished={\url{http://research.microsoft.com/en-us/projects/verifierq/}}, year = {accessed February 4, 2014}, key = {Q Program Verifier} } @inproceedings{qadeer-rehof:2005:cb, author = {Shaz Qadeer and Jakob Rehof}, title = {Context-Bounded Model Checking of Concurrent Software}, year = {2005}, pages = {93-107}, crossref = {tacas2005}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{qadeer-wu:2004:kiss, author = {Shaz Qadeer and Dinghao Wu}, title = {KISS: keep it simple and sequential}, year = {2004}, pages = {14-24}, crossref = {pldi2004}, bibsource = {DBLP, http://dblp.uni-trier.de} } % RRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRR @inproceedings{rabinovitz-grumberg:2005:rg, author = {Ishai Rabinovitz and Orna Grumberg}, title = {Bounded Model Checking of Concurrent Programs}, year = {2005}, pages = {82-97}, crossref = {cav2005}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{rakamaric:2010:storm, author = {Zvonimir Rakamari\'c}, title = {{STORM}: Static Unit Checking of Concurrent Programs}, year = {2010}, pages = {519-520}, ee = {http://doi.acm.org/10.1145/1810295.1810460}, crossref = {icse2010-2}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{rakamaric-hu:2009:smack, author = {Zvonimir Rakamari\'c and Alan J. Hu}, title = {A Scalable Memory Model for Low-Level Code}, year = {2009}, pages = {290-304}, ee = {http://dx.doi.org/10.1007/978-3-540-93900-9_24}, crossref = {vmcai2009}, bibsource = {DBLP, http://dblp.uni-trier.de} } @article{ramalingam:2000:undecidable, author = {G. Ramalingam}, title = {Context-sensitive synchronization-sensitive analysis is undecidable}, journal = {ACM Trans. Program. Lang. Syst.}, volume = {22}, number = {2}, year = {2000}, pages = {416-430}, bibsource = {DBLP, http://dblp.uni-trier.de} } @article{ritchie-thompson:1974:unix, author = {Ritchie, Dennis M. and Thompson, Ken}, title = {The {UNIX} time-sharing system}, journal = {Commun. ACM}, issue_date = {July 1974}, volume = {17}, number = {7}, month = jul, year = {1974}, issn = {0001-0782}, pages = {365--375}, numpages = {11}, url = {http://doi.acm.org/10.1145/361011.361061}, doi = {10.1145/361011.361061}, acmid = {361061}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {PDP-11, command language, file system, operating system, time-sharing}, } @inproceedings{robby-dwyer-hatcliff:2003:bogor, author = {Robby and Matthew B. Dwyer and John Hatcliff}, title = {Bogor: an extensible and highly-modular software model checking framework}, year = {2003}, pages = {267-276}, booktitle = {Proceedings of the 11th ACM SIGSOFT Symposium on Foundations of Software Engineering 2003 held jointly with 9th European Software Engineering Conference, ESEC/FSE 2003, Helsinki, Finland, September 1-5, 2003}, } @article{romano-forget:2013:openmc, title = "The {OpenMC Monte Carlo} Particle Transport Code", author = "Paul K. Romano and Benoit Forget", journal = "Annals of Nuclear Energy", volume = "51", number = "0", pages = "274 - 281", year = "2013" } @misc{rose, Howpublished = {\url{http://www.rosecompiler.org/}}, Title = {{ROSE} compiler infrastructure}, key = {ROSE}, Year = 2012 } @article{rossi-resurrect, Author = {Louis F. Rossi}, Date-Added = {2008-07-13 16:56:18 -0400}, Date-Modified = {2008-07-13 16:56:18 -0400}, Journal = {SIAM J. Sci. Comp.}, Number = {2}, Pages = {370-397}, Title = {Resurrecting Core Spreading Methods: A New Scheme That is Both Deterministic and Convergent}, Volume = {17}, Year = {1996}} @article{rossi-biot-savart, Author = {Louis F. Rossi}, Date-Added = {2008-07-13 16:56:18 -0400}, Date-Modified = {2008-07-13 16:56:18 -0400}, Journal = {SIAM J. Sci. Comput.}, Number = {4}, Owner = {rossi}, Pages = {1509--1532}, Title = {Evaluation of the {B}iot-{S}avart integral for deformable elliptical Gaussian vortex elements}, Volume = {28}, Year = {2006}} @article{rossi-deform-1, Author = {Louis F. Rossi}, Date-Added = {2008-07-13 16:40:50 -0400}, Date-Modified = {2008-07-13 16:40:50 -0400}, Institution = {University of Delaware}, Journal = {SIAM J. Sci. Comput.}, Number = {3}, Pages = {885-906}, Title = {Achieving high-order convergence rates with deforming basis functions.}, Type = {Mathematical Sciences}, Volume = {26}, Year = {2005}} @Misc{romio, key = {ROMIO}, title = {{ROMIO}: {A} High-Performance, Portable {MPI-IO} Implementation}, howpublished = {\url{http://www.mcs.anl.gov/romio}} } % SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS @inproceedings{ppcp-sigcse-2012, author = {Caitlin Sadowski and Thomas Ball Judith Bishop and Sebastian Burckhardt and Ganesh Gopalakrishnan and Joseph Mayo and Madanlal Musuvathi and Shaz Qadeer and Stephen Toub}, title = {Practical Parallel and Concurrent Programming}, booktitle = {ACM SIGCSE}, month = may, year = 2011} @book{sanders-kandrot:2010:cuda-by-example, title={{CUDA} by Example: An Introduction to General-Purpose {GPU} Programming}, url={https://developer.nvidia.com/content/cuda-example-introduction-general-purpose-gpu-programming-0}, year = {2010}, publisher={Addison-Wesley}, author = {Jason Sanders and Edward Kandrot} } @misc{sarl:2014:web, title={{SARL}: The {S}ymbolic {A}lgebra and {R}easoning {L}ibrary}, howpublished = {\url{http://vsl.cis.udel.edu/sarl}}, key = {SARL}, year = {accessed Feb.\ 6, 2014} } @misc{sat-challenge:2012:web, title = {{SAT} {C}hallenge 2012 web site}, howpublished = {\url{http://baldur.iti.kit.edu/SAT-Challenge-2012/}}, key = {SAT Challenge 2012}, year = {2012} } @article{sewell-cacm-x86, author = {Peter Sewell and Susmit Sarkar and Scott Owens and Francesco Zappa Nardelli and Magnus O. Myreen}, title = {x86-TSO: a rigorous and usable programmer's model for x86 multiprocessors}, journal = {Commun. ACM}, volume = 53, number = 7, pages = {89-97}, year = 2010} @article{shasha-snir, author = {Dennis Shasha and Marc Snir}, title = {Efficient and Correct Execution of Parallel Programs that Share Memory}, pages = {282-312}, journal = {ACM TOPLAS}, volume= 10, number= 1, month = jan, year = 1988} @inproceedings{shah-shymasundar-varma:2009:cssa-barrier, author = {Harshit J. Shah and R. K. Shyamasundar and Pradeep Varma}, title = {Concurrent {SSA} for general barrier-synchronized parallel programs}, year = {2009}, pages = {1-12}, ee = {http://dx.doi.org/10.1109/IPDPS.2009.5161030}, crossref = {DBLP:conf/ipps/2009}, bibsource = {DBLP, http://dblp.uni-trier.de} } @misc{siegel:mpispinweb, Author = {Stephen F. Siegel}, Date-Added = {2008-07-13 16:56:18 -0400}, Date-Modified = {2008-07-13 16:56:18 -0400}, Howpublished = {\url{http://vsl.cis.udel.edu/mpi-spin}}, Title = {The {{\textsc{MPI-Spin}}} web page}, Year = {2008}} @inproceedings{siegel:2007:vmcai, Author = {Stephen F. Siegel}, Crossref = {vmcai2007}, Date-Added = {2012-01-31 15:18:59 -0500}, Date-Modified = {2012-01-31 15:18:59 -0500}, Pages = {44--58}, Title = {{Model Checking Nonblocking {MPI} Programs}} } @inproceedings{siegel-gopalakrishnan:2011:vmcai, author = {Stephen F. Siegel and Ganesh Gopalakrishnan}, title = {Formal Analysis of Message Passing}, pages = {2-18}, crossref = {vmcai2011}, note = {Invited Tutorial} } @inproceedings{siegel-rossi:2008:eccsvm_pvmmpi, Author = {Stephen F. Siegel and Louis F. Rossi}, Crossref = {pvmmpi2008}, Pages = {274--282}, Title = {{Analyzing {BlobFlow}: A Case Study Using Model Checking to Verify Parallel Scientific Software}} } @article{siegel-mironova-avrunin-clarke:2008:tosem, Author = {Stephen F. Siegel and Anastasia Mironova and George S. Avrunin and Lori A. Clarke}, Journal = {ACM Transactions on Software Engineering and Methodology}, Number = 2, Pages = {Article 10, 1--34}, Title = {Combining Symbolic Execution with Model Checking to Verify Parallel Numerical Programs}, Volume = 17, Year = 2008 } @article{siegel-siegel:2010:madre_ijhpca, Author = {Stephen F. Siegel and Andrew R. Siegel}, Date-Added = {2009-07-19 16:30:46 -0500}, Date-Modified = {2010-06-28 14:24:35 -0400}, Journal = {International Journal of High Performance Computing Applications}, Month = feb, Number = {1}, Pages = {{93--104}}, Title = {{MADRE}: The {M}emory-{A}ware {D}ata {R}edistribution {E}ngine}, Volume = {24}, Year = {2010}} @inproceedings{siegel-zirkel:2012:loops, Author = {Stephen F. Siegel and Timothy K. Zirkel}, Crossref = {vmcai2012}, Pages = {412--427}, Title = {Loop Invariant Symbolic Execution for Parallel Programs}} @inproceedings{siegel-zirkel:2011:ppopp, Author = {Stephen F. Siegel and Timothy K. Zirkel}, Crossref = {ppopp2011}, Pages = {309--310}, Title = {Automatic Formal Verification of {MPI}-Based Parallel Programs}} @article{siegel-zirkel:2011:tass-mcs, Author = {Stephen F. Siegel and Timothy K. Zirkel}, Date-Added = {2012-01-31 15:18:59 -0500}, Date-Modified = {2012-01-31 15:18:59 -0500}, Journal = {Mathematics in Computer Science}, Number = {4}, Pages = {395--426}, Publisher = {Birkh\"auser Basel}, Title = {{TASS}: The {T}oolkit for {A}ccurate {S}cientific {S}oftware}, Volume = {5}, Year = {2011} } @article{siegel-zirkel:2011:fevs-mcs, Author = {Stephen F. Siegel and Timothy K. Zirkel}, Journal = {Mathematics in Computer Science}, Number = {4}, Pages = {427--435}, Publisher = {Birkh\"auser Basel}, Title = {{FEVS}: A {F}unctional {E}quivalence {V}erification {S}uite for High Performance Scientific Computing}, Volume = {5}, Year = {2011}} @InProceedings{zirkel-etal:2013:chapel, title = {Automated Verification of {C}hapel Programs Using Model Checking and Symbolic Execution}, author={Zirkel, Timothy K. and Siegel, Stephen F. and McClory, Timothy}, crossref = {nfm2013}, doi={10.1007/978-3-642-38088-4_14}, url={http://dx.doi.org/10.1007/978-3-642-38088-4_14}, pages={198--212} } @misc{fevs:2011:web, Author = {Stephen F. Siegel and Timothy K. Zirkel}, Howpublished = {\url{http://vsl.cis.udel.edu/fevs}}, Title = {A {F}unctional {E}quivalence {V}erification {S}uite}, Urldate = {2011}} @inproceedings{siegel-zirkel:2011:assert, Author = {Stephen F. Siegel and Timothy K. Zirkel}, Title = {Collective Assertions}, crossref = {vmcai2011}, Pages = {387-402} } @inproceedings{flanagan-predictive-race, author = {Yannis Smaragdakis and Jacob Evans and Caitlin Sadowski and Jaeheon Yi and Cormac Flanagan}, title = { Sound predictive race detection in polynomial time}, booktitle = { POPL}, year = 2012, pages = {387-400}} @misc{smt-comp:2012:web, title = {{SMT-COMP} 2012 web site}, howpublished = {\url{http://smtcomp.sourceforge.net/2012/}}, year = 2012, key = {SMT-COMP 2012} } @book{stallman-etal:2010:gcc, author={Richard M. Stallman and {the GCC Developer Community}}, title={Using the {GNU} {C}ompiler {C}ollection: For {GCC} version 4.7.2}, publisher={GNU Press, a division of the Free Software Foundation}, url={http://gcc.gnu.org/onlinedocs/gcc}, year={2010}, note={\url{http://gcc.gnu.org/onlinedocs/gcc}} } @article{strom-yemini:1986:typestate, author = {Robert E. Strom and Shaula Yemini}, title = {Typestate: A Programming Language Concept for Enhancing Software Reliability}, journal = {IEEE Trans. Software Eng.}, volume = {12}, number = {1}, year = {1986}, pages = {157-171}, ee = {http://doi.ieeecomputersociety.org/10.1109/TSE.1986.6312929}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{strout-kreaseck-hovland:2006:dataflow, author = {Strout, Michelle Mills and Kreaseck, Barbara and Hovland, Paul D.}, title = {Data-Flow Analysis for {MPI} Programs}, 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}, 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{techcon09-svs, author = "Subodh Sharma and Ganesh Gopalakrishnan", title = "Formal Verification of {MCAPI} Applications Using the Dynamic Verification tool {MCC}", month = sep, year = "2009", booktitle = "SRC Techcon, Austin, TX", note = "{\em Chosen as the Best Verification Session Paper.}", } @inproceedings{svs-smbf-brazil-2012, author = { Subodh Sharma and Ganesh Gopalakrishnan and Greg Bronevetsky}, title ={A Sound Reduction of Persistent-sets for Deadlock Detection in {MPI} Applications}, booktitle = {SMBF 2012 - The Brazilian Symposium on Formal Methods}, month = sep, year = 2012 } @InProceedings{svs:hldvt09, author = "Subodh Sharma and Ganesh Gopalakrishnan and Eric Mercer", title = "Dynamic Verification of Multicore Communication Applications in {MCAPI}", month = nov, publisher = "IEEE", year = "2009", booktitle = "International High-Level Design, Validation and Test Workshop (HLDVT)", } @InProceedings{svs:fmcad09, author = "Subodh Sharma and Ganesh Gopalakrishnan and Eric Mercer and Jim Holt", title = "{MCC} - {A} runtime verification tool for {MCAPI} user applications", booktitle = "9th International Conference Formal Methods in Computer Aided Design (FMCAD)", publisher = "IEEE", month = nov, pages = "41--44", year = "2009", } @InProceedings{europvm08-barrier, author = "Subodh Sharma and Sarvani Vakkalanka and Ganesh Gopalakrishnan and Robert M. Kirby and Rajeev Thakur and William Gropp", title = "A Formal Approach to Detect Functionally Irrelevant Barriers in {MPI} Programs", pages = "", crossref = "pvmmpi2008", } @inproceedings{suwimonteerabuth-etal:2008:cbjava, author = {Dejvuth Suwimonteerabuth and Javier Esparza and Stefan Schwoon}, title = {Symbolic Context-Bounded Analysis of Multithreaded {Java} Programs}, year = {2008}, pages = {270-287}, crossref = {spin2008}, bibsource = {DBLP, http://dblp.uni-trier.de} } % TTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTT @misc{tass-web, title = "TASS: The Toolkit for Accurate Scientific Software", howpublished = {\url{http://vsl.cis.udel.edu/tass}}, key = {TASS}, year = {2012} } @inproceedings{tofte-talpin:1994:regions, author = {Mads Tofte and Jean-Pierre Talpin}, title = {Implementation of the Typed Call-by-Value lambda-Calculus using a Stack of Regions}, year = {1994}, pages = {188-201}, ee = {http://doi.acm.org/10.1145/174675.177855}, crossref = {DBLP:conf/popl/1994}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{torre-etal:2009:cbred, author = {Salvatore La Torre and P. Madhusudan and Gennaro Parlato}, title = {Reducing Context-Bounded Concurrent Reachability to Sequential Reachability}, year = {2009}, pages = {477-492}, crossref = {cav2009}, bibsource = {DBLP, http://dblp.uni-trier.de} } @article{touili-atig:2010:tcs, author = {Touili, Tayssir and Atig, Mohamed Faouzi}, title = {Verifying parallel programs with dynamic communication structures}, journal = {Theor. Comput. Sci.}, issue_date = {August, 2010}, volume = {411}, number = {38--39}, month = aug, year = {2010}, issn = {0304-3975}, pages = {3460--3468}, numpages = {9}, url = {http://dx.doi.org/10.1016/j.tcs.2010.05.028}, doi = {10.1016/j.tcs.2010.05.028}, acmid = {1842410}, publisher = {Elsevier Science Publishers Ltd.}, address = {Essex, UK}, keywords = {Concurrent programs, Model checking, Pushdown Networks, Reachability analysis, Recognizable sets}, } @inproceedings{tu-padua:1995:gatedssa-parallelcompiler, author = {Peng Tu and David A. Padua}, title = {Gated {SSA}-based Demand-Driven Symbolic Analysis for Parallelizing Compilers}, booktitle = {International Conference on Supercomputing}, year = {1995}, pages = {414-423}, ee = {http://doi.acm.org/10.1145/224538.224648}, bibsource = {DBLP, http://dblp.uni-trier.de} } % UUUUUUUUUUUUUUUUUUUUUUUUUUUUUUUUUUUUUUUUUUUUUUUUUUUUUUUUUUUUUUUUUUUUUU @techreport{upc:2005:spec, author = {{UPC} {C}onsortium}, title = {{UPC} {L}anguage {S}pecifications, v1.2}, institution = {Lawrence Berkeley National Lab}, number = {Tech Report LBNL-59208}, year = 2005 } % VVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVV @InProceedings{sarvani-padtad08, author = "Sarvani Vakkalanka and Michael DeLisi and Ganesh Gopalakrishnan and Robert M. Kirby", title = "Scheduling Considerations for Building Dynamic Verification Tools for {MPI}", booktitle = "Parallel and Distributed Systems - Testing and Debugging {(PADTAD-VI)}", month = jul, address = "Seattle, WA", year = "2008", } @inproceedings{fm2009, author = {Sarvani Vakkalanka and Anh Vo and Ganesh Gopalakrishnan and Robert M. Kirby}, title = {Reduced Execution Semantics of {MPI}: From theory to practice}, booktitle = {FM 2009}, month = nov, year = 2009, pages = {724-740}} @inproceedings{cav08-isp, author = {Vakkalanka, Sarvani and Gopalakrishnan, Ganesh and Kirby, Robert M.}, title = {Dynamic Verification of {MPI} Programs with Reductions in Presence of Split Operations and Relaxed Orderings}, year = {2008}, pages = {66--79}, crossref = {cav2008} } @inproceedings{europvm08-isp, author = {Sarvani Vakkalanka and Michael DeLisi and Ganesh Gopalakrishnan and Robert M. Kirby and Rajeev Thakur and William Gropp}, title = {Implementing Efficient Dynamic Formal Verification Methods for {MPI} Programs}, booktitle = {{EuroPVM/MPI}}, year = 2008} @inproceedings{cav2008:isp, author = {Sarvani Vakkalanka and Ganesh Gopalakrishnan and Robert M. Kirby}, title = {Dynamic verification of {MPI} programs with reductions in presence of split operations and relaxed orderings}, crossref = {cav2008} } @inproceedings{visser-etal:2012:green, author = {Willem Visser and Jaco Geldenhuys and Matthew B. Dwyer}, title = {Green: reducing, reusing and recycling constraints in program analysis}, pages = {58}, ee = {http://doi.acm.org/10.1145/2393596.2393665}, crossref = {fse2012}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{DAM-sc10, author = {Anh Vo and Sriram Aananthakrishnan and Ganesh Gopalakrishnan and Bronis R. {de Supinski} and Martin Schulz and Greg Bronevetsky}, title = {A Scalable and Distributed Dynamic Formal Verifier for {MPI} Programs}, booktitle = {{The International Conference for High Performance Computing, Networking, Storage and Analysis (SC10)}}, publisher = {ACM}, key = {SC10}, year = 2010, url = {http://www.cs.utah.edu/fv/DAMPI/sc10.pdf} } @inproceedings{pact11-avo, author = {Vo, A. and Gopalakrishnan, G. and Kirby, R.~M. and de~Supinski, B.~R. and Schulz, M. and Bronevetsky, G.}, title = {Large Scale Verification of {MPI} Programs Using {L}amport Clocks with Lazy Update}, booktitle = {{PACT}}, year = 2011} @InProceedings{europvm09-iprobe, author = "Anh Vo and Sarvani Vakkalanka and Jason Williams and Ganesh Gopalakrishnan and Robert M. Kirby and Rajeev Thakur", title = "Sound and Efficient Dynamic Verification of {MPI} Programs with Probe Non-Determinism", booktitle = "EuroPVM/MPI", month = sep, year = "2009", pages = "271-281" } @inproceedings{ppopp09-isp, author = {Vo, Anh and Vakkalanka, Sarvani and DeLisi, Michael and Gopalakrishnan, Ganesh and Kirby, Robert M. and Thakur, Rajeev}, title = {Formal verification of practical {MPI} programs}, booktitle = {Proceedings of the 14th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming}, series = {PPoPP '09}, year = {2009}, isbn = {978-1-60558-397-6}, location = {Raleigh, NC, USA}, pages = {261--270}, numpages = {10}, url = {http://doi.acm.org/10.1145/1504176.1504214}, doi = {http://doi.acm.org/10.1145/1504176.1504214}, acmid = {1504214}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {distributed programming, dynamic partial order reduction, message passing interface, model checking, mpi}, } % WWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWW @book{wijngaarden:1969:algol, author = {Wijngaarden, A. van}, title = {Report on the algorithmic language ALGOL 68}, year = {1969}, isbn = {B0007IUUXM}, publisher = {Printing by the Mathematisch Centrum}, } @article{wilson-etal:1994:suif, author = {Robert P. Wilson and Robert S. French and Christopher S. Wilson and Saman P. Amarasinghe and Jennifer-Ann M. Anderson and Steven W. K. Tjiang and Shih-Wei Liao and Chau-Wen Tseng and Mary W. Hall and Monica S. Lam and John L. Hennessy}, title = {{SUIF}: An Infrastructure for Research on Parallelizing and Optimizing Compilers}, journal = {SIGPLAN Notices}, volume = {29}, number = {12}, year = {1994}, pages = {31-37}, ee = {http://doi.acm.org/10.1145/193209.193217}, bibsource = {DBLP, http://dblp.uni-trier.de} } @article{wrinn:2012:outreach, author = {Wrinn, Michael}, title = {Parallel computing: thoughts following a four-year tour of academic outreach}, journal = {ACM Inroads}, issue_date = {September 2012}, volume = {3}, number = {3}, month = sep, year = {2012}, issn = {2153-2184}, pages = {4--8}, numpages = {5}, url = {http://doi.acm.org/10.1145/2339055.2339057}, doi = {10.1145/2339055.2339057}, acmid = {2339057}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {CS principles, computational thinking, computer science education}, } % XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX @inproceedings{xie-aiken:2005:saturn, author = {Yichen Xie and Alexander Aiken}, title = {Scalable error detection using boolean satisfiability}, year = {2005}, pages = {351-363}, ee = {http://doi.acm.org/10.1145/1040305.1040334}, crossref = {DBLP:conf/popl/2005}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{xu-kremenek-zhang:2010:memoryC, author = {Zhongxing Xu and Ted Kremenek and Jian Zhang}, title = {A Memory Model for Static Analysis of C Programs}, year = {2010}, pages = {535-548}, ee = {http://dx.doi.org/10.1007/978-3-642-16558-0_44}, crossref = {DBLP:conf/isola/2010-1}, bibsource = {DBLP, http://dblp.uni-trier.de} } @misc{xum-webpage, key = "xum-webpage", title = {Download Site for our {XUM} multicore design}, note = {\url{http://www.cs.utah.edu/fv/XUM}}} % YYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYY @inproceedings{yuyang-spin09, author = {Yang, Yu and Chen, Xiaofang and Gopalakrishnan, Ganesh and Wang, Chao}, title = {Automatic Discovery of Transition Symmetry in Multithreaded Programs Using Dynamic Analysis}, booktitle = {Proceedings of the 16th International SPIN Workshop on Model Checking Software}, year = {2009}, isbn = {978-3-642-02651-5}, location = {Grenoble, France}, pages = {279--295}, numpages = {17}, url = {http://dx.doi.org/10.1007/978-3-642-02652-2_22}, doi = {http://dx.doi.org/10.1007/978-3-642-02652-2_22}, acmid = {1575294}, publisher = {Springer-Verlag}, address = {Berlin, Heidelberg}, } @inproceedings{java-grande, author = {Yue Yang and Ganesh Gopalakrishnan and Gary Lindstrom}, title = {Specifying {Java} Thread Semantics using a Uniform Memory Model}, booktitle = {Joint ACM Java Grande - ISCOPE Conference}, pages = {192 - 201}, note = {ISBN:1-58113-599-8}, year = 2002} @inproceedings{ipdps04-nemos, author = {Yue Yang and Ganesh Gopalakrishnan and Gary Lindstrom and Konrad Slind}, title = {Nemos: A Framework for Axiomatic and Executable Specifications of Memory Consistency Models}, booktitle = {International Parallel and Distributed Processing Symposium}, year = 2004} @article{yelick-etal:1998:titanium, author = {Katherine A. Yelick and Luigi Semenzato and Geoff Pike and Carleton Miyamoto and Ben Liblit and Arvind Krishnamurthy and Paul N. Hilfinger and Susan L. Graham and David Gay and Phillip Colella and Alexander Aiken}, title = {Titanium: A High-performance {Java} Dialect}, journal = {Concurrency - Practice and Experience}, volume = {10}, number = {11-13}, year = {1998}, pages = {825--836}, ee = {http://onlinelibrary.wiley.com/doi/10.1002/(SICI)1096-9128(199809/11)10:11/13$<$825::AID-CPE383$>$3.0.CO;2-H/abstract}, bibsource = {DBLP, http://dblp.uni-trier.de} } % ZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZ @inproceedings{zhang-dusterwald:2007:barriers, author = {Yuan Zhang and Evelyn Duesterwald}, title = {Barrier matching for programs with textually unaligned barriers}, crossref={ppopp2007}, pages = {194--204}, } %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% CROSSREFS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Keep conference entries organized by conference. Within % each conference section, organize chronologically. % Use keys of the form "cav2009", "vmcai2012", etc. %%%% ASE @proceedings{DBLP:conf/kbse/2010, editor = {Charles Pecheur and Jamie Andrews and Elisabetta Di Nitto}, title = {ASE 2010, 25th IEEE/ACM International Conference on Automated Software Engineering, Antwerp, Belgium, September 20-24, 2010}, booktitle = {ASE 2010, 25th IEEE/ACM International Conference on Automated Software Engineering, Antwerp, Belgium, September 20-24, 2010}, publisher = {ACM}, year = {2010}, isbn = {978-1-4503-0116-9}, bibsource = {DBLP, http://dblp.uni-trier.de} } %%%% Boogie workshop % ? %%%% CAV @proceedings{cav2005, editor = {Kousha Etessami and Sriram K. Rajamani}, title = {Computer Aided Verification, 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005, Proceedings}, booktitle = {Computer Aided Verification, 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005, Proceedings}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {3576}, year = {2005}, isbn = {3-540-27231-3}, bibsource = {DBLP, http://dblp.uni-trier.de} } @proceedings{DBLP:conf/cav/2007, editor = {Werner Damm and Holger Hermanns}, title = {Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings}, booktitle = {Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {4590}, year = {2007}, isbn = {978-3-540-73367-6}, bibsource = {DBLP, http://dblp.uni-trier.de} } @proceedings{cav2007, Bibsource = {DBLP, http://dblp.uni-trier.de}, Booktitle = {Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings}, Date-Added = {2012-12-17 01:03:12 +0000}, Date-Modified = {2012-12-17 01:03:21 +0000}, Editor = {Werner Damm and Holger Hermanns}, Isbn = {978-3-540-73367-6}, Publisher = {Springer}, Series = {Lecture Notes in Computer Science}, Title = {Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3--7, 2007, Proceedings}, Volume = {4590}, Year = {2007}} @proceedings{cav2008, editor = {Aarti Gupta and Sharad Malik}, title = {Computer Aided Verification, 20th International Conference, CAV 2008, Princeton, NJ, USA, July 7-14, 2008, Proceedings}, booktitle = {Computer Aided Verification, 20th International Conference, CAV 2008, Princeton, NJ, USA, July 7-14, 2008, Proceedings}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {5123}, year = {2008}, isbn = {978-3-540-70543-7}, bibsource = {DBLP, http://dblp.uni-trier.de} } @proceedings{cav2009, Booktitle = {Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009, Proceedings}, Editor = {Ahmed Bouajjani and Oded Maler}, Isbn = {978-3-642-02657-7}, Publisher = {Springer}, Series = {Lecture Notes in Computer Science}, Title = {Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009, Proceedings}, Volume = {5643}, Year = {2009}} @proceedings{cav2011, editor = {Ganesh Gopalakrishnan and Shaz Qadeer}, title = {Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings}, booktitle = {Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {6806}, year = {2011}, isbn = {978-3-642-22109-5}, ee = {http://dx.doi.org/10.1007/978-3-642-22110-1}, bibsource = {DBLP, http://dblp.uni-trier.de} } @proceedings{cav2012, editor = {P. Madhusudan and Sanjit A. Seshia}, title = {Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings}, booktitle = {Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {7358}, year = {2012}, isbn = {978-3-642-31423-0}, ee = {http://dx.doi.org/10.1007/978-3-642-31424-7}, bibsource = {DBLP, http://dblp.uni-trier.de} } @proceedings{cav2013, editor = {Natasha Sharygina and Helmut Veith}, title = {Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13--19, 2013. Proceedings}, booktitle = {Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13--19, 2013. Proceedings}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {8044}, year = {2013}, isbn = {978-3-642-39798-1}, ee = {http://dx.doi.org/10.1007/978-3-642-39799-8}, bibsource = {DBLP, http://dblp.uni-trier.de} } %%%% CC @proceedings{DBLP:conf/cc/2011, editor = {Jens Knoop}, title = {Compiler Construction - 20th International Conference, CC 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbr{\"u}cken, Germany, March 26-April 3, 2011. Proceedings}, booktitle = {Compiler Construction - 20th International Conference, CC 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbr{\"u}cken, Germany, March 26-April 3, 2011. Proceedings}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {6601}, year = {2011}, isbn = {978-3-642-19860-1}, ee = {http://dx.doi.org/10.1007/978-3-642-19861-8}, bibsource = {DBLP, http://dblp.uni-trier.de} } %%%% ESOP: European Conference on Programming Languages and Systems @proceedings{esop2013, booktitle = {Proceedings of the 22nd European Conference on Programming Languages and Systems}, editor = {Felleisen, Matthias and Gardner, Philippa}, series = {ESOP'13}, year = {2013}, isbn = {978-3-642-37035-9}, issn = {0302-9743}, location = {Rome, Italy}, publisher = {Springer-Verlag}, address = {Berlin, Heidelberg} } %%%% PVMMPI: EuroPVM/MPI and EuroMPI @proceedings{pvmmpi2006, Booktitle = {{Recent Advances in Parallel Virtual Machine and Message Passing Interface, 13th European PVM/MPI User's Group Meeting, Bonn, Germany, September 17-20, 2006, Proceedings}}, Editor = {Bernd Mohr and Jesper Larsson Tr{\"a}ff and Joachim Worringen and Jack Dongarra}, Publisher = {Springer}, Series = {Lecture Notes in Computer Science}, Title = {{Recent Advances in Parallel Virtual Machine and Message Passing Interface, 13th European PVM/MPI User's Group Meeting, Bonn, Germany, September 17-20, 2006, Proceedings}}, Volume = {4192}, Year = {2006} } @proceedings{pvmmpi2008, Booktitle = {Recent Advances in {P}arallel {V}irtual {M}achine and {M}essage {P}assing {I}nterface, 15th {E}uropean {PVM/MPI} User's Group Meeting, Proceedings}, Editor = {Alexey Lastovetsky and Tahar Kechadi and Jack Dongarra}, Publisher = {Springer}, Series = {LNCS}, Title = {Recent Advances in {P}arallel {V}irtual {M}achine and {M}essage {P}assing {I}nterface, 15th {E}uropean {PVM/MPI} User's Group Meeting, Proceedings}, Volume = {5205}, Year = {2008} } %%%% FMCO @proceedings{fmco2005, editor = {Frank S. de Boer and Marcello M. Bonsangue and Susanne Graf and Willem P. de Roever}, title = {Formal Methods for Components and Objects, 4th International Symposium, FMCO 2005, Amsterdam, The Netherlands, November 1-4, 2005, Revised Lectures}, booktitle = {Formal Methods for Components and Objects, 4th International Symposium, FMCO 2005, Amsterdam, The Netherlands, November 1-4, 2005, Revised Lectures}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {4111}, year = {2006}, isbn = {3-540-36749-7}, bibsource = {DBLP, http://dblp.uni-trier.de} } %%%% FSE @proceedings{fse2012, editor = {Will Tracz and Martin P. Robillard and Tevfik Bultan}, title = {20th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE-20), SIGSOFT/FSE'12, Cary, NC, USA - November 11 - 16, 2012}, booktitle = {20th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE-20), SIGSOFT/FSE'12, Cary, NC, USA - November 11 - 16, 2012}, publisher = {ACM}, year = {2012}, isbn = {978-1-4503-1614-9, 978-1-4503-0443-6}, ee = {http://dl.acm.org/citation.cfm?id=2393596}, bibsource = {DBLP, http://dblp.uni-trier.de} } %%%% GPGPU @proceedings{2010gpgpu, editor = {David R. Kaeli and Miriam Leeser}, title = {Proceedings of 3rd Workshop on General Purpose Processing on Graphics Processing Units, GPGPU 2010, Pittsburgh, Pennsylvania, USA, March 14, 2010}, booktitle = {Proceedings of 3rd Workshop on General Purpose Processing on Graphics Processing Units, GPGPU 2010, Pittsburgh, Pennsylvania, USA, March 14, 2010}, publisher = {ACM}, series = {ACM International Conference Proceeding Series}, volume = {425}, year = {2010}, isbn = {978-1-60558-935-0}, bibsource = {DBLP, http://dblp.uni-trier.de} } %%%% HVC @proceedings{hvc2007, editor = {Karen Yorav}, title = {Hardware and Software: Verification and Testing, Third International Haifa Verification Conference, HVC 2007, Haifa, Israel, October 23-25, 2007, Proceedings}, booktitle = {Haifa Verification Conference}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {4899}, year = {2008}, isbn = {978-3-540-77964-3}, bibsource = {DBLP, http://dblp.uni-trier.de} } %%%% ICPP @proceedings{DBLP:conf/icpp/1998, title = {1998 International Conference on Parallel Processing (ICPP '98), 10-14 August 1998, Minneapolis, Minnesota, USA, Proceedings}, booktitle = {1998 International Conference on Parallel Processing (ICPP '98), 10-14 August 1998, Minneapolis, Minnesota, USA, Proceedings}, publisher = {IEEE Computer Society}, year = {1998}, isbn = {0-8186-8650-2}, bibsource = {DBLP, http://dblp.uni-trier.de} } %%%% ICSE @proceedings{icse2008, editor = {Wilhelm Sch{\"a}fer and Matthew B. Dwyer and Volker Gruhn}, title = {30th International Conference on Software Engineering (ICSE 2008), Leipzig, Germany, May 10-18, 2008}, booktitle = {30th International Conference on Software Engineering (ICSE 2008), Leipzig, Germany, May 10-18, 2008}, publisher = {ACM}, year = {2008}, isbn = {978-1-60558-079-1}, bibsource = {DBLP, http://dblp.uni-trier.de} } @proceedings{icse2010-2, editor = {Jeff Kramer and Judith Bishop and Premkumar T. Devanbu and Sebasti{\'a}n Uchitel}, title = {Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering - Volume 2, ICSE 2010, Cape Town, South Africa, 1-8 May 2010}, booktitle = {Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering - Volume 2, ICSE 2010, Cape Town, South Africa, 1-8 May 2010}, publisher = {ACM}, year = {2010}, isbn = {978-1-60558-719-6}, bibsource = {DBLP, http://dblp.uni-trier.de} } %%%% IPDPS @proceedings{DBLP:conf/ipps/2009, title = {23rd IEEE International Symposium on Parallel and Distributed Processing, IPDPS 2009, Rome, Italy, May 23-29, 2009}, booktitle = {23rd IEEE International Symposium on Parallel and Distributed Processing, IPDPS 2009, Rome, Italy, May 23-29, 2009}, publisher = {IEEE}, year = {2009}, bibsource = {DBLP, http://dblp.uni-trier.de} } %%%% ISCA @proceedings{DBLP:conf/isca/1990, editor = {Jean-Loup Baer and Larry Snyder and James R. Goodman}, title = {Proceedings of the 17th Annual International Symposium on Computer Architecture (ISCA). Seattle, WA, June 1990}, booktitle = {Proceedings of the 17th Annual International Symposium on Computer Architecture (ISCA). Seattle, WA, June 1990}, publisher = {ACM}, year = {1990}, isbn = {0-89791-366-3}, ee = {http://dl.acm.org/citation.cfm?id=325164}, bibsource = {DBLP, http://dblp.uni-trier.de} } %%%% ISMM @proceedings{DBLP:conf/iwmm/2009, editor = {Hillel Kolodner and Guy L. Steele Jr.}, title = {Proceedings of the 8th International Symposium on Memory Management, ISMM 2009, Dublin, Ireland, June 19-20, 2009}, booktitle = {ISMM}, publisher = {ACM}, year = {2009}, isbn = {978-1-60558-347-1}, ee = {http://dl.acm.org/citation.cfm?id=1542431}, bibsource = {DBLP, http://dblp.uni-trier.de} } %%%% ISoLA @proceedings{DBLP:conf/isola/2010-1, editor = {Tiziana Margaria and Bernhard Steffen}, title = {Leveraging Applications of Formal Methods, Verification, and Validation - 4th International Symposium on Leveraging Applications, ISoLA 2010, Heraklion, Crete, Greece, October 18-21, 2010, Proceedings, Part I}, booktitle = {Leveraging Applications of Formal Methods, Verification, and Validation - 4th International Symposium on Leveraging Applications, ISoLA 2010, Heraklion, Crete, Greece, October 18-21, 2010, Proceedings, Part I}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {6415}, year = {2010}, isbn = {978-3-642-16557-3}, ee = {http://dx.doi.org/10.1007/978-3-642-16558-0}, bibsource = {DBLP, http://dblp.uni-trier.de} } %%%% NFM (Nasa Formal Methods) @proceedings{nfm2013, booktitle = {NASA Formal Methods: 5th International Symposium, NFM 2013, Moffett Field, CA, USA, May 14-16, 2013. Proceedings}, title = {NASA Formal Methods: 5th International Symposium, NFM 2013, Moffett Field, CA, USA, May 14-16, 2013. Proceedings}, year={2013}, isbn={978-3-642-38087-7}, volume={7871}, series={Lecture Notes in Computer Science}, editor={Brat, Guillaume and Rungta, Neha and Venet, Arnaud}, publisher={Springer Berlin Heidelberg} } %%%% OOPSLA @proceedings{DBLP:conf/oopsla/2007, editor = {Richard P. Gabriel and David F. Bacon and Cristina Videira Lopes and Guy L. Steele Jr.}, title = {Proceedings of the 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2007, October 21-25, 2007, Montreal, Quebec, Canada}, booktitle = {Proceedings of the 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2007, October 21-25, 2007, Montreal, Quebec, Canada}, publisher = {ACM}, year = {2007}, isbn = {978-1-59593-786-5}, bibsource = {DBLP, http://dblp.uni-trier.de} } @proceedings{DBLP:conf/oopsla/2008, editor = {Gail E. Harris}, title = {Proceedings of the 23rd Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2008, October 19-23, 2008, Nashville, TN, USA}, booktitle = {Proceedings of the 23rd Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2008, October 19-23, 2008, Nashville, TN, USA}, publisher = {ACM}, year = {2008}, isbn = {978-1-60558-215-3}, bibsource = {DBLP, http://dblp.uni-trier.de} } %%%% PASTE @proceedings{paste2005, editor = {Michael D. Ernst and Thomas P. Jensen}, title = {Proceedings of the 2005 ACM SIGPLAN-SIGSOFT Workshop on Program Analysis For Software Tools and Engineering, PASTE'05, Lisbon, Portugal, September 5-6, 2005}, booktitle = {Proceedings of the 2005 ACM SIGPLAN-SIGSOFT Workshop on Program Analysis For Software Tools and Engineering, PASTE'05, Lisbon, Portugal, September 5-6, 2005}, publisher = {ACM}, year = {2005}, isbn = {1-59593-239-9}, ee = {http://dl.acm.org/citation.cfm?id=1108792}, bibsource = {DBLP, http://dblp.uni-trier.de} } %%%% PLDI @proceedings{pldi2002, editor = {Jens Knoop and Laurie J. Hendren}, title = {Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Berlin, Germany, June 17-19, 2002}, booktitle = {Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Berlin, Germany, June 17-19, 2002}, publisher = {ACM}, year = {2002}, isbn = {1-58113-463-0}, ee = {http://dl.acm.org/citation.cfm?id=512529}, bibsource = {DBLP, http://dblp.uni-trier.de} } @proceedings{pldi2004, editor = {William Pugh and Craig Chambers}, title = {Proceedings of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation 2004, Washington, DC, USA, June 9-11, 2004}, booktitle = {Proceedings of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation 2004, Washington, DC, USA, June 9-11, 2004}, publisher = {ACM}, year = {2004}, isbn = {1-58113-807-5}, bibsource = {DBLP, http://dblp.uni-trier.de} } @proceedings{pldi2005, editor = {Vivek Sarkar and Mary W. Hall}, title = {Proceedings of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation, Chicago, IL, USA, June 12-15, 2005}, booktitle = {Proceedings of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation, Chicago, IL, USA, June 12-15, 2005}, publisher = {ACM}, year = {2005}, isbn = {1-59593-056-6}, bibsource = {DBLP, http://dblp.uni-trier.de} } @proceedings{pldi2007, editor = {Jeanne Ferrante and Kathryn S. McKinley}, title = {Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, San Diego, California, USA, June 10-13, 2007}, booktitle = {Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, San Diego, California, USA, June 10-13, 2007}, publisher = {ACM}, year = {2007}, isbn = {978-1-59593-633-2}, bibsource = {DBLP, http://dblp.uni-trier.de} } %%%% POPL @proceedings{DBLP:conf/popl/1989, title = {Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, USA, January 11-13, 1989}, booktitle = {Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, USA, January 11-13, 1989}, publisher = {ACM Press}, year = {1989}, isbn = {0-89791-294-2}, ee = {http://dl.acm.org/citation.cfm?id=75277}, bibsource = {DBLP, http://dblp.uni-trier.de} } @proceedings{DBLP:conf/popl/1994, editor = {Hans-Juergen Boehm and Bernard Lang and Daniel M. Yellin}, title = {Conference Record of POPL'94: 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, Oregon, USA, January 17-21, 1994}, booktitle = {Conference Record of POPL'94: 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, Oregon, USA, January 17-21, 1994}, publisher = {ACM Press}, year = {1994}, isbn = {0-89791-636-0}, ee = {http://dl.acm.org/citation.cfm?id=174675}, bibsource = {DBLP, http://dblp.uni-trier.de} } @proceedings{DBLP:conf/popl/2005, editor = {Jens Palsberg and Mart\'{\i}n Abadi}, title = {Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12-14, 2005}, booktitle = {Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12-14, 2005}, publisher = {ACM}, year = {2005}, isbn = {1-58113-830-X}, ee = {http://dl.acm.org/citation.cfm?id=1040305}, bibsource = {DBLP, http://dblp.uni-trier.de} } @proceedings{popl2009, editor = {Zhong Shao and Benjamin C. Pierce}, title = {Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009}, booktitle = {Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009}, publisher = {ACM}, year = {2009}, isbn = {978-1-60558-379-2}, ee = {http://dl.acm.org/citation.cfm?id=1480881}, bibsource = {DBLP, http://dblp.uni-trier.de} } @proceedings{popl2011, editor = {Thomas Ball and Mooly Sagiv}, title = {Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011}, booktitle = {Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011}, publisher = {ACM}, year = {2011}, isbn = {978-1-4503-0490-0}, ee = {http://dl.acm.org/citation.cfm?id=1926385}, bibsource = {DBLP, http://dblp.uni-trier.de} } %%%% PPoPP @proceedings{ppopp2007, editor = {Katherine A. Yelick and John M. Mellor-Crummey}, title = {Proceedings of the 12th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPOPP 2007, San Jose, California, USA, March 14-17, 2007}, booktitle = {Proceedings of the 12th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPOPP 2007, San Jose, California, USA, March 14-17, 2007}, publisher = {ACM}, year = {2007}, isbn = {978-1-59593-602-8}, ee = {http://dl.acm.org/citation.cfm?id=1229428}, bibsource = {DBLP, http://dblp.uni-trier.de} } @proceedings{ppopp2011, Booktitle = {Proceedings of the 16th ACM SIGPLAN Annual Symposium on Principles and Practices of Parallel Programming (PPoPP '11)}, Editor = {Calin Cascaval and Pen-Chung Yew}, Publisher = {ACM}, Title = {Proceedings of the 16th ACM SIGPLAN Annual Symposium on Principles and Practices of Parallel Programming (PPoPP '11)}, Year = {2011}} %%%% SAS @proceedings{sas2012, editor = {Antoine Min{\'e} and David Schmidt}, title = {Static Analysis - 19th International Symposium, SAS 2012, Deauville, France, September 11-13, 2012. Proceedings}, booktitle = {Static Analysis - 19th International Symposium, SAS 2012, Deauville, France, September 11-13, 2012. Proceedings}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {7460}, year = {2012}, isbn = {978-3-642-33124-4}, ee = {http://dx.doi.org/10.1007/978-3-642-33125-1}, bibsource = {DBLP, http://dblp.uni-trier.de} } %%%% SC (Supercomputing) %%%% Spin @proceedings{spin2008, editor = {Klaus Havelund and Rupak Majumdar and Jens Palsberg}, title = {Model Checking Software, 15th International SPIN Workshop, Los Angeles, CA, USA, August 10-12, 2008, Proceedings}, booktitle = {Model Checking Software, 15th International SPIN Workshop, Los Angeles, CA, USA, August 10-12, 2008, Proceedings}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {5156}, year = {2008}, isbn = {978-3-540-85113-4}, bibsource = {DBLP, http://dblp.uni-trier.de} } @proceedings{spin2010, editor = {Jaco van de Pol and Michael Weber}, title = {Model Checking Software - 17th International SPIN Workshop, Enschede, The Netherlands, September 27-29, 2010. Proceedings}, booktitle = {Model Checking Software - 17th International SPIN Workshop, Enschede, The Netherlands, September 27-29, 2010. Proceedings}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {6349}, year = {2010}, isbn = {978-3-642-16163-6}, ee = {http://dx.doi.org/10.1007/978-3-642-16164-3}, bibsource = {DBLP, http://dblp.uni-trier.de} } %%%% TACAS @proceedings{tacas2003, Bibsource = {DBLP, http://dblp.uni-trier.de}, Booktitle = {{Tools and Algorithms for the Construction and Analysis of Systems, 9th International Conference, TACAS 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings}}, Date-Added = {2012-01-31 21:39:58 -0500}, Date-Modified = {2012-01-31 21:40:02 -0500}, Editor = {Hubert Garavel and John Hatcliff}, Isbn = {3-540-00898-5}, Publisher = {Springer}, Series = {Lecture Notes in Computer Science}, Title = {{Tools and Algorithms for the Construction and Analysis of Systems, 9th International Conference, TACAS 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings}}, Volume = {2619}, Year = {2003}} @proceedings{tacas2005, editor = {Nicolas Halbwachs and Lenore D. Zuck}, title = {Tools and Algorithms for the Construction and Analysis of Systems, 11th International Conference, TACAS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings}, booktitle = {Tools and Algorithms for the Construction and Analysis of Systems, 11th International Conference, TACAS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {3440}, year = {2005}, isbn = {3-540-25333-5}, bibsource = {DBLP, http://dblp.uni-trier.de} } @proceedings{tacas2006, editor = {Holger Hermanns and Jens Palsberg}, title = {Tools and Algorithms for the Construction and Analysis of Systems, 12th International Conference, TACAS 2006 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 25 - April 2, 2006, Proceedings}, booktitle = {Tools and Algorithms for the Construction and Analysis of Systems, 12th International Conference, TACAS 2006 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 25 - April 2, 2006, Proceedings}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {3920}, year = {2006}, isbn = {3-540-33056-9}, bibsource = {DBLP, http://dblp.uni-trier.de} } @proceedings{tacas2007, editor = {Orna Grumberg and Michael Huth}, title = {Tools and Algorithms for the Construction and Analysis of Systems, 13th International Conference, TACAS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24 - April 1, 2007, Proceedings}, booktitle = {Tools and Algorithms for the Construction and Analysis of Systems, 13th International Conference, TACAS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24 - April 1, 2007, Proceedings}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {4424}, year = {2007}, isbn = {978-3-540-71208-4}, bibsource = {DBLP, http://dblp.uni-trier.de} } @proceedings{tacas2008, editor = {C. R. Ramakrishnan and Jakob Rehof}, title = {Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings}, booktitle = {Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {4963}, year = {2008}, isbn = {978-3-540-78799-0}, bibsource = {DBLP, http://dblp.uni-trier.de} } @proceedings{tacas2012, editor = {Cormac Flanagan and Barbara K{\"o}nig}, title = {Tools and Algorithms for the Construction and Analysis of Systems - 18th International Conference, TACAS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings}, booktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 18th International Conference, TACAS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {7214}, year = {2012}, isbn = {978-3-642-28755-8}, bibsource = {DBLP, http://dblp.uni-trier.de} } @proceedings{tacas2013, title = {Proceedings of the 19th {I}nternational {C}onference on {T}ools and {A}lgorithms for the {C}onstruction and {A}nalysis of {S}ystems}, booktitle = {Proceedings of the 19th {I}nternational {C}onference on {T}ools and {A}lgorithms for the {C}onstruction and {A}nalysis of {S}ystems}, series = {TACAS'13}, year = {2013}, isbn = {978-3-642-36741-0}, location = {Rome, Italy}, publisher = {Springer-Verlag}, address = {Berlin, Heidelberg}, editor={Piterman, Nir and Smolka, Scott A.} } %%%% VMCAI @proceedings{vmcai2006, editor = {E. Allen Emerson and Kedar S. Namjoshi}, title = {Verification, Model Checking, and Abstract Interpretation, 7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006, Proceedings}, booktitle = {Verification, Model Checking, and Abstract Interpretation, 7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006, Proceedings}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {3855}, year = {2006}, isbn = {3-540-31139-4}, bibsource = {DBLP, http://dblp.uni-trier.de} } @proceedings{vmcai2007, Booktitle = {{Verification, Model Checking, and Abstract Interpretation: 8th International Conference, {VMCAI} 2007, Nice, France, January 14--16, 2007, Proceedings}}, Date-Added = {2012-01-31 15:18:59 -0500}, Date-Modified = {2012-01-31 15:18:59 -0500}, Editor = {Byron Cook and Andreas Podelski}, Series = {LNCS}, Title = {{Verification, Model Checking, and Abstract Interpretation: 8th International Conference, {VMCAI} 2007, Nice, France, January 14--16, 2007, Proceedings}}, Volume = 4349, Year = 2007} @proceedings{vmcai2009, editor = {Neil D. Jones and Markus M{\"u}ller-Olm}, title = {Verification, Model Checking, and Abstract Interpretation, 10th International Conference, VMCAI 2009, Savannah, GA, USA, January 18-20, 2009. Proceedings}, booktitle = {Verification, Model Checking, and Abstract Interpretation, 10th International Conference, VMCAI 2009, Savannah, GA, USA, January 18-20, 2009. Proceedings}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {5403}, year = {2009}, isbn = {978-3-540-93899-6}, ee = {http://dx.doi.org/10.1007/978-3-540-93900-9}, bibsource = {DBLP, http://dblp.uni-trier.de} } @proceedings{vmcai2011, Editor = {Ranjit Jhala and David Schmidt}, Booktitle = {Verification, Model Checking, and Abstract Interpretation: 12th International Conference, {VMCAI} 2011, Austin, TX, January 23--25, 2011, Proceedings}, Title = {Verification, Model Checking, and Abstract Interpretation: 12th International Conference, {VMCAI} 2011, Austin, TX, January 23--25, 2011, Proceedings}, Publisher = {Springer}, Series = {LNCS}, Volume = {6538}, Year = 2011 } @proceedings{vmcai2012, Editor = {Kuncak, Viktor and Rybalchenko, Andrey}, Booktitle = {Verification, Model Checking, and Abstract Interpretation: 13th International Conference, {VMCAI} 2012, Philadelphia, PA, USA, January 22--24, 2012, Proceedings}, Title = {Verification, Model Checking, and Abstract Interpretation: 13th International Conference, {VMCAI} 2012, Philadelphia, PA, USA, January 22--24, 2012, Proceedings}, Publisher = {Springer}, Series = {LNCS}, Volume = {7148}, Year = 2012 } @InProceedings{balaji08:sdp-hybrid, author = "P. Balaji and S. Bhagvat and R. Thakur and D. K. Panda", booktitle = "Proceedings of the IEEE International Conference on High Performance Computing (HiPC)", title = "Sockets Direct Protocol for Hybrid Network Stacks: A Case Study with {iWARP} over {10G} {Ethernet}", address = "Bangalore, India", month = dec, year = "2008", } @Article{lai09:proone, author = "P. Lai and P. Balaji and R. Thakur and D. K. Panda", title = "{ProOnE: A General Purpose Protocol Onload Engine for Multi- and Many-Core Architectures}", journal = "Special edition of the Springer Journal of Computer Science on Research and Development (presented at the International Supercomputing Conference (ISC))", volume = "23", number = "3", pages = "133--142", year = "2009", }