PVS stands for People Verification System or Program Verification System. It is developed at CSL (Computer Science Laboratory) of SRI International

Like Coq or Isabelle, it is a proof assistant. It does not prove theorems automatically, but rather helps a user design coherent specifications, implement functions meeting those specifications, and prove theorems.

It is both a language and an inference system. The language is a typed higher order logic, featuring undecidable type checking.

One of the things I like about PVS is that type checking is undecidable. PVS will generate proof obligations (also called TCCs for Type Checking Conditions) from user theories, when it cannot fully type check these theories. PVS language is very flexible, as it allows the user write incoherent specifications or theories: unprovable TCCs will help the writer pin point mistakes, and gradually improve theories, without limiting user's creativity. This is a fruitful approach, very close to human reasoning. People, mathematicians, logicians do make mistakes: people need a tolerant framework, helping them find and correct their mistakes.

I like Coq too, for its elegance and minimality, but I have been raised with PVS, and know it better ...

IT304-IT305 Class: reserved to ENSEIRB-MATMECA IT304, IT305 GL students (you must connect and sign in with your Google identifier).