bib/swtools.bib

@unpublished{DouglasEngelbart1968
,author="Douglas Engelbart"
,title="The Demo"
,year="1968"
,month="December"
,day="9"
,note="URL:
\url{http://dougengelbart.org/firsts/dougs-1968-demo.html}"
,lastchecked="November 12, 2016"
}

@unpublished{StephenJohnson1977lint
,author="Stephen Johnson"
,title="Lint, a {C} program checker"
,year="1977"
,month="December"
,note="Computer Science Technical Report 65, Bell Laboratories"
}

@Book{GlenfordJMyers1979
,Author="Glenford J. Myers"
,title="The Art of Software Testing"
,Publisher="Wiley"
,Year="1979"
,pages="174"
}

@Book{MargaretAEllis1990Cplusplus
,Author="Margaret A. Ellis and Bjarne Stroustrup"
,title="The Annotated {C++} Reference Manual"
,Publisher="Addison Wesley"
,Year="1990"
,pages="447"
}

@unpublished{ScottGriffen2000
,author="Scott Griffen"
,title="Internet Pioneers: Doug Englebart"
,year="2000"
,month="May"
,note="Available:
\url{http://www.ibiblio.org/pioneers/englebart.html}
[Viewed November 28, 2008]"
}

@Book{Holzmann03a
,Author="Gerard J. Holzmann"
,title="The {Spin} Model Checker: Primer and Reference Manual"
,Publisher="Addison-Wesley"
,address={Boston, MA, USA}
,Year="2003"
,pages="608"
}

@unpublished{PeteBecker2009N3000
,author="Pete Becker"
,title="Working Draft, Standard for Programming Language {C++}"
,month="November"
,day="9"
,year="2009"
,note="Available:
\url{http://open-std.org/jtc1/sc22/wg21/docs/papers/2009/n3000.pdf}
[Viewed: November 9, 2009]"
}

@unpublished{PeteBecker2010N3035
,author="Pete Becker"
,title="Working Draft, Standard for Programming Language {C++}"
,month="February"
,day="16"
,year="2010"
,note="Available:
\url{http://open-std.org/jtc1/sc22/wg21/docs/papers/2010/n3035.pdf}
[Viewed: February 16, 2010]"
}

@unpublished{PeteBecker2010N3126
,author="Pete Becker"
,title="Working Draft, Standard for Programming Language {C++}"
,month="August"
,day="21"
,year="2010"
,note="Available:
\url{http://open-std.org/jtc1/sc22/wg21/docs/papers/2010/n3126.pdf}
[Viewed: February 16, 2010]"
}

@unpublished{PeteBecker2010N3225
,author="Pete Becker"
,title="Working Draft, Standard for Programming Language {C++}"
,month="November"
,day="27"
,year="2010"
,note="Available:
\url{http://open-std.org/jtc1/sc22/wg21/docs/papers/2010/n3225.pdf}
[Viewed: March 4, 2011]"
}

@unpublished{PeteBecker2011N3242
,author="Pete Becker"
,title="Working Draft, Standard for Programming Language {C++}"
,month="February"
,day="28"
,year="2011"
,note="\url{http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2011/n3242.pdf}"
}

@unpublished{StefanusDuToit2013N3691
,author="Stefanus Du Toit"
,title="Working Draft, Standard for Programming Language {C++}"
,month="May"
,day="16"
,year="2013"
,note="\url{http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2013/n3691.pdf}"
}

@unpublished{RichardSmith2015N4527
,author="Richard Smith"
,title="Working Draft, Standard for Programming Language {C++}"
,month="May"
,day="22"
,year="2015"
,note="\url{http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2015/n4527.pdf}"
}

@unpublished{JonathanCorbet2004sparse
,author="Jonathan Corbet"
,title="Finding kernel problems automatically"
,month="June"
,day="1"
,year="2004"
,note="\url{http://lwn.net/Articles/87538/}"
}

@article{Jackson:2000:FBC:347636.383378
,author = {Jackson, Daniel and Vaziri, Mandana}
,title = {Finding Bugs with a Constraint Solver}
,journal = {SIGSOFT Softw. Eng. Notes}
,issue_date = {Sept. 2000}
,volume = {25}
,number = {5}
,month = aug
,year = {2000}
,issn = {0163-5948}
,pages = {14--25}
,numpages = {12}
,url = {http://doi.acm.org/10.1145/347636.383378}
,doi = {10.1145/347636.383378}
,acmid = {383378}
,publisher = {ACM}
,address = {New York, NY, USA}
,keywords = {alloy language, constraint solvers, detecting bugs, model checking, relational formulas, static analysis, testing}
}

@inproceedings{EdmundClarke2004CBMC
,AUTHOR    = { Clarke, Edmund
               and Kroening, Daniel
               and Lerda, Flavio }
,TITLE     = { A Tool for Checking {ANSI-C} Programs }
,BOOKTITLE = { Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004) }
,YEAR      = { 2004 }
,PUBLISHER = { Springer }
,PAGES     = { 168--176 }
,ISBN      = { 3-540-21299-X }
,SERIES    = { Lecture Notes in Computer Science }
,VOLUME    = { 2988 }
,EDITOR    = { Kurt Jensen and Andreas Podelski }
}

@inproceedings{YoannPadioleau2005CollateralEvolution
,author = "Yoann Padioleau and Julia L. Lawall and Gilles Muller"
,title = "Understanding Collateral Evolution in Linux Device Drivers"
,booktitle = {Proceedings of the ACM SIGOPS EuroSys 2006 Conference}
,month = {April}
,year = {2006}
,pages = {59-71}
,publisher = {ACM}
,address = {Leuven, Belgium}
,url={http://doi.acm.org/10.1145/1217935.1217942}
}

@unpublished{JonathanCorbet2006lockdep
,author="Jonathan Corbet"
,title="The kernel lock validator"
,month="May"
,day="31"
,year="2006"
,note="Available:
\url{http://lwn.net/Articles/185666/}
[Viewed: March 26, 2010]"
}

@unpublished{StevenRostedt2010perfHP+DeathlyMacros
,author="Steven Rostedt"
,title="tracing: {Harry} {Potter} and the {Deathly} {Macros}"
,month="December"
,day="3"
,year="2010"
,note="Available:
\url{http://lwn.net/Articles/418710/}
[Viewed: August 28, 2011]"
}

@unpublished{StevenRostedt2010perfTraceEventP1
,author="Steven Rostedt"
,title="Using the {TRACE\_EVENT()} macro (Part 1)"
,month="March"
,day="24"
,year="2010"
,note="Available:
\url{http://lwn.net/Articles/379903/}
[Viewed: August 28, 2011]"
}

@unpublished{StevenRostedt2010perfTraceEventP2
,author="Steven Rostedt"
,title="Using the {TRACE\_EVENT()} macro (Part 2)"
,month="March"
,day="31"
,year="2010"
,note="Available:
\url{http://lwn.net/Articles/381064/}
[Viewed: August 28, 2011]"
}

@unpublished{StevenRostedt2010perfTraceEventP3
,author="Steven Rostedt"
,title="Using the {TRACE\_EVENT()} macro (Part 3)"
,month="April"
,day="21"
,year="2010"
,note="Available:
\url{http://lwn.net/Articles/383362/}
[Viewed: August 28, 2011]"
}

@unpublished{MathieuDesnoyers2009LFCollabSummit
,author="Mathieu Desnoyers and Michel R. Dagenais"
,title="LTTng, Filling the Gap Between Kernel Instrumentation and a Widely Usable Kernel Tracer"
,month="April"
,day="8"
,year="2009"
,note="Available:
\url{http://events.linuxfoundation.org/slides/lfcs09_desnoyers_paper.pdf}
[Viewed: August 28, 2011]"
}

@unpublished{Maranget2012TutorialARMPower
,Author="Luc Maranget and Susmit Sarkar and Peter Sewell"
,Title="A Tutorial Introduction to the {ARM} and {POWER} Relaxed Memory Models"
,month="October"
,day="10"
,year="2012"
,note="\url{https://www.cl.cam.ac.uk/~pes20/ppc-supplemental/test7.pdf}"
}

@unpublished{PaulEMcKenney2011ppcmem
,Author="Paul E. McKenney"
,Title="Validating Memory Barriers and Atomic Instructions"
,month="December"
,day="6"
,year="2011"
,note="\url{http://lwn.net/Articles/470681/}"
}

@unpublished{JadeAlglave2011ppcmem
,Author="Jade Alglave and Luc Maranget and Pankaj Pawan and Susmit Sarkar and Peter Sewell and Derek Williams and Francesco Zappa Nardelli"
,Title="{PPCMEM/ARMMEM}: A Tool for Exploring the {POWER} and {ARM} Memory Models"
,month="June"
,day="4"
,year="2011"
,note="\url{http://www.cl.cam.ac.uk/~pes20/ppc-supplemental/pldi105-sarkar.pdf}"
}

@unpublished{RichardBornat2006SheepGoats
,Author="Richard Bornat"
,Title="Dividing the Sheep from the Goats"
,month="January"
,day="24"
,year="2006"
,note={Seminar at School of Computing, Univ. of Kent. Abstract is available at
\url{https://www.cs.kent.ac.uk/seminar_archive/2005_06/abs_2006_01_24.html}.
Retracted in July 2014:
\url{http://www.eis.mdx.ac.uk/staffpages/r_bornat/papers/camel_hump_retraction.pdf}}
,lastchecked="November 28, 2016"
}

@inproceedings{SaeedDehnadi2009SheepGoats
,author = {Saeed Dehnadi and Richard Bornat and Ray Adams}
,title = {Meta-analysis of the effect of consistency on success in early learning of programming}
,booktitle = {PPIG 2009}
,month = {June}
,year = {2009}
,pages = {1--13}
,numpages = {13}
,publisher = {Psychology of Programming Interest Group}
,address = {University of Limerick, Ireland}
,url={http://www.ppig.org/papers/21st-dehnadi.pdf}
,lastchecked="November 12, 2016"
}

@unpublished{RegBraithwaite2007FizzBuzz
,Author="Reg Braithwaite"
,Title="Don't Overthink FizzBuzz"
,month="January"
,day="24"
,year="2007"
,note={\url{http://weblog.raganwald.com/2007/01/dont-overthink-fizzbuzz.html}}
}

@unpublished{StevenRostedt2011locdepCryptic
,Author="Steven Rostedt"
,Title="lockdep: How to read its cryptic output"
,month="September"
,day="9"
,year="2011"
,note={\url{http://www.linuxplumbersconf.org/2011/ocw/sessions/153}}
}

@unpublished{ValgrindHomePage
,Author="{The Valgrind Developers}"
,Title="Valgrind"
,month="November"
,day="10"
,year="2011"
,note={\url{http://www.valgrind.org/}}
}

@unpublished{OProfileHomePage
,Author="{The OProfile Developers}"
,Title="OProfile"
,month="April"
,day="28"
,year="2012"
,note={\url{http://oprofile.sourceforge.net}}
}

@unpublished{LinuxKernelPerfWiki
,Author="Stephane Eranian and Eric Gouriou and Tipp Moseley and Willem de Bruijn"
,Title="Linux kernel profiling with perf"
,month="June"
,day="29"
,year="2011"
,note={\url{https://perf.wiki.kernel.org/index.php/Tutorial}}
}

@unpublished{NishanthAravamudan2005stiu
,author="Nishanth Aravamudan"
,title="{[PATCH]} Add schedule\_timeout\_\{in\-ter\-rupt\-i\-ble,un\-in\-ter\-rupt\-i\-ble\}\{,\_msecs\}() interfaces"
,month="July"
,day="22"
,year="2005"
,url={http://lwn.net/Articles/144763/}
,note="Linux Weekly News"
}

@book{Kroening:2008:DPA:1391237
,author = {Kroening, Daniel and Strichman, Ofer}
,title = {Decision Procedures: An Algorithmic Point of View}
,year = {2008}
,isbn = {3540741046, 9783540741046}
,edition = {1}
,publisher = {Springer Publishing Company, Incorporated}
}

@unpublished{JohnRegehr2010UndefinedBehavior
,Author="John Regehr"
,Title="A Guide to Undefined Behavior in C and C++, Part 1"
,month="July"
,day="9"
,year="2010"
,note="\url{http://blog.regehr.org/archives/213}"
}

@inproceedings{Golovanevsky:2010:TDL:2174824.2174835
,author = {Golovanevsky, Olga and Dayan, Alon and Zaks, Ayal and Edelsohn, David}
,title = {Trace-Based Data Layout Optimizations for Multi-core Processors}
,booktitle = {Proceedings of the 5th International Conference on High Performance Embedded Architectures and Compilers}
,series = {HiPEAC'10}
,year = {2010}
,isbn = {3-642-11514-4, 978-3-642-11514-1}
,location = {Pisa, Italy}
,pages = {81--95}
,numpages = {15}
,url = {http://dx.doi.org/10.1007/978-3-642-11515-8_8}
,doi = {10.1007/978-3-642-11515-8_8}
,acmid = {2174835}
,publisher = {Springer-Verlag}
,address = {Berlin, Heidelberg}
,keywords = {cache-conscious data layout, compiler optimizations, data affinity, false sharing, spatial locality}
}

@inproceedings{NicolasPalix2011CoccinelleTenYears
,author = {Nicolas Palix and Ga\"{e}l Thomas and Suman Saha and Christophe Calv\`{e}s and Julia Lawall and Gilles Muller}
,title = "Faults in Linux: Ten Years Later"
,booktitle = {Proceedings of the Sixteenth International Conference on
Architectural Support for Programming Languages and Operating Systems
(ASPLOS 2011)}
,month = {March}
,year = {2011}
,pages = {305-318}
,publisher = {ACM}
,address = {Newport Beach, California, USA}
,url={http://dx.doi.org/10.1145/1950365.1950401}
}

@Conference{DaveJones2011Trinity
,author = "Dave Jones"
,title = "Trinity: A system call fuzzer"
,booktitle = {Proceedings of the 13\textsuperscript{th} Ottawa Linux Symposium}
,month = {June}
,year = {2011}
,pages = {???--???}
,address = {Ottawa, Canada}
,url={http://codemonkey.org.uk/projects/trinity/}
}

@unpublished{PaulEMcKenney2012SignedOverflow
,Author="Paul E. McKenney"
,Title="Signed overflow optimization hazards in the kernel"
,month="August"
,day="15"
,year="2012"
,note="\url{http://lwn.net/Articles/511259/}"
}

@inproceedings{Alglave:2013:SVW:2450268.2450306
,author = {Alglave, Jade and Kroening, Daniel and Nimal, Vincent and Tautschnig, Michael}
,title = {Software verification for weak memory via program transformation}
,booktitle = {Proceedings of the 22nd European conference on Programming Languages and Systems}
,series = {ESOP'13}
,year = {2013}
,isbn = {978-3-642-37035-9}
,location = {Rome, Italy}
,pages = {512--532}
,numpages = {21}
,url = {http://dx.doi.org/10.1007/978-3-642-37036-6_28}
,doi = {10.1007/978-3-642-37036-6_28}
,acmid = {2450306}
,publisher = {Springer-Verlag}
,address = {Berlin, Heidelberg}
}

@inproceedings{VijayDSilva2012-sas
,AUTHOR={ D'Silva, Vijay and Haller, Leopold and Kroening, Daniel }
,TITLE={ Satisfiability Solvers are Static Analyzers }
,BOOKTITLE={ Static Analysis Symposium (SAS) }
,YEAR={ 2012 }
,PUBLISHER={ Springer }
,PAGES={ 317--333 }
,SERIES={ LNCS }
,VOLUME={ 7460 }
,DOI={ 10.1007/978-3-642-33125-1_22 }
}

@inproceedings{JadeAlglave2013-WeaknessIsVirtue
,AUTHOR={ Alglave, Jade }
,TITLE={ Weakness is a virtue }
,BOOKTITLE={ ({EC})\textsuperscript{2} 2013: 6\textsuperscript{th}
International Workshop on Exploiting Concurrency Efficiently and Correctly }
,YEAR={ 2013 }
,PAGES={3}
,URL={ http://www0.cs.ucl.ac.uk/staff/j.alglave/papers/ec213.pdf }
,LASTCHECKED={ November 12, 2016 }
}

@inproceedings{JadeAlglave2013-cav
,AUTHOR={ Alglave, Jade and Kroening, Daniel and Tautschnig, Michael }
,TITLE={ Partial Orders for Efficient {Bounded Model Checking} of Concurrent Software }
,BOOKTITLE={ Computer Aided Verification (CAV) }
,YEAR={ 2013 }
,PUBLISHER={ Springer }
,PAGES={ 141--157 }
,SERIES={ LNCS }
,VOLUME={ 8044 }
,DOI={ 10.1007/978-3-642-39799-8_9 }
}

@unpublished{PaulEMcKenney2013PlumbersValidation
,Author="Paul E. McKenney"
,Title="Advances in validation of concurrent software"
,month="September"
,day="19"
,year="2013"
,note="\url{http://www.rdrop.com/users/paulmck/scalability/paper/Validation.2013.09.19b.pdf}"
}

@inproceedings{Lin:2013:CMJ:2510665.2511597
,author = {Lin, Yu and Dig, Danny}
,title = {CHECK-THEN-ACT Misuse of Java Concurrent Collections}
,booktitle = {Proceedings of the 2013 IEEE Sixth International Conference on Software Testing, Verification and Validation}
,series = {ICST '13}
,year = {2013}
,isbn = {978-0-7695-4968-2}
,pages = {164--173}
,numpages = {10}
,url = {http://dx.doi.org/10.1109/ICST.2013.41}
,doi = {10.1109/ICST.2013.41}
,acmid = {2511597}
,publisher = {IEEE Computer Society}
,address = {Washington, DC, USA}
,keywords = {Java Concurrent Collection, Check-then-Act, Atomicity Violation, Empirical Study}
}

@inproceedings{Alglave:2014:HCM:2594291.2594347
,author = {Alglave, Jade and Maranget, Luc and Tautschnig, Michael}
,title = {Herding Cats: Modelling, Simulation, Testing, and Data-mining for Weak Memory}
,booktitle = {Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation}
,series = {PLDI '14}
,year = {2014}
,isbn = {978-1-4503-2784-8}
,location = {Edinburgh, United Kingdom}
,pages = {40--40}
,numpages = {1}
,url = {http://doi.acm.org/10.1145/2594291.2594347}
,doi = {10.1145/2594291.2594347}
,acmid = {2594347}
,publisher = {ACM}
,address = {New York, NY, USA}
,keywords = {concurrency, verification, weak memory models}
}

@article{Palix:2014:FL:2642648.2619090
,author = {Palix, Nicolas and Thomas, Ga\={e}l and Saha, Suman and Calv\`{e}s, Christophe and Muller, Gilles and Lawall, Julia}
,title = {Faults in Linux 2.6}
,journal = {ACM Trans. Comput. Syst.}
,issue_date = {June 2014}
,volume = {32}
,number = {2}
,month = jun
,year = {2014}
,issn = {0734-2071}
,pages = {4:1--4:40}
,articleno = {4}
,numpages = {40}
,url = {http://doi.acm.org/10.1145/2619090}
,doi = {10.1145/2619090}
,acmid = {2619090}
,publisher = {ACM}
,address = {New York, NY, USA}
,keywords = {Linux, fault finding}
}

@unpublished{CarlLeonardsson2014Nidhugg
,Author="Carl Leonardsson and Kostis Sagonas and Truc Nguyen Lam and
Michalis Kokologiannakis"
,Title="Nidhugg"
,month="July"
,day="13"
,year="2014"
,note="\url{https://github.com/nidhugg/nidhugg}"
}

@unpublished{PaulEMcKenney2014weakaxiom
,Author="Paul E. McKenney and Alan Stern"
,Title="Axiomatic validation of memory barriers and atomic instructions"
,month="August"
,day="19"
,year="2014"
,note="\url{http://lwn.net/Articles/608550/}"
}

@phdthesis{VincentNimalPhD
,author="Vincent Nimal"
,title="Static analyses over weak memory"
,school="University of Oxford"
,year="2014"
}

@unpublished{DeadlockEmpire2016
,Author="Michael Pokorny"
,Title="The Deadlock Empire"
,month="February"
,day="9"
,year="2016"
,note="\url{https://deadlockempire.github.io/}"
}

@unpublished{PaulEMcKenney2016P0124R2-LKMM
,Author="Paul E. McKenney and Ulrich Weigand and Andrea Parri and Boqun Feng"
,Title="Linux-Kernel Memory Model"
,month="June"
,day="6"
,year="2016"
,note="\url{http://open-std.org/JTC1/SC22/WG21/docs/papers/2016/p0124r2.html}"
}

@article{Roychoudhury:2016:FSD:2963119.2856103
,author = {Roychoudhury, Abhik and Chandra, Satish}
,title = {Formula-based Software Debugging}
,journal = {Commun. ACM}
,issue_date = {July 2016}
,volume = {59}
,number = {7}
,month = jun
,year = {2016}
,issn = {0001-0782}
,pages = {68--77}
,numpages = {10}
,url = {http://doi.acm.org/10.1145/2856103}
,doi = {10.1145/2856103}
,acmid = {2856103}
,publisher = {ACM}
,address = {New York, NY, USA}
}

@inproceedings{Groce:2015:VMC:2916135.2916190
,author = {Groce, Alex and Ahmed, Iftekhar and Jensen, Carlos and McKenney, Paul E.}
,title = {How Verified is My Code? Falsification-Driven Verification (T)}
,booktitle = {Proceedings of the 2015 30th IEEE/ACM International Conference on Automated Software Engineering (ASE)}
,series = {ASE '15}
,year = {2015}
,isbn = {978-1-5090-0025-8}
,pages = {737--748}
,numpages = {12}
,url = {http://dx.doi.org/10.1109/ASE.2015.40}
,doi = {10.1109/ASE.2015.40}
,acmid = {2916190}
,publisher = {IEEE Computer Society}
,address = {Washington, DC, USA}
}

@unpublished{JadeAlglave2017LWN-LKMM-1
,author="Jade Alglave and Luc Maranget and Paul E. McKenney and Andrea Parri and Alan Stern"
,title="A formal kernel memory-ordering model (part 1)"
,month="April"
,day="14"
,year="2017"
,note="\url{https://lwn.net/Articles/718628/}"
}

@unpublished{JadeAlglave2017LWN-LKMM-2
,author="Jade Alglave and Luc Maranget and Paul E. McKenney and Andrea Parri and Alan Stern"
,title="A formal kernel memory-ordering model (part 2)"
,month="April"
,day="20"
,year="2017"
,note="\url{https://lwn.net/Articles/720550/}"
}