@book(ahrendt2016deductive, author = {Wolfgang Ahrendt and Bernhard Beckert and Richard Bubel and Reiner H{\"a}hnle and Peter H Schmitt and Mattias Ulbrich}, year = {2016}, title = {{Deductive Software Verification--The KeY Book: From Theory to Practice}}, publisher = {Springer}, doi = {10.1007/978-3-319-49812-6}, ) @article(BFL+11, 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 = {Comm.\ ACM}, volume = {54}, pages = {81--91}, doi = {10.1145/1953122.1953145}, ) @article(baumann2012lessons, author = {Christoph Baumann and Bernhard Beckert and Holger Blasum and Thorsten Bormer}, year = {2012}, title = {{Lessons Learned from Microkernel Verification--Specification is the new Bottleneck}}, journal = {SSV}, doi = {10.4204/EPTCS.102.4}, ) @inproceedings(beckert2016deductive, author = {Bernhard Beckert and Thorsten Bormer and Daniel Grahl}, year = {2016}, title = {{Deductive Verification of Legacy Code}}, booktitle = {Proc.\ Int'l Symposium Leveraging Applications of Formal Methods, Verification and Validation (ISoLA)}, organization = {Springer}, pages = {749--765}, doi = {10.1007/978-3-319-47166-2_53}, ) @book(BHS07, author = {Bernhard Beckert and Reiner H\"ahnle and Peter Schmitt}, year = {2007}, title = {{Verification of Object-Oriented Software: The {KeY} Approach}}, publisher = {Springer}, address = {Berlin, Heidelberg}, ) @inproceedings(beckert2017proving, author = {Bernhard Beckert and Jonas Schiffl and Peter H Schmitt and Mattias Ulbrich}, year = {2017}, title = {Proving JDK’s Dual Pivot Quicksort Correct}, booktitle = {Working Conference on Verified Software: Theories, Tools, and Experiments}, organization = {Springer}, pages = {35--48}, doi = {10.1007/978-3-319-47846-3_5}, ) @book(BC04, author = {Yves Bertot and Pierre Cast\'eran}, year = {2004}, title = {{Interactive Theorem Proving and Program Development - Coq'Art: The Calculus of Inductive Constructions}}, publisher = {Springer}, address = {Berlin, Heidelberg}, doi = {10.1007/978-3-662-07964-5}, ) @inproceedings(bhargavan2017everest, author = {Karthikeyan Bhargavan and Barry Bond and Delignat-Lavaud, Antoine and C{\'e}dric Fournet and Chris Hawblitzel and Catalin Hritcu and Samin Ishtiaq and Markulf Kohlweiss and Rustan Leino and Jay Lorch}, year = {2017}, title = {{Everest: Towards a Verified, Drop-in Replacement of HTTPS}}, booktitle = {Leibniz International Proceedings in Informatics (LIPIcs)}, volume = {71}, organization = {Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik}, doi = {10.4230/LIPIcs.SNAPL.2017.1}, ) @article(BS:SEJ93, author = {Jonathan Bowen and Victoria Stavridou}, year = {1993}, title = {{Safety-critical Systems, Formal Methods and Standards}}, journal = {Software Engineering Journal}, volume = {8}, number = {4}, pages = {189--209}, doi = {10.1049/sej.1993.0025}, ) @article(BM13, author = {Hagen Buchwald and Florian Meyerer}, year = {2013}, title = {{C4J: Contracts, Java und Eclipse}}, journal = {Eclipse Magazin}, volume = {13}, number = {3}, pages = {64--69}, ) @article(BCC+05, author = {Lilian Burdy and Yoonsik Cheon and David R. Cok and Michael D. Ernst and Joseph Kiniry and Gary T. Leavens and K. Rustan M. Leino and Erik Poll}, year = {2005}, title = {{An Overview of JML Tools and Applications}}, journal = {Int'l J.\ Software Tools for Technology Transfer (STTT)}, volume = {7}, number = {3}, pages = {212--232}, doi = {10.1007/s10009-004-0167-4}, ) @book(CGP99, author = {Edmund M. Clarke and Orna Grumberg and Doron A. Peled}, year = {1999}, title = {{Model Checking}}, publisher = {MIT Press}, address = {Cambridge, Massachussetts}, ) @article(CW:CSUR96, author = {Edmund M Clarke and Jeannette M Wing}, year = {1996}, title = {Formal methods: State of the Art and Future Directions}, journal = {ACM Computing Surveys (CSUR)}, volume = {28}, number = {4}, pages = {626--643}, doi = {10.1145/242223.242257}, ) @inproceedings(cohen2009vcc, author = {Ernie Cohen and Markus Dahlweid and Mark Hillebrand and Dirk Leinenbach and Micha{\l} Moskal and Thomas Santen and Wolfram Schulte and Stephan Tobies}, year = {2009}, title = {{VCC: A Practical System for Verifying Concurrent C}}, booktitle = {Proc.\ Int'l.\ Conf.\ Theorem Proving in Higher Order Logics (TPHOLs)}, organization = {Springer}, pages = {23--42}, doi = {10.1007/978-3-540-74591-4_15}, ) @inproceedings(C:NFM11, author = {David R. Cok}, year = {2011}, title = {{OpenJML: JML for Java 7 by Extending OpenJDK}}, booktitle = {Proc.\ Int'l Conf.\ NASA Formal Methods (NFM)}, publisher = {Springer}, address = {Berlin, Heidelberg}, pages = {472--479}, doi = {10.1007/978-3-642-18070-5_13}, ) @inproceedings(cok2004esc, author = {David R Cok and Joseph Kiniry}, year = {2004}, title = {{ESC/Java2: Uniting ESC/Java and JML}}, booktitle = {Proc.\ Int'l Conf.\ Construction and Analysis of Safe, Secure, and Interoperable Smart Devices (CASSIS)}, volume = {3362}, organization = {Springer}, pages = {108--128}, doi = {10.1007/978-3-540-30569-9_6}, ) @inproceedings(cuoq2012frama, author = {Pascal Cuoq and Florent Kirchner and Nikolai Kosmatov and Virgile Prevosto and Julien Signoles and Boris Yakobowski}, year = {2012}, title = {{Frama-C}}, booktitle = {Proc.\ Int'l.\ Conf.\ Software Engineering and Formal Methods (SEFM)}, organization = {Springer}, pages = {233--247}, doi = {10.1007/978-3-642-33826-7_16}, ) @inproceedings(de2015openjdk, author = {De Gouw, Stijn and Jurriaan Rot and Frank S de Boer and Richard Bubel and Reiner H{\"a}hnle}, year = {2015}, title = {{OpenJDK’s Java.utils.Collection.sort() is Broken: The Good, the Bad and the Worst Case}}, booktitle = {Proc.\ Int'l Conf.\ Computer Aided Verification (CAV)}, organization = {Springer}, pages = {273--289}, doi = {10.1007/978-3-319-21690-4_16}, ) @article(ernst2015kiv, author = {Gidon Ernst and J{\"o}rg Pf{\"a}hler and Gerhard Schellhorn and Dominik Haneberg and Wolfgang Reif}, year = {2015}, title = {{KIV: Overview and VerifyThis Competition}}, journal = {Int'l J.\ Software Tools for Technology Transfer (STTT)}, volume = {17}, number = {6}, pages = {677--694}, doi = {10.1007/s10009-014-0308-3}, ) @inproceedings(estler2014contracts, author = {H-Christian Estler and Carlo A Furia and Martin Nordio and Marco Piccioni and Bertrand Meyer}, year = {2014}, title = {{Contracts in Practice}}, booktitle = {International Symposium on Formal Methods}, organization = {Springer}, pages = {230--246}, doi = {10.1007/978-3-319-06410-9_17}, ) @inproceedings(FM07, author = {Jean-Christophe Filli\^atre and Claude March\'e}, year = {2007}, title = {{The Why/Krakatoa/Caduceus Platform for Deductive Program Verification}}, booktitle = {Computer Aided Verification}, publisher = {Springer}, address = {Berlin, Heidelberg}, pages = {173--177}, doi = {10.1007/978-3-540-73368-3_21}, ) @article(F67, author = {Robert W. Floyd}, year = {1967}, title = {{Assigning Meanings to Programs}}, journal = {Mathematical Aspects of Computer Science}, volume = {19}, pages = {19--32}, doi = {10.1090/psapm/019/0235771}, ) @article(furia2017autoproof, author = {Carlo A Furia and Martin Nordio and Nadia Polikarpova and Julian Tschannen}, year = {2017}, title = {{AutoProof: Auto-Active Functional Verification of Object-Oriented Programs}}, journal = {Int'l J.\ Software Tools for Technology Transfer (STTT)}, volume = {19}, number = {6}, pages = {697--716}, doi = {10.1007/s10009-016-0419-0}, ) @article(HLL+12, author = {John Hatcliff and Gary T. Leavens and K. Rustan M. Leino and Peter M\"{u}ller and Matthew Parkinson}, year = {2012}, title = {{Behavioral Interface Specification Languages}}, journal = {ACM Computing Surveys}, volume = {44}, number = {3}, pages = {16:1--16:58}, doi = {10.1145/2187671.2187678}, ) @inproceedings(hawblitzel2015ironfleet, author = {Chris Hawblitzel and Jon Howell and Manos Kapritsos and Jacob R Lorch and Bryan Parno and Michael L Roberts and Srinath Setty and Brian Zill}, year = {2015}, title = {{IronFleet: Proving Practical Distributed Systems Correct}}, booktitle = {Proc.\ Symposium on Operating Systems Principles (SOSP)}, organization = {ACM}, pages = {1--17}, doi = {10.1145/2815400.2815428}, ) @inproceedings(hawblitzel2014ironclad, author = {Chris Hawblitzel and Jon Howell and Jacob R Lorch and Arjun Narayan and Bryan Parno and Danfeng Zhang and Brian Zill}, year = {2014}, title = {{Ironclad Apps: End-to-End Security via Automated Full-System Verification}}, booktitle = {Proc.\ USENIX Symposium Operating Systems Design and Implementation (OSDI)}, volume = {14}, pages = {165--181}, ) @inproceedings(H:JMLC03, author = {C. A. R. Hoare}, year = {2003}, title = {{The Verifying Compiler: A Grand Challenge for Computing Research}}, booktitle = {Proc.\ Joint Modular Languages Conference (JMLC)}, publisher = {Springer}, address = {Berlin, Heidelberg}, pages = {25--35}, doi = {10.1007/978-3-540-45213-3_4}, ) @inproceedings(kaiser2007evolution, author = {Robert Kaiser and Stephan Wagner}, year = {2007}, title = {{Evolution of the PikeOS Microkernel}}, booktitle = {Proc.\ Int'l.\ Workshop on Microkernels for Embedded Systems (MIKES)}, pages = {50}, ) @inproceedings(knight1997formal, author = {John C Knight and Colleen L DeJong and Matthew S Gibble and Luis G Nakano}, year = {1997}, title = {{Why are Formal Methods not used more Widely?}}, booktitle = {Fourth NASA Langley Formal Methods Workshop}, organization = {Citeseer}, doi = {10.1.1.2.3395}, ) @inproceedings(KTPS:ITP18, author = {Alexander Kn\"uppel and Thomas Th\"um and Carsten I. Pardylla and Ina Schaefer}, year = {2018}, title = {{Understanding Parameters of Deductive Verification: An Empirical Investigation of KeY}}, booktitle = {Proc.\ Int'l.\ Conf.\ Interactive Theorem Proving (ITP)}, organization = {Springer}, doi = {10.1007/978-3-642-29044-2}, ) @inproceedings(kuesters2011verifiability, author = {Ralf K{\"u}esters and Tomasz Truderung and Andreas Vogt}, year = {2011}, title = {{Verifiability, Privacy, and Coercion-resistance: New Insights From a Case Study}}, booktitle = {Proc.\ Symposium on Security and Privacy (SP)}, organization = {IEEE}, pages = {538--553}, doi = {10.1109/SP.2011.21}, ) @misc(LC06, author = {Gary T. Leavens and Yoonsik Cheon}, year = {2006}, title = {{Design by Contract with JML}}, url = {http://www.jmlspecs.org/jmldbc.pdf}, ) @inproceedings(LM:ICSE07, author = {Gary T. Leavens and Peter M\"uller}, year = {2007}, title = {{Information Hiding and Visibility in Interface Specifications}}, booktitle = {Proc.\ Int'l Conf.\ Software Engineering (ICSE)}, publisher = {IEEE}, address = {Washington, DC, USA}, pages = {385--395}, doi = {10.1109/ICSE.2007.44}, ) @article(leavens2006behavioral, author = {Gary T Leavens and David A Naumann}, year = {2006}, title = {Behavioral Subtyping is Equivalent to Modular Reasoning for Object-oriented Programs}, ) @book(LG86, author = {Barbara Liskov and John Guttag}, year = {1986}, title = {{Abstraction and Specification in Program Development}}, publisher = {MIT Press}, address = {Cambridge, MA, USA}, ) @article(LW:TOPLAS94, author = {Barbara H. Liskov and Jeannette M. Wing}, year = {1994}, title = {{A Behavioral Notion of Subtyping}}, journal = {ACM Trans.\ Programming Languages and Systems (TOPLAS)}, volume = {16}, number = {6}, pages = {1811--1841}, doi = {10.1145/197320.197383}, ) @article(marche2012jessie, author = {Claude March{\'e} and Yannick Moy}, year = {2012}, title = {{The Jessie Plugin for Deductive Verification in Frama-C}}, journal = {INRIA Saclay {\^I}le-de-France and LRI, CNRS UMR}, doi = {10.1.1.229.3233}, ) @book(M88, author = {Bertrand Meyer}, year = {1988}, title = {{Object-Oriented Software Construction}}, edition = {1st}, publisher = {Prentice-Hall, Inc.}, address = {Upper Saddle River, NJ, USA}, ) @article(M92, author = {Bertrand Meyer}, year = {1992}, title = {{Applying Design by Contract}}, journal = {IEEE Computer}, volume = {25}, number = {10}, pages = {40--51}, doi = {10.1109/2.161279}, ) @book(NWP02, author = {Tobias Nipkow and Markus Wenzel and Lawrence C. Paulson}, year = {2002}, title = {{Isabelle/HOL: A Proof Assistant for Higher-Order Logic}}, publisher = {Springer}, address = {Berlin, Heidelberg}, doi = {10.1007/3-540-45949-9}, ) @inproceedings(ORR+:CAV96, author = {Sam Owre and Sreeranga P. Rajan and John M. Rushby and Natarajan Shankar and Mandayam K. Srivas}, year = {1996}, title = {{PVS: Combining Specification, Proof Checking, and Model Checking}}, booktitle = {Proc.\ Int'l Conf.\ Computer Aided Verification (CAV)}, publisher = {Springer}, address = {Berlin, Heidelberg}, pages = {411--414}, doi = {10.1007/3-540-61474-5_91}, ) @article(pariente2010formal, author = {Dillon Pariente and Emmanuel Ledinot}, year = {2010}, title = {{Formal Verification of Industrial C Code using Frama-C: A Case Study}}, journal = {Proc.\ Int'l Conf.\ Formal Verification of Object-Oriented Software (FoVeOOS)}, pages = {205}, ) @inproceedings(polikarpova2015fully, author = {Nadia Polikarpova and Julian Tschannen and Carlo A Furia}, year = {2015}, title = {{A Fully Verified Container Library}}, booktitle = {Proc.\ Int'l Symposium Formal Methods (FM)}, organization = {Springer}, pages = {414--434}, doi = {10.1007/978-3-319-19249-9_26}, ) @article(RRDH06, author = {Robby and Edwin Rodr\'iguez and Matthew B. Dwyer and John Hatcliff}, year = {2006}, title = {{Checking JML Specifications Using an Extensible Software Model Checking Framework}}, journal = {Int'l J.\ Software Tools for Technology Transfer (STTT)}, volume = {8}, number = {3}, pages = {280--299}, doi = {10.1007/s10009-005-0218-5}, ) @book(rogers1967theory, author = {Hartley Rogers and H Rogers}, year = {1967}, title = {{Theory of Recursive Functions and Effective Computability}}, volume = {5}, publisher = {McGraw-Hill New York}, ) @incollection(R97, author = {John Rushby}, year = {1997}, title = {{Formal Methods and their role in the Certification of Critical Systems}}, booktitle = {Safety and Reliability of Software Based Systems}, publisher = {Springer}, pages = {1--42}, doi = {10.1007/978-1-4471-0921-1_1}, ) @book(SD88, author = {Donald Sannella}, year = {1988}, title = {{A Survey of Formal Software Development Methods}}, publisher = {University of Edinburgh, Department of Computer Science, Laboratory for Foundations of Computer Science}, ) @book(Sch01, author = {Johann Schumann}, year = {2001}, title = {{Automated Theorem Proving in Software Engineering}}, publisher = {Springer}, address = {Berlin, Heidelberg}, doi = {10.1007/978-3-662-22646-9}, ) @book(schumann2001automated, author = {Johann M Schumann}, year = {2001}, title = {{Automated Theorem Proving in Software Engineering}}, publisher = {Springer Science \& Business Media}, doi = {10.1007/978-3-662-22646-9}, ) @inproceedings(TSKA:VAST11, author = {Thomas Th\"{u}m and Ina Schaefer and Martin Kuhlemann and Sven Apel}, year = {2011}, title = {{Proof Composition for Deductive Verification of Software Product Lines}}, booktitle = {Proc.\ Int'l Workshop Variability-intensive Systems Testing, Validation and Verification (VAST)}, publisher = {IEEE}, address = {Washington, DC, USA}, pages = {270--277}, doi = {10.1109/ICSTW.2011.48}, ) @inproceedings(wampler2006contract4j, author = {Dean Wampler}, year = {2006}, title = {{Contract4J for Design by Contract in Java: Design Pattern-like Protocols and Aspect Interfaces}}, booktitle = {Fifth AOSD Workshop on ACP4IS}, pages = {27--30}, doi = {10.1.1.115.2281}, ) @misc(why, author = {{Why Development Team}}, title = {{Why: A Software Verification Platform}}, howpublished = {Website}, note = {Available online at \url{http://why.lri.fr/}}, )