covenant - Intersection of CFLs


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