Layered verification approach

This verification example demonstrates a layered verification approach, where the functional properties of the program are verified via history-based reasoning (that is, recording the changes to a certain shared states as a process algebra).

General information

ID80
Articlenone
Back-endSilicon
LanguageJava
FeaturesArrays, Histories
Sources
Path to example filelayers/HistoryApplication.java
Date2017-06-19

Statistical information

Lines of code318 lines (comments not included)
Lines of specification96 lines (30.19% of the total)
Computation timeunknown

Example code

Note, verification may take a while and has a time-out of 20 seconds.