Resources

Proof obligations from the B formal method

The application of the B formal method and the Event-B system specification approach generates verification conditions that have to be proved to ensure the soundness of the produced artifacts: they are called proof obligations. Atelier B is an IDE that supports both the B method and Event B. In Atelier B, proof obligations are represented in an XML format called POG. CLEARSY contributes to the BLaSST project by collecting representative proof obligations and publishing those proof obligations once they have been anonymized: 681 285 proof obligations distributed in 5 431 files, weighing 6.

SMT-LIB 2.6 encoding of proof obligations from the B formal method

The application of the B formal method and the Event-B system specification approach generates verification conditions that have to be proved to ensure the soundness of the produced artifacts: they are called proof obligations. Atelier B is an IDE that supports both the B method and Event B. In Atelier B, proof obligations are represented in an XML format called POG. In order to be able to use modern automatic proof technologies, CLEARSY has developed a translator from the POG format to the SMT-LIB 2.

Tool to collect metrics on proof obligations

The application of the B formal method and the Event-B system specification approach generates verification conditions that have to be proved to ensure the soundness of the produced artifacts: they are called proof obligations. Atelier B is an IDE that supports both the B method and Event B. In Atelier B, proof obligations are represented in an XML format called POG. CLEARSY contributes to the BLaSST project by publishing pogmetrics, a software tool that collect miscellaneous metrics on POG files.