Coq Formalization And Soundness Proof For An Input/Output Verification Approach

Software OPEN SOURCE
Penninckx, Willem; Jacobs, Bart;
(2016)
  • Publisher: Zenodo
  • Related identifiers: doi: 10.5281/zenodo.887578
  • Subject: Molecular Biology | Inorganic Chemistry | coq | soundness | Sociology | Physiology | input/output | Biochemistry | Cancer | verification
    • FOR: 80699 Information Systems not elsewhere classified | 69999 Biological Sciences not elsewhere classified
    acm: TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES | TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS

<p>This is a Coq formalization and soundness proof for an input/output verification approach. The proof rules do not support verifying nonterminating executions, although the step semantics support nonterminating runs.</p> <p>Coq version used: 8.4pl4</p> <p> </p... View more
Share - Bookmark

  • Download from
    Zenodo via Zenodo (Software, 2016)
    figshare via figshare (Software, 2016)
  • Funded by
  • Related to
    FET FP7-> FET Open: FET Young Explorers
    FET FP7-> FET Open: Architecture-driven verification of systems software
  • Cite this software