Automatic Certification of Java Source Code in Rewriting Logic

Java program and JML specification of safety policy

Selected program
ExampleEvenOdd2p1.java ExampleNonInterference23.java ExampleNoninterference9.java ExampleEvenOdd2p3.java ExampleNoninterference7.java ExampleNoninterference3.java ExampleNoninterferenceA.java ExampleNoninterferenceJMLerror3.java ExampleEvenOdd3p2.java ExampleEven2p5.java ExampleNoninterference8.java ExampleNoninterferenceJMLerror4.java ExampleNoninterferenceJMLerror1.java ExampleNoninterference0.java ExampleNoninterferenceC.java ExampleEvenOdd2.java ExampleNoninterference2.java ExampleNoninterferenceH.java ExampleNoninterferenceG.java ExampleEvenOdd2p4.java ExampleNoninterferenceF.java ExampleNoninterferenceJMLerror2.java ExampleNoninterference4p1.java ExampleNoninterference5.java ExampleNoninterferenceD.java ExampleNonInterference15.java ExampleNonInterference16.java ExampleNoninterference4.java ExampleNoninterferenceB.java ExampleEvenOdd1.java ExampleEvenOdd3.java ExampleNoninterference6.java ExampleEven2p2.java
Load from disk

Java code (from )
/* -- empty -- */ not selected

Verification & Certification

Select method:
-- --


Select safety property:
Int. arithmetics Non Interference


Verification only
With reduced label certificate
With reduced rules certificate
With full certificate