This project is read-only.

This page lists papers significant parts of which are directly related to VCC.

2015

  • Sumesh Divakaran: A Refinement-Based Methodology for Verifying Abstract Data Type Implementations. PhD Thesis, Indian Institute of Science, Bangalore, 2015.

2014

  • Ernie Cohen: Modular Verification of Hybrid System Code with VCC. arXiv:1403.3611 [cs.SE]
  • Mikhail Kovalev, G. Chen, Ernie Cohen: Store Buffer Reduction with MMUs. VSTTE 2014.
  • Ismail Kuru, Burku Ozkan, Suha Mutluergil, Serdar Tasiran, Tayfun Elmas, Ernie Cohen: Verifying Programs under Snapshot Isolation and Similar Relaxed Consistency Models. TRANSACT 2014.
  • Edgar Pek, Xiaokng Qiu, P. Madhusudan: Natural Proofs for Data Structure Manipulation in C using Separation Logic. PLDI 2014.
  • Sumesh Divakaran, Deepak D'Souza, Nigamanth Sridhar: Efficient Refinement Checking in VCC. In VSTTE 2014
  • François Dupressoir, Andrew Gordon, Jan Juriens, David Naumann: Guiding a general-purpose C verifier to prove cryptographic protocols. JCS  22 (2014), No.5, pp.823-866

2013

  • Ernie Cohen: Data Abstraction in VCC. In Engineering Dependable Systems, IOS Press 2013.
  • Wolfgang Paul, Sabina Schmaltz, Ernie Cohen : Theory of Multicore Hypervisor Verification.
    In SOFSEM 2013.
  • Sabina Schmaltz: Towards the Pervasive Formal Verification of Multi-Core Operating Systems and Hypervisors Implemented in C. PhD. Thesis, Univsitat des Saarlandes (2013).

2012

  • Eyad Alkassar, Ernie Cohen, Mikhail Kovalev, Wolfgang J. Paul: Verification of TLB Virtualization Implemented in C.
    In Verified Software: Theories, Tools, Experiments (VSTTE 2012), 2012. [BIB | PDF]

  • Jianqi Shi, Jifeng He, Huibiao Zhum Huixing Fang, Yanhong Huang, Xiaoxian Zhang:  ORIENTAIS: Formal Verified OSEK/VDX Real-Time Operating System.
    In 17th International Conference on Engineering of Complex Computer Systems (ICECCS), 2012

  • Nadia Polikarpova, Michał Moskal: Verifying implementations of security protocols by refinement.
    In Verified Software: Theories, Tools, Experiments (VSTTE 2012), 2012. [BIB | PDF]

  • Fazilatunnessa: Techniques for developing verified concurrent programs based on monitors and semaphores. Master's Thesis, Memorial University of Newfoundland, 2012.
  • Andrey Shadrin: Mixed low- and high level programming language semantics and automated verification of a small hypervisor. PhD. Thesis, Universitat des Saarlandes, 2012.
  • CWolfgang Paul, Sabine Schmaltz, Andrey Shadrin: Completing the Automated Verification of a Small Hypervisor - Assembler Code Verification. SEFM 2012.

2011

  • Eyad Alkassar, Sascha Böhme, Kurt Mehlhorn, Christine Rizkallah: Verification of Certifying Computations.
    In Computer Aided Verification (CAV 2011), 2011. [BIB | PDF]

  • Christoph Baumann, Holger Blasum, Thorsten Bormer, Sergey Tverdyshev: Proving Memory Separation in a Microkernel by Code Level Verification.
    In 1st International Workshop on Architectures and Applications for Mixed-Criticality Systems (AMICS 2011), 2011. [BIB | PDF]

  • Eyad Alkassar, Sascha Böhme, Kurt Mehlhorn, Christine Rizkallah, and Pascal Schweitzer: An Introduction to Certifying Algorithms.
    Information Technology: Vol. 53, No. 6

  • François Dupressoir, Andrew D. Gordon, Jan Jürjens, David A. Naumann: Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols.
    In Computer Security Foundations (CSF 2011), 2011. [BIB | PDF]

  • Claire Le Goues, K. Rustan M. Leino, Michał Moskal: The Boogie Verification Debugger.
    In Software Engineering and Formal Methods (SEFM 2011), 2011. [BIB | PDF]

  • Vladimir Klebanov, Peter Müller, Natarajan Shankar, Gary T. Leavens, Valentin Wüstholz, Eyad Alkassar, Rob Arthan, Derek Bronish, Rod Chapman, Ernie Cohen, Mark Hillebrand, Bart Jacobs, K. Rustan M. Leino, Rosemary Monahan, Frank Piessens, Nadia Polikarpova, Tom Ridge, Jan Smans, Stephan Tobies, Thomas Tuerk, Mattias Ulbrich, Benjamin Weiß: The 1st Verified Software Competition: Experience Report.
    In Formal Methods (FM 2011), 2011. [BIB]

2010

  • Eyad Alkassar, Ernie Cohen, Mark A. Hillebrand, Hristo Pentchev: Modular Specification and Verification of Interprocess Communication.
    In Formal Methods in Computer-Aided Design, 10th International Conference (FMCAD 2010), 2010. [BIB | PDF]

  • Eyad Alkassar, Ernie Cohen, Mark A. Hillebrand, Mikhail Kovalev, Wolfgang Paul: Verifying Shadow Page Table Algorithms.
    In Formal Methods in Computer-Aided Design, 10th International Conference (FMCAD 2010), 2010. [BIB | PDF]

  • Eyad Alkassar, Mark A. Hillebrand, Wolfgang Paul, Elena Petrova: Automated Verification of a Small Hypervisor.
    In Verified Software: Theories, Tools, Experiments (VSTTE 2010), 2010. [BIB | PDF]

  • Christoph Baumann, Bernhard Beckert, Holger Blasum, Thorsten Bormer: Ingredients of Operating System Correctness.
    In Embedded World 2010 Conference, 2010. [BIB | PDF]

  • Bernhard Beckert, Michał Moskal: Deductive Verification of System Software in the Verisoft XT Project.
    In Künstliche Intelligenz vol. 24(1), 2010. [BIB]

  • Sascha Böhme, Michał Moskal, Wolfram Schulte, Burkhart Wolff: HOL-Boogie: An Interactive Prover-Backend for the Verifiying C Compiler.
    In Journal of Automated Reasoning vol. 44(1--2), 2010. [BIB | PDF]

  • Ernie Cohen, Michał Moskal, Wolfram Schulte, Stephan Tobies: Local Verification of Global Invariants in Concurrent Programs.
    In Computer Aided Verification (CAV 2010), 2010. [BIB | PDF]

  • Ernie Cohen, Bert Schirmer: From Total Store Order to Sequential Consistency: A Practical Reduction Theorem.
    In Interactive Theorem Proving (ITP 2010), 2010. [BIB]

  • Dirk Leinenbach, Thomas Santen: Verifying the Microsoft Hyper-V Hypervisor with VCC.
    In 09381 Extended Abstracts Collection -- Refinement Based Methods for the Construction of Dependable Systems, 2010. [BIB]

  • S. F. M. De Sousa: Towards a Formally Verified Kernel Module.  INFORUM 2010.

2009

  • Christoph Baumann, Thorsten Bormer: Verifying the PikeOS Microkernel: First Results in the Verisoft XT Avionics Project.
    In Doctoral Symposium on Systems Software Verification (DS SSV 2009), 2009. [BIB | PDF]

  • Christoph Baumann, Bernhard Beckert, Holger Blasum, Thorsten Bormer: Better Avionics Software Reliability by Code Verification -- A Glance at Code Verification Methodology in the Verisoft XT Project.
    In Embedded World 2009 Conference, 2009. [BIB | PDF]

  • Christoph Baumann, Bernhard Beckert, Holger Blasum, Thorsten Bormer: Formal Verification of a Microkernel Used in Dependable Software Systems.
    In Computer Safety, Reliability, and Security (SAFECOMP 2009), 2009. [BIB | PDF]

  • Ernie Cohen, Norbert Schirmer: A Better Reduction Theorem for Store Buffers.
    Technical Report arXiv:0909.4637, arXiv, 2009. [BIB | PDF]

  • Ernie Cohen, Eyad Alkassar, Vladimir Boyarinov, Markus Dahlweid, Ulan Degenbaev, Mark Hillebrand, Bruno Langenstein, Dirk Leinenbach, Michał Moskal, Steven Obua, Wolfgang Paul, Hristo Pentchev, Elena Petrova, Thomas Santen, Norbert Schirmer, Sabine Schmaltz, Wolfram Schulte, Andrey Shadrin, Stephan Tobies, Alexandra Tsyban, Sergey Tverdyshev: Invariants, Modularity, and Rights.
    In Perspectives of Systems Informatics (PSI 2009), 2009. [BIB | PDF]

  • Ernie Cohen, Michał Moskal, Wolfram Schulte, Stephan Tobies: A Precise Yet Efficient Memory Model for C.
    In Workshop on Systems Software Verification (SSV 2009), 2009. [BIB | PDF]

  • Ernie Cohen, Markus Dahlweid, Mark Hillebrand, Dirk Leinenbach, Michał Moskal, Thomas Santen, Wolfram Schulte, Stephan Tobies: VCC: A Practical System for Verifying Concurrent C.
    In Theorem Proving in Higher Order Logics (TPHOLs 2009), 2009. [BIB | PDF]

  • Markus Dahlweid, Michał Moskal, Thomas Santen, Stephan Tobies, Wolfram Schulte: VCC: Contract-based Modular Verification of Concurrent C.
    In ICSE Companion 2009: 31st International Conference on Software Engineering, 2009. [BIB | PDF]

  • Mark A. Hillebrand, Dirk C. Leinenbach: Formal Verification of a Reader-Writer Lock Implementation in C.
    In Workshop on Systems Software Verification (SSV 2009), 2009. [BIB]

  • Dirk Leinenbach, Thomas Santen: Verifying the Microsoft Hyper-V Hypervisor with VCC.
    In Formal Methods (FM 2009), 2009. [BIB]

  • Ernie Cohen, Michał Moskal, Wolfram Schulte, Stephan Tobies: A Practical Verification Methodology for Concurrent Programs.
    Technical Report MSR-TR-2009-15, Microsoft Research, 2009. [BIB | PDF]

  • Uland Degenbaev, Wolfgang J. Paul, Norbert Schirmer: Pervasive Theorey of Memory. Fesschrift Mehlhorn, LNCS 5760 (2009).
  • Stefan Maus: Verification of Hypervisor Subroutines Written in Assembler. PsD. Thesis, Universitat Freiburg (2009).

2008

  • Sascha Böhme, Rustan Leino, Burkhart Wolff: HOL-Boogie -- An Interactive Prover for the Boogie Program Verifier.
    In Theorem Proving in Higher Order Logics (TPHOLs 2008), 2008. [BIB | PDF]

  • Stefan Maus, Michał Moskal, Wolfram Schulte: Vx86: x86 Assembler Simulated in C Powered by Automated Theorem Proving.
    In Algebraic Methodology and Software Technology (AMAST 2008), 2008. [BIB | PDF]

Last edited Mar 3, 2015 at 10:09 PM by erniecohen, version 19

Comments

No comments yet.