thesis.bib

@inproceedings{Polikarpova2012,
 author = {Polikarpova, Nadia and Furia, Carlo A. and Pei, Yu and Wei, Yi and Meyer, Bertrand},
 title = {What good are strong specifications?},
 booktitle = {Proceedings of the 2013 International Conference on Software Engineering},
 series = {ICSE '13},
 year = {2013},
 isbn = {978-1-4673-3076-3},
 location = {San Francisco, CA, USA},
 pages = {262--271},
 numpages = {10},
 url = {http://dl.acm.org/citation.cfm?id=2486788.2486823},
 acmid = {2486823},
 publisher = {IEEE Press},
 address = {Piscataway, NJ, USA},
}


@MastersThesis{Rudd2010,
  author = 	 "Robert Andrew Rudd",
  title = 	 "An Improved Scalable Mixed-Level Approach to Dynamic Analysis of C and C++ Programs",
  school = 	 MITEECS,
  year = 	 "2010",
  OPTkey = 	 "",
  OPTtype = 	 "",
  address = 	 MITaddr,
  month = 	 jan,
  OPTnote = 	 "",
  OPTannote = 	 "",
  abstract =
   "In this thesis, I address the challenges of developing tools which use a
    mixed-level approach to dynamic binary analysis. The mixed-level approach
    combines advantages of both sourcebased and binary-based approaches to
    dynamic analysis, but comes with the added challenge of dealing with the
    implementation details of a specific implementation of the target language.
    This thesis describes the implementation of three existing tools which use
    the mixed-level approach: Fjalar, a C/C++ dynamic analysis framework,
    Kvasir, A C/C++ value profiling tool, and Dyncomp, a tool for inferring the
    abstract types of a C or C++ program.
    \par
    Additionally, this thesis describes the steps I took in increasing the
    maintainability and portability of these tools. I investigated and
    documented platform specific dependencies; I documented the process of
    merging in upstream changes of Valgrind, the Dynamic Binary Instrumenter
    Fjalar is built on, to aid Fjalar in keeping in-sync with Valgrind
    bug-fixes; and I implemented a tool for debugging Dyncomp errors.",
  usesDaikon = "1",
  OPTusesDaikonAsTestSubject = "",
  OPTomitfromcv = "",
  basefilename = "rudd-mixedlevel-mengthesis",
  OPTdownloads = "",
  OPTdownloadsnonlocal = "",
  OPTsupersededby = "",
  category =  "Dynamic analysis",
  summary =
   "This thesis describes enhancements to tde mixed-level approach to
   dynamic binary analysis that was first proposed and implemented by Guo.",
}

@InProceedings{Polikarpova2009,
  author = 	 "Nadia Polikarpova and Ilinca Ciupa and Bertrand Meyer",
  title = 	 "A comparative study of programmer-written and automatically inferred contracts",
  booktitle = ISSTA2009,
  pages = 	 "93--104",
  year = 	 2009,
  address = 	 ISSTA2009addr,
  month = 	 ISSTA2009date,
  abstract =
   "Where do contracts --- specification elements embedded in executable code
    --- come from? To produce them, should we rely on the programmers, on
    automatic tools, or some combination?
    \par
    Recent work, in particular the Daikon system, has shown that it is possible
    to infer some contracts automatically from program executions. The main
    incentive has been an assumption that most programmers are reluctant to
    invent the contracts themselves. The experience of contract-supporting
    languages, notably Eiffel, disproves that assumption: programmers will
    include contracts if given the right tools. That experience also shows,
    however, that the resulting contracts are generally partial and
    occasionally incorrect.
    \par
    Contract inference tools provide the opportunity for studying objectively
    the quality of programmer-written contracts, and for assessing the
    respective roles of humans and tools. Working on 25 classes taken from
    different sources such as widely-used standard libraries and code written
    by students, we applied Daikon to infer contracts and compared the results
    (totaling more than 19500 inferred assertion clauses) with the already
    present contracts.
    \par
    We found that a contract inference tool can be used to strengthen
    programmer-written contracts, but cannot infer all contracts that humans
    write. The tool generates around five times as many relevant assertion
    clauses as written by programmers; but it only finds around 60\% of those
    originally written by programmers. Around a third of the generated
    assertions clauses are either incorrect or irrelevant. The study also
    uncovered interesting correlations between the quality of inferred
    contracts and some code metrics.",
  usesDaikon = 1,
  OPTbasefilename = "",
  downloads = "http://se.ethz.ch/~meyer/publications/testing/citadel-issta.pdf PDF",
  OPTdownloadsnonlocal = "",
  OPTcategory =  "",
  OPTsummary = 	 "",
}


@Article{ErnstPGMPTX2007,
  author =	 "Michael D. Ernst and Jeff H. Perkins and Philip J. Guo
                  and Stephen McCamant and Carlos Pacheco
                  and Matthew S. Tschantz and Chen Xiao",
  title =	 "The {Daikon} system for dynamic detection of likely invariants",
  journal = 	 SCP,
  year = 	 2007,
  volume = 	 69,
  number = 	 "1--3",
  pages = 	 "35--45",
  month = 	 dec,
  abstract =
   "Daikon is an implementation of dynamic detection of likely invariants;
    that is, the Daikon invariant detector reports likely program
    invariants.  An invariant is a property that holds at a certain point
    or points in a program; these are often used in assert statements,
    documentation, and formal specifications.   Examples
    include being constant ($x = a$), non-zero ($x \ne 0$), being
    in a range ($a \le x \le b$), linear relationships ($y =
    ax+b$), ordering ($x \le y$), functions from a library ($x =
    \mathrm{fn}(y)$), containment ($x \in y$), sortedness ($x\
    \mathrm{is}\ \mathrm{sorted}$), and many more.  Users can extend Daikon
    to check for additional invariants.
    \par
    Dynamic invariant detection runs a program, observes the values
    that the program computes, and then reports properties that were
    true over the observed executions.  Dynamic invariant detection is
    a machine learning technique that can be applied to arbitrary
    data.  Daikon can detect invariants in C, C + +, Java, and Perl
    programs, and in record-structured data sources; it is easy to
    extend Daikon to other applications.
    \par
    Invariants can be useful in program understanding and a host of other
    applications.
    Daikon's output has been used for generating test cases, predicting
    incompatibilities in component integration, automating
    theorem-proving, repairing inconsistent data structures, and checking
    the validity of data streams, among other tasks.
    \par
    Daikon is freely available in source and binary form, along with
    extensive documentation, at \url{http://pag.csail.mit.edu/daikon/}.",
  basefilename = "daikon-tool-scp2007",
  downloads = "http://pag.csail.mit.edu/daikon/ Daikon implementation",
  downloadsnonlocal =
    "http://homes.cs.washington.edu/~mernst/pubs/daikon-tool-scp2007.pdf PDF",
  category =     "Invariant detection",
  csetags = "mernst,mernst-Invariant-detection,plse",
  summary =
   "This paper discusses the Daikon tool, including its features,
    applications, architecture, and development process.  It is not a paper
    about dynamic invariant detection per se.",
}



@inproceedings{Guo2006,
 author = {Guo, Philip J. and Perkins, Jeff H. and McCamant, Stephen and Ernst, Michael D.},
 title = {Dynamic inference of abstract types},
 booktitle = {Proceedings of the 2006 international symposium on Software testing and analysis},
 series = {ISSTA '06},
 year = {2006},
 isbn = {1-59593-263-1},
 location = {Portland, Maine, USA},
 pages = {255--265},
 numpages = {11},
 url = {http://doi.acm.org/10.1145/1146238.1146268},
 doi = {10.1145/1146238.1146268},
 acmid = {1146268},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {C, C++, Java, abstract types, dynamic analysis, interaction, mixed-level analysis, type inference, units, values and variables},
}


@MANUAL{DaikonUserManual:Online,
	KEY          = "DaikonUserManual",
	TITLE        = "The Daikon Invariant Detector User Manual",
	MONTH        = "September",
	YEAR         = "2010",
	NOTE         = "\url{http://groups.csail.mit.edu/pag/daikon/download/doc/daikon.html}"
}

@MANUAL{DaikonDeveloperManual:Online,
	KEY          = "DaikonDeveloperManual",
	TITLE        = "The Daikon Invariant Detector Developer Manual",
	MONTH        = "September",
	YEAR         = "2010",
	NOTE         = "\url{http://groups.csail.mit.edu/pag/daikon/download/doc/developer.html}"
}

@MISC{CCI,
    author = "Microsoft Research",
    note = {\url{https://ccimetadata.codeplex.com/}}
}

@MISC{Mikunov:2003:Online,
author = {Aleksandr Mikunov},
title = {Rewrite MSIL Code on the Fly with the .NET Framework Profiling API},
month = {September},
year = {2003},
note = {\url{http://msdn.microsoft.com/en-us/magazine/cc188743.aspx}}
}

@MISC{ProfilerApiReference:Online,
KEY          = "ProfilerApiReference",
title = {Profiling (Unmanaged API Reference)},
month = {September},
year = {2010},
note = {\url{http://msdn.microsoft.com/en-us/library/ms404386.aspx}}
}

@inproceedings{pex,
 author = {Tillmann, Nikolai and De Halleux, Jonathan},
 title = {Pex: white box test generation for .NET},
 booktitle = {Proceedings of the 2nd international conference on Tests and proofs},
 series = {TAP'08},
 year = {2008},
 isbn = {3-540-79123-X, 978-3-540-79123-2},
 location = {Prato, Italy},
 pages = {134--153},
 numpages = {20},
 url = {http://dl.acm.org/citation.cfm?id=1792786.1792798},
 acmid = {1792798},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg},
}

@inproceedings{static,
 author = {F\"{a}hndrich, Manuel and Logozzo, Francesco},
 title = {Static contract checking with abstract interpretation},
 booktitle = {Proceedings of the 2010 international conference on Formal verification of object-oriented software},
 series = {FoVeOOS'10},
 year = {2011},
 isbn = {3-642-18069-8, 978-3-642-18069-9},
 location = {Paris, France},
 pages = {10--30},
 numpages = {21},
 url = {http://dl.acm.org/citation.cfm?id=1949303.1949305},
 acmid = {1949305},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg},
}

@MISC{contracts,
title = {Code Contracts},
month = {June},
year = {2013},
note = {\url{https://research.microsoft.com/en-us/projects/contracts/}}
}

@phdthesis{daikon,
 author = {Ernst, Michael Dean},
 title = {Dynamically discovering likely program invariants},
 year = {2000},
 isbn = {0-599-89515-2},
 note = {AAI9983472},
 publisher = {University of Washington},
}