seminarski.bib

@book{laski2009software,
  title={{Software Verification and Analysis}},
  author={Laski, J. and Stanley, W.},
  isbn={9781848822405},
  url={http://books.google.rs/books?id=5hFnaDQ1jiAC},
  year={2009},
  publisher={Springer-Verlag},
  address = {London}
}

@book{pham_reliability,
 author = {Pham, Hoang},
 title = {System Software Reliability (Springer Series in Reliability Engineering)},
 year = {2005},
 isbn = {1852339500},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg},
}

@book{quinn_ethics,
 author = {Quinn, Michael J.},
 title = {Ethics for the Information Age},
 year = {2016},
 isbn = {0134296540, 9780134296548},
 edition = {7th},
 publisher = {Pearson},
}

@misc{abstract_interpretation,
title = {{Abstract Interpretation}},
note = {on-line at: \url{https://www.di.ens.fr/~cousot/AI/}},
    author = {{Patrick Cousot}},
    year = {2008}
}

@article{symbolic_execution,
 author = {King, James C.},
 title = {Symbolic Execution and Program Testing},
 journal = {Commun. ACM},
 issue_date = {July 1976},
 volume = {19},
 number = {7},
 month = jul,
 year = {1976},
 issn = {0001-0782},
 pages = {385--394},
 numpages = {10},
 url = {http://doi.acm.org/10.1145/360248.360252},
 doi = {10.1145/360248.360252},
 acmid = {360252},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {program debugging, program proving, program testing, program verification, symbolic execution, symbolic interpretation},
} 

@inproceedings{ironfleet,
 author = {Hawblitzel, Chris and Howell, Jon and Kapritsos, Manos and Lorch, Jacob R. and Parno, Bryan and Roberts, Michael L. and Setty, Srinath and Zill, Brian},
 title = {IronFleet: Proving Practical Distributed Systems Correct},
 booktitle = {Proceedings of the 25th Symposium on Operating Systems Principles},
 series = {SOSP '15},
 year = {2015},
 isbn = {978-1-4503-3834-9},
 location = {Monterey, California},
 pages = {1--17},
 numpages = {17},
 url = {http://doi.acm.org/10.1145/2815400.2815428},
 doi = {10.1145/2815400.2815428},
 acmid = {2815428},
 publisher = {ACM},
 address = {New York, NY, USA},
}

@article{compcert,
 author = {Leroy, Xavier},
 title = {Formal Verification of a Realistic Compiler},
 journal = {Commun. ACM},
 issue_date = {July 2009},
 volume = {52},
 number = {7},
 month = jul,
 year = {2009},
 issn = {0001-0782},
 pages = {107--115},
 numpages = {9},
 url = {http://doi.acm.org/10.1145/1538788.1538814},
 doi = {10.1145/1538788.1538814},
 acmid = {1538814},
 publisher = {ACM},
 address = {New York, NY, USA},
} 

@inproceedings{sel4,
 author = {Klein, Gerwin and Elphinstone, Kevin and Heiser, Gernot and Andronick, June and Cock, David and Derrin, Philip and Elkaduwe, Dhammika and Engelhardt, Kai and Kolanski, Rafal and Norrish, Michael and Sewell, Thomas and Tuch, Harvey and Winwood, Simon},
 title = {seL4: Formal Verification of an OS Kernel},
 booktitle = {Proceedings of the ACM SIGOPS 22Nd Symposium on Operating Systems Principles},
 series = {SOSP '09},
 year = {2009},
 isbn = {978-1-60558-752-3},
 location = {Big Sky, Montana, USA},
 pages = {207--220},
 numpages = {14},
 url = {http://doi.acm.org/10.1145/1629575.1629596},
 doi = {10.1145/1629575.1629596},
 acmid = {1629596},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {isabelle/hol, l4, microkernel, sel4},
} 

@inproceedings{cakeml,
 author = {Kumar, Ramana and Myreen, Magnus O. and Norrish, Michael and Owens, Scott},
 title = {CakeML: A Verified Implementation of ML},
 booktitle = {Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
 series = {POPL '14},
 year = {2014},
 isbn = {978-1-4503-2544-8},
 location = {San Diego, California, USA},
 pages = {179--191},
 numpages = {13},
 url = {http://doi.acm.org/10.1145/2535838.2535841},
 doi = {10.1145/2535838.2535841},
 acmid = {2535841},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {ML, compiler bootstrapping, compiler verification, machine code verification, read-eval-print loop, verified garbage collection., verified parsing, verified type checking},
}

@misc{isabelle,
title = {{Isabelle/HOL}},
note = {on-line at: \url{https://isabelle.in.tum.de/}},
    author = {{University of Cambridge and Technische Universität München}},
    year = {2018}
}

@misc{coq,
title = {{Coq}},
note = {on-line at: \url{https://coq.inria.fr/}},
    author = {{Thierry Coquand, Gérard Pierre Huet, Christine Paulin-Mohring, Bruno Barras, Jean-Christophe Filliâtre, Hugo Herbelin, Chetan Murthy, Yves Bertot and Pierre Castéran}},
    year = {2019}
}

@misc{Statistika_prosek_gresaka,
title = {{Number of errors on 1000 lines of code}},
note = {On-line at: \url{https://news.ycombinator.com/}},
    author = {{Hacker News}},
    year = {2016}
}

@misc{ibm_halstead,
title = {{Halstead Metrics}},
note = {On-line at: \url{https://www.ibm.com/support/knowledgecenter/en/SSSHUF_8.0.2/com.ibm.rational.testrt.studio.doc/topics/csmhalstead.htm}},
    author = {{IBM Knowledge Center}}
}

@misc{holsted_primer,
title = {Halstead metric example},
note = {From Eindhoven University of Technology: \url{https://www.tue.nl/en/university/departments/mathematics-and-computer-science/}}
}

@misc{selenium,
title = {{Selenium}},
note = {Main website at: \url{https://www.seleniumhq.org}}
}

@misc{therac25,
title = {Therac-25},
note = {Source: \url{https://hackaday.com/2015/10/26/killed-by-a-machine-the-therac-25/}}
}

@misc{mars,
title = {{Mars Climate Orbiter}},
note = {Source: \url{https://www.simscale.com/blog/2017/12/nasa-mars-climate-orbiter-metric/}}
}

@misc{boeing737,
title = {{Boeing 737 MAX}},
note = {Source: \url{https://www.bbc.com/news/world-africa-47553174}}
}

@misc{larunway,
title = {{Los Angeles Runway Disaster}},
note = {Source: \url{https://wikivisually.com/wiki/Los_Angeles_runway_disaster}}
}



@misc{mccabe_fortran,
title = {{System Software Reliability}},
note = {Chapter 5.3: McCabe's Cyclomatic Complexity Metric},
    author = {{Hoang Pham}},
    year = {2006}
}

@article{haltingproblem,
    author = {Turing, A. M.},
    citeulike-article-id = {155758},
    journal = {Proceedings of the London Mathematical Society},
    keywords = {computability, entscheidungsproblem, turing},
    number = {42},
    pages = {230--265},
    posted-at = {2005-04-08 18:11:59},
    priority = {0},
    title = {{On Computable Numbers, with an application to the Entscheidungsproblem}},
    volume = {2},
    year = {1936}
}

@misc{Bayou,
title = {{Bayou}},
note = {On-line at: \url{http://askbayou.com//}},
    author = {{Department of Computer Science, Rice University}}
}