@article(SpecSharp,
 author       = {Mike Barnett and Manuel F{\"a}hndrich and K. Rustan M. Leino and Peter M{\"u}ller and Wolfram Schulte and Herman Venter},
 year         = {2011},
 title        = {Specification and verification: the {Spec\#} experience},
 journal      = {Commun. ACM},
 volume       = {54},
 number       = {6},
 pages        = {81--91},
 doi          = {10.1145/1953122.1953145},
 note         = {\url{http://specsharp.codeplex.com/}},
)
@inproceedings(Bruns11,
 author       = {Daniel Bruns},
 year         = {2011},
 title        = {Specification of Red-black Trees: Showcasing Dynamic Frames, Model Fields and Sequences},
 booktitle    = {10th~{KeY} Symposium},
 note         = {\url{http://digbib.ubka.uni-karlsruhe.de/volltexte/1000024828}},
)
@inproceedings(VCC,
 author       = {Ernie Cohen and Markus Dahlweid and Mark A. Hillebrand and Dirk Leinenbach and Michal Moskal and Thomas Santen and Wolfram Schulte and Stephan Tobies},
 year         = {2009},
 title        = {{VCC:} A Practical System for Verifying Concurrent {C}},
 booktitle    = {TPHOLs},
 series       = {LNCS},
 volume       = {5674},
 publisher    = {Springer},
 pages        = {23--42},
 doi          = {10.1007/978-3-642-03359-9\_2},
 note         = {\url{http://vcc.codeplex.com/}},
)
@misc(Dafny-examples,
 year         = {Last access: Nov.~2014},
 title        = {Dafny example gallery},
 howpublished = {\url{http://dafny.codeplex.com/SourceControl/latest}},
)
@proceedings(tfm-2004,
 editor       = {C. Neville Dean and Raymond T. Boute},
 year         = {2004},
 title        = {Teaching Formal Methods, CoLogNET/FME Symposium, {TFM} 2004, Ghent, Belgium, November 18--19, 2004, Proceedings},
 series       = {LNCS},
 volume       = {3294},
 publisher    = {Springer},
 doi          = {10.1007/b102075},
)
@proceedings(tfm-2009,
 editor       = {Jeremy Gibbons and Jos{\'{e}} Nuno Oliveira},
 year         = {2009},
 title        = {Teaching Formal Methods, Second International Conference, {TFM} 2009, Eindhoven, The Netherlands, November 2--6, 2009. Proceedings},
 series       = {LNCS},
 volume       = {5846},
 publisher    = {Springer},
 doi          = {10.1007/978-3-642-04912-5},
)
@inproceedings(gladischTyszberowicz2013,
 author       = {Christoph Gladisch and Shmuel Tyszberowicz},
 year         = {2013},
 title        = {Specifying a Linked Data Structure in {JML} for Formal Verification and Runtime Checking},
 booktitle    = {SBMF},
 series       = {LNCS},
 volume       = {8195},
 publisher    = {Springer},
 pages        = {99--114},
 doi          = {10.1007/978-3-642-41071-0\_8},
)
@proceedings(formed,
 editor       = {Z. Istenes},
 year         = {2008},
 title        = {Formal Methods in Computer Science Education, {FORMED} 2008, Budapest, Hungary, March 29, 2008, Proceedings},
 note         = {\url{http://157.181.166.108/pdf/FORMED_2008.pdf}},
)
@inproceedings(Jaume-Laurent14a,
 author       = {Mathieu Jaume and Th{\'{e}}o Laurent},
 year         = {2014},
 title        = {Teaching Formal Methods and Discrete Mathematics},
 booktitle    = {F-IDE},
 series       = {{EPTCS}},
 volume       = {149},
 pages        = {30--43},
 doi          = {10.4204/EPTCS.149.4},
)
@inproceedings(Kiniry-Zimmerman08a,
 author       = {Joseph R. Kiniry and Daniel M. Zimmerman},
 year         = {2008},
 title        = {Secret Ninja Formal Methods},
 booktitle    = {FM 2008},
 series       = {LNCS},
 volume       = {5014},
 publisher    = {Springer},
 pages        = {214--228},
 doi          = {10.1007/978-3-540-68237-0\_16},
)
@techreport(BoogieManual,
 author       = {K. Rustan M. Leino},
 year         = {2008},
 title        = {This is {Boogie} 2},
 type         = {Technical Report},
 institution  = {Microsoft Research},
 url          = {http://research.microsoft.com/apps/pubs/default.aspx?id=147643},
 note         = {\url{http://research.microsoft.com/apps/pubs/default.aspx?id=147643}},
)
@inproceedings(Dafny,
 author       = {K. Rustan M. Leino},
 year         = {2010},
 title        = {{Dafny}: An Automatic Program Verifier for Functional Correctness},
 booktitle    = {LPAR-16},
 series       = {LNCS},
 volume       = {6355},
 publisher    = {Springer},
 pages        = {348--370},
 doi          = {10.1007/978-3-642-17511-4\_20},
 note         = {\url{http://research.microsoft.com/en-us/projects/dafny/}},
)
@incollection(auto-active-LM,
 author       = {K. Rustan M. Leino and Micha{\l} Moskal},
 year         = {2010},
 title        = {Usable Auto-Active Verification},
 booktitle    = {Usable Verification Workshop},
 publisher    = {\url{http://fm.csl.sri.com/UV10/}},
)
@inproceedings(Leino04,
 author       = {K. Rustan M. Leino and Peter M{\"{u}}ller},
 year         = {2004},
 title        = {Object Invariants in Dynamic Contexts},
 booktitle    = {ECOOP},
 series       = {LNCS},
 volume       = {3086},
 publisher    = {Springer},
 pages        = {491--516},
 doi          = {10.1007/978-3-540-24851-4\_22},
)
@inproceedings(Mehnert12,
 author       = {Hannes Mehnert and Filip Sieczkowski and Lars Birkedal and Peter Sestoft},
 year         = {2012},
 title        = {Formalized Verification of Snapshotable Trees: Separation and Sharing},
 booktitle    = {VSTTE},
 series       = {LNCS},
 volume       = {7152},
 pages        = {179--195},
 doi          = {10.1007/978-3-642-27705-4\_15},
)
@inproceedings(MitschQP14,
 author       = {Stefan Mitsch and Jan{-}David Quesel and Andr{\'{e}} Platzer},
 year         = {2014},
 title        = {Refactoring, Refinement, and Reasoning -- {A} Logical Characterization for Hybrid Systems},
 booktitle    = {{FM}},
 series       = {LNCS},
 volume       = {8442},
 publisher    = {Springer},
 pages        = {481--496},
 doi          = {10.1007/978-3-319-06410-9\_33},
)
@inproceedings(PFM10-VSTTE10,
 author       = {Nadia Polikarpova and Carlo A. Furia and Bertrand Meyer},
 year         = {2010},
 title        = {Specifying Reusable Components},
 booktitle    = {VSTTE},
 series       = {LNCS},
 volume       = {6217},
 publisher    = {Springer},
 pages        = {127--141},
 doi          = {10.1007/978-3-642-15057-9\_9},
)
@inproceedings(EB2,
 author       = {Nadia Polikarpova and Julian Tschannen and Carlo A. Furia},
 year         = {2015},
 title        = {A Fully Verified Container Library},
 booktitle    = {FM},
 series       = {LNCS},
 volume       = {9109},
 publisher    = {Springer},
 pages        = {414--434},
 doi          = {10.1007/978-3-319-19249-9\_26},
)
@inproceedings(semicola,
 author       = {Nadia Polikarpova and Julian Tschannen and Carlo A. Furia and Bertrand Meyer},
 year         = {2014},
 title        = {Flexible Invariants Through Semantic Collaboration},
 booktitle    = {FM},
 series       = {LNCS},
 volume       = {8442},
 publisher    = {Springer},
 pages        = {514--530},
 doi          = {10.1007/978-3-319-06410-9\_35},
)
@inproceedings(Poll09a,
 author       = {Erik Poll},
 year         = {2009},
 title        = {Teaching Program Specification and Verification Using {JML} and {ESC/Java2}},
 booktitle    = {TFM 2009},
 series       = {LNCS},
 volume       = {5846},
 publisher    = {Springer},
 pages        = {92--104},
 doi          = {10.1007/978-3-642-04912-5\_7},
)
@article(sttt-paper,
 author       = {Julian Tschannen and Carlo A. Furia and Martin Nordio},
 year         = {2014},
 title        = {{A}uto{P}roof Meets Some Verification Challenges},
 journal      = {International Journal on Software Tools for Technology Transfer},
 doi          = {10.1007/s10009-014-0300-y},
)
@inproceedings(TFNM11-SEFM11,
 author       = {Julian Tschannen and Carlo A. Furia and Martin Nordio and Bertrand Meyer},
 year         = {2011},
 title        = {Usable Verification of Object-Oriented Programs by Combining Static and Dynamic Techniques},
 booktitle    = {SEFM},
 series       = {LNCS},
 volume       = {7041},
 publisher    = {Springer},
 pages        = {382--398},
 doi          = {10.1007/978-3-642-24690-6\_26},
)
@inproceedings(tacas15,
 author       = {Julian Tschannen and Carlo A. Furia and Martin Nordio and Nadia Polikarpova},
 year         = {2015},
 title        = {{A}uto{P}roof: Auto-active Functional Verification of Object-oriented Programs},
 booktitle    = {TACAS},
 series       = {LNCS},
 volume       = {9035},
 publisher    = {Springer},
 pages        = {566--580},
 doi          = {10.1007/978-3-662-46681-0\_53},
)
@misc(VeriFast-examples,
 year         = {Last access: Nov.~2014},
 title        = {VeriFast example gallery},
 howpublished = {\url{http://people.cs.kuleuven.be/~bart.jacobs/verifast/examples/}},
)
@misc(Why3-examples,
 year         = {Last access: Nov.~2014},
 title        = {Why3 example gallery},
 howpublished = {\url{http://toccata.lri.fr/gallery/why3.en.html}},
)