source: CIVL/mods/dev.civl.com/doc/manual/civl.bib@ 1aaefd4

% 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",
}