@inproceedings(DBLP:conf/cav/AlkassarBMR11, author = "Eyad Alkassar and Sascha B{\"o}hme and Kurt Mehlhorn and Christine Rizkallah", year = "2011", title = "Verification of Certifying Computations", editor = "Ganesh Gopalakrishnan and Shaz Qadeer", booktitle = "CAV", series = "LNCS 6806", publisher = "Springer", pages = "67--82", doi = "10.1007/978-3-642-22110-1\_7", ) @incollection(AlkassarEtAl2010, author = "Eyad Alkassar and Mark Hillebrand and Wolfgang Paul and Elena Petrova", year = "2010", title = "Automated Verification of a Small Hypervisor", booktitle = "Verified Software: Theories, Tools, Experiments", series = "LNCS", volume = "6217", publisher = "Springer", pages = "40--54", doi = "10.1007/978-3-642-15057-9\_3", ) @inproceedings(barnett05specsharp, author = "Mike Barnett and K. Rustan M. Leino and Wolfram Schulte", year = "2005", title = "The {Spec\#} Programming System: An Overview", booktitle = "Construction and Analysis of Safe, Secure, and Interoperable Smart Devices (CASSIS), International Workshop, 2004, Marseille, France, Revised Selected Papers", series = "LNCS 3362", publisher = "Springer", pages = "49--69", doi = "10.1007/978-3-540-30569-9\_3", ) @inproceedings(BaumannBlasumBormerTverdyshev2011, author = "C. Baumann and H. Blasum and T. Bormer and S. Tverdyshev", year = "2011", title = "{Proving Memory Separation in a Microkernel by Code Level Verification}", editor = "Wilfried Steiner and Roman Obermaisser", booktitle = "{1st International Workshop on Architectures and Applications for Mixed-Criticality Systems (AMICS 2011)}", publisher = "IEEE Computer Society", address = "Newport Beach, CA, USA", doi = "10.1109/ISORCW.2011.14", ) @inproceedings(BaumannBeckertBlasumBormer2009b, author = "Christoph Baumann and Bernhard Beckert and Holger Blasum and Thorsten Bormer", year = "2009", title = "{Formal Verification of a Microkernel Used in Dependable Software Systems}", editor = "Bettina Buth and Gerd Rabe and Till Seyfarth", booktitle = "{SAFECOMP'09}", series = "{LNCS 5775}", publisher = "Springer", pages = "187--200", doi = "10.1007/978-3-642-04468-7\_16", ) @inproceedings(BaumannBeckertEA2010, author = "Christoph Baumann and Bernhard Beckert and Holger Blasum and Thorsten Bormer", year = "2010", title = "{Ingredients of Operating System Correctness}", booktitle = "{Proceedings, embedded world 2010 Conference, Nuremberg, Germany}", note = "Available at \url {http://formal.iti.kit.edu/beckert/pub/embeddedworld2010.pdf}", ) @incollection(BeckertBormerKlebanov2010, author = "Bernhard Beckert and Thorsten Bormer and Vladimir Klebanov", year = "2012", title = "Improving the Usability of Specification Languages and Methods for Annotation-Based Verification", editor = "Bernhard Aichernig and Frank de Boer and Marcello Bonsangue", booktitle = "Formal Methods for Components and Objects", series = "LNCS", volume = "6957", pages = "61--79", doi = "10.1007/978-3-642-25271-6\_4", ) @inproceedings(BeckertBormerMerzSinz2011, author = "Bernhard Beckert and Thorsten Bormer and Florian Merz and Carsten Sinz", year = "2011", title = "Integration of Bounded Model Checking and Deductive Verification", booktitle = "FoVeOOS'11", pages = "86--104", doi = "10.1007/978-3-642-31762-0\_7", ) @book(KeYBook2007, editor = "Bernhard Beckert and Reiner H\"ahnle and Peter H. Schmitt", year = "2007", title = "Verification of Object-Oriented Software: The {KeY} Approach", series = "LNCS 4334", publisher = "Springer-Verlag", doi = "10.1007/978-3-540-69061-0", ) @inproceedings(Bianculli:2012:SPR:2337223.2337341, author = "Domenico Bianculli and Carlo Ghezzi and Cesare Pautasso and Patrick Senti", year = "2012", title = "Specification patterns from research to industry: a case study in service-based applications", booktitle = "Proceedings of the 2012 International Conference on Software Engineering", series = "ICSE 2012", publisher = "IEEE Press", address = "Piscataway, NJ, USA", pages = "968--976", doi = "10.1109/ICSE.2012.6227125", ) @inproceedings(Bohme:2008:HIP:1459784.1459802, author = "Sascha B\"{o}hme and K. Rustan Leino and Burkhart Wolff", year = "2008", title = "HOL-Boogie -- An Interactive Prover for the Boogie Program-Verifier", booktitle = "Proc., 21st Int. Conf. on Theorem Proving in Higher Order Logics", publisher = "Springer", pages = "150--166", doi = "10.1007/978-3-540-71067-7\_15", ) @inproceedings(COSTCompetition2011, author = "Thorsten Bormer and Marc Brockschmidt and Dino Distefano and Gidon Ernst and Jean-Christophe Filli{\^a}tre and Radu Grigore and Marieke Huisman and Vladimir Klebanov and Claude March{\'e} and Rosemary Monahan and Wojciech Mostowski and Nadia Polikarpova and Christoph Scheben and Gerhard Schellhorn and Bogdan Tofan and Julian Tschannen and Mattias Ulbrich", year = "2011", title = "The COST IC0701 Verification Competition 2011", booktitle = "FoVeOOS'11", pages = "3--21", doi = "10.1007/978-3-642-31762-0\_2", ) @inproceedings(Cohen:TPHOLs2009-23, 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 = "Theorem Proving in Higher Order Logics (TPHOLs)", series = "Lecture Notes in Computer Science", volume = "5674", publisher = "Springer", pages = "23--42", doi = "10.1007/978-3-642-03359-9\_2", ) @techreport(DeLine-Leino05, author = "Rob DeLine and K. Rustan M. Leino", year = "2005", title = "{BoogiePL}: A Typed Procedural Language for Checking Object-oriented Programs", type = "Technical Report", number = "MSR-TR-2005-70", institution = "Microsoft Research", url = "ftp://ftp.research.microsoft.com/pub/tr/TR-2005-70.pdf", ) @incollection(FilliatreM04, author = "Jean-Christophe Filli\^{a}tre and Claude March\'{e}", year = "2004", title = "Multi-prover Verification of {C} Programs", booktitle = "Formal Methods and Software Engineering", series = "LNCS 3308", publisher = "Springer", pages = "15--29", doi = "10.1007/978-3-540-30482-1\_10", ) @inproceedings(Goldstein2007, author = "M. Goldstein and Y.A. Feldman and S. Tyszberowicz", year = "2006", title = "Refactoring with contracts", booktitle = "Agile Conference, 2006", pages = "10 pp. --64", doi = "10.1109/AGILE.2006.44", ) @mastersthesis(GrebingDA2012, author = "Sarah Grebing", year = "2012", title = "Evaluating and Improving the Usability of Interactive Verification Systems", type = "Diploma thesis", school = "Universit\"{a}t Koblenz-Landau", ) @mastersthesis(Hull2010, author = "Ian Hull", year = "2010", title = "{Automated Refactoring of Java Contracts}", school = "University College Dublin", ) @inproceedings(Kaiser2007evolution, author = "Robert Kaiser and Stephan Wagner", year = "2007", title = "Evolution of the {PikeOS} Microkernel", editor = "Ihor Kuz and Stefan M Petters", booktitle = "MIKES: 1st International Workshop on Microkernels for Embedded Systems", ) @article(Klein_EHACDEEKNSTW_10, author = "Gerwin Klein and June Andronick and Kevin Elphinstone and Gernot Heiser and David Cock and Philip Derrin and Dhammika Elkaduwe and Kai Engelhardt and Rafal Kolanski and Michael Norrish and Thomas Sewell and Harvey Tuch and Simon Winwood", year = "2010", title = "{seL4}: Formal Verification of an Operating System Kernel", journal = "Communications of the ACM", volume = "53", number = "6", pages = "107--115", doi = "10.1145/1743546.1743574", ) @incollection(springerlink:10.1007/978-3-642-05089-3_51, author = "Dirk Leinenbach and Thomas Santen", year = "2009", title = "Verifying the Microsoft Hyper-V Hypervisor with VCC", editor = "Ana Cavalcanti and Dennis Dams", booktitle = "FM 2009: Formal Methods", series = "Lecture Notes in Computer Science", volume = "5850", publisher = "Springer Berlin / Heidelberg", pages = "806--809", doi = "10.1007/978-3-642-05089-3\_51", ) @inproceedings(Maus08vx86, author = "Stefan Maus and Micha{\l } Moskal and Wolfram Schulte", year = "2008", title = "Vx86: x86 assembler simulated in C powered by automated theorem proving", booktitle = "12TH International Conference on Algebraic Methodology and Technology (AMAST 2008)", series = "LNCS", volume = "5140", doi = "10.1007/978-3-540-79980-1\_22", ) @inproceedings(moura08z3, author = "Leonardo de Moura and Nikolaj Bj{\o }rner", year = "2008", title = "{Z3}: {A}n Efficient {SMT} Solver", booktitle = "Proc., 14th Int.\ Conf.\ on Tools and Algorithms for the Construction and Analysis of Systems, Budapest, Hungary", series = "LNCS 4963", publisher = "Springer", pages = "337--340", doi = "10.1007/978-3-540-78800-3\_24", ) @book(DO-178B, author = "{RTCA SC-167 / EUROCAE WG-12}", year = "1992", title = "DO-178B: Software Considerations in Airborne Systems and Equipment Certification", publisher = "Radio Technical Commission for Aeronautics (RTCA), Inc., 1828 L St. NW., Suite 805, Washington, D.C. 20036", ) @phdthesis(Sh12, author = "Andrey Shadrin", year = "2012", title = "Mixed Low- and High Level Programming Language Semantics and Automated Verification of a Small Hypervisor", school = "Saarland University, Saarbrücken", url = "http://www-wjp.cs.uni-saarland.de/publikationen/Sh12.pdf", ) @inproceedings(SFM2010aprecisememorymodel, author = "Carsten Sinz and Stephan Falke and Florian Merz", year = "2010", title = "A Precise Memory Model for Low-Level Bounded Model Checking", booktitle = "SSV'10", ) @misc(Tobies2011, author = "Stephan Tobies", title = "The Hyper-V Verification Experiment", note = "Presentation slides available at \url {http://research.microsoft.com/en-us/um/redmond/events/ss2011/slides/friday/stephan_tobies.pdf}", )