NASA logo

+ Contact NASA



  • + HOME
  • + WELCOME
  • + QUICK PAGE
  • + PHILOSOPHY
  • + TEAM
  • + RESEARCH
  • + LINKS

  • PVSio

    PVSio is a PVS* package that extends the ground evaluator with a predefined library of imperative programming language features such as side effects, unbounded loops, input/output operations, floating point arithmetic, exception handling, pretty printing, and parsing. The PVSio input/output library is implemented via semantic attachments*.

    PVSio has been part of PVS since PVS 5.0 and is included in the latest release of PVS*. PVSio provides:

    Downloads

    Publications

    The tag [*] identifies links that are outside the NASA domain