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