TRecS (Types for RECursion Schemes): Type-Based Model Checker for Higher-Order Recursion Schemes

TRecS is a model checker for higher-order recursion schemes, which takes a higher-order recursion scheme G and a (deterministic) trivial automaton A as input, and checks whether the (possibly infinite) tree generated by G is accepted by A. The model checking problem for higher-order recursion schemes has been shown to be decidable by Luke Ong in 2006, but its worst-case complexity is k-EXPTIME complete for order-k recursion schemes. TRecS is (to our knowledge) the first implementation of a higher-order model checker ever built. It uses a type-based model checking algorithm proposed by Kobayashi at PPDP 2009, and runs fast for many typical inputs, despite the huge worst-case complexity. Since the development of TRecS, it has been used as backends of program verification tools, like MoCHi, which is a sort of "software model checker" for ML, and EHMTT Verifier, which is also a verification tool for tree-generating functional programs. You can test TRecS through the web interface below. The technical background is found in:

Naoki Kobayashi, Model Checking Higher-Order Programs, JACM, 60(3), 2013.

Enter a recursion scheme and a specification in the box below, and press the "submit" button. Examples are given below. Currently, our model checker only accepts deterministic Buchi automata with a trivial acceptance condition.

You can test only small examples on this page. Consult us (Naoki Kobayashi) if you would like to get source programs of TRecS and run it on your machine.

%BEGING    /*** Rewring rules of a recursion scheme. Non-terminal must start with a capital letter. ***/
S -> F c.  /*** The non-terminal of the first rule is interpreted as the start symbol. ***/
F x -> a x (F (b x)).  /*** Unbounded names ("a", "b" in this rule) are interpreted as terminals. ***/
%ENDG

%BEGINA    /*** Transition rules of a Buchi tree automaton (where all the states are final). ***/
q0 a -> q0 q0. /*** The first state is interpreted as the initial state. **/
q0 b -> q1.
q1 b -> q1.
q0 c -> .
q1 c -> .
%ENDA

/* encoding of the following file accessing program.
  let rec f x = if * then close x else (read(x); f x)
  let y = open "foo" in
    f y
  The property to be checked is: File "foo" is accessed according to
  read* close.
*/
%BEGING    
S -> F d end.  
F x k -> br (close k) (read (F x k)).  
%ENDG

%BEGINA    
q0 br -> q0 q0. 
q1 br -> q1 q1.
q0 read -> q0.
q0 close -> q1.
q1 end -> .
%ENDA

/*** An example taken from POPL09 paper, which creates and accesses two files ***/
%BEGING
S -> Newr C1.
C1 x -> Neww (C2 x).
C2 x y -> F x y end.
F x y k -> br (Close x (Close y k)) (Read x (Write y (F x y k))).
I x y -> x y.
K x y -> y.
Newr k -> br (newr (k I)) (k K).
Neww k -> br (neww (k I)) (k K).
Close x k -> x close k.
Read x k -> x read k.
Write y k -> y write k.
%ENDG

%BEGINA
q0 br -> q0 q0.
qr br -> qr qr.
qw br -> qw qw.
qrw br -> qrw qrw.
q0 newr -> qr.
qr read -> qr.
qr close -> qc.
q0 neww -> qw.
qw write -> qw.
qw close -> qc.
qw newr -> qrw.
qr neww -> qrw.
qrw read -> qrw.
qrw write -> qrw.
qrw close -> qrw.
qc end ->.
q0 end ->.
qrw end ->.
%ENDA

/*** An example taken from POPL09 paper, which acquires and releases a lock. ***/
%BEGING
S -> br (New (F0 end)) (New (F1 end)).
F0 k x -> C0 x k.
F1 k x -> Lock x (C1 x k).
C0 x k -> k.
C1 x k -> Unlock x k.
New k -> br (newl (k I)) (k K).
I x y -> x y.
K x y -> y.
Lock x k -> x lock k.
Unlock x k -> x unlock k.
%ENDG

%BEGINA
q0 br -> q0 q0.
q1 br -> q1 q1.
q2 br -> q2 q2.
q0 newl -> q1.
q1 lock -> q2.
q2 unlock -> q1.
q0 end -> .
q1 end -> .
%ENDA

  _case n i e1 ... en

%BEGING
S -> br (New (C 0)) (New (C 1)).
C b x -> F b x (G b x end).
F b x k -> _case 2 b k (Lock x k).  
G b x k -> _case 2 b k (Unlock x k).
New k -> br (newl (k I)) (k K).
I x y -> x y.
K x y -> y.
Lock x k -> x lock k.
Unlock x k -> x unlock k.
%ENDG
%BEGINA
q0 br -> q0 q0.
q1 br -> q1 q1.
q2 br -> q2 q2.
q0 newl -> q1.
q1 lock -> q2.
q2 unlock -> q1.
q0 end -> .
q1 end -> .
%ENDA

Example 5

/* HORS obtained by abstracting the following program with predicate even
fun repeat n f x = if n=0 then x else repeat (n-1) f (f x)
fun main( ) = if even(n) then assert(repeat n not true)
                     else ( ) 
*/
%BEGING
S -> If NB (Repeat True Not True Assert) end.
Repeat b f x k -> If b (C b f x NB k)  (C b f x False k).
C b f x b1 k -> If b1 (k x) (Repeat (Not b) f (f x) k).
Assert b -> b end fail.
If b x y -> b x y.
Not b x y -> b y x. 
NB x y -> br x y.    
True x y -> x.     
False x y -> y.
%ENDG
%BEGINA
q0 br -> q0 q0.
q0 end -> .
%ENDA

Example 6

/** HORS obtained by CPS conversion of the following call-by-value program.
let rec repeatEven f x = if * then x else f (repeatOdd f x)
and repeatOdd f x = f (repeatEven f x) 
let main( ) = if (repeatEven not true) then ( ) else fail
**/
%BEGING
Main -> RepeatEven C Not True.
RepeatEven k f x -> If TF (k x) (RepeatOdd (f k) f x).
RepeatOdd k f x -> RepeatEven (f k) f x.
C b -> If b end fail.
Not k b -> If b (k False) (k True).
If b x y -> b x y.
True x y -> x.      
False x y -> y.
TF x y -> br x y.
%ENDG
%BEGINA
q0 br -> q0 q0.
q0 end -> .
%ENDA

Loop program

/** HORS obtained by CPS conversion of the following call-by-value program.
let rec loop x = if x then loop x else x 
let f x = fail
let main () = f (loop true)
**/
%BEGING
S -> Loop True G.
Loop x k -> If x (Loop x k) (k x).
F x k -> fail.
Id x -> x.
G r -> F r Id.
If b x y -> b x y.
True x y -> x.      
False x y -> y.
%ENDG
%BEGINA
q0 br -> q0 q0.
q0 end -> .
%ENDA

Fibonacci words

%BEGING
S -> Fib b a.
Fib x y -> br (x e) (Fib y (Concat y x)).
Concat x y z -> x(y z).
%ENDG
%BEGINA
q0 br -> q0 q0.
q1 br -> q1 q1.
q0 a -> q0.
q0 b -> q1.
q1 a -> q0.
q0 e -> .
q1 e -> .
%ENDA