covenant is a tool for testing emptiness of a set of context free languages (CFLs). Since this problem is undecidable, covenant implements a CEGAR-based schema which might not terminate. The main novelty is a complete refinement procedure for regular separable CFLs.
covenant takes input from stdin. An example is:
; this is a comment ( S1 -> [ A B]; A -> [ \x61 \x61]; A -> [ \x62 \x62]; A -> [ \x61 S1 \x61, \x62 S1 \x62 ]; B -> [ \x61 \x62 B]; B -> [ \x61 \x62] ) ( S2 -> [ A B]; A -> [ \x61 \x61]; A -> [ \x62 \x62]; A -> [ \x61 S2 \x61, \x62 S2 \x62 ]; B -> [ \x62 \x61 B]; B -> [ \x62 \x61] )
The non-terminal symbol appearing on the left-hand side in the first grammar production is considered the start symbol of the grammar. In the above example the start symbols are S1 and S2, respectively.
A current limitation is that terminal symbols can only ranges from 0 to 127 and they must be described in hexadecimal format. E.g., \x61 is the ASCII character "a", \x62 is "b", and so on.
Click here for a 64-bit Linux/x86 binary and some instances. Many thanks to Georgel Calin for providing instances from safety verification of concurrent programs.
Type "covenant --help"
Jorge A. Navas