Eldarica Web Interface

Eldarica accepts Horn clauses in Prolog and SMT-LIB format, as well as programs in a C-like language, including the keywords:

• assert(condition): verify that a condition holds at this point in the program. (alternative syntax: static_assert(...))
• assume(condition): assume that a condition holds.
• atomic { stm1; stm2; ... }: execute a block of statements atomically. atomic { assume(!lock); lock=1; } will atomically check that lock has value 0, and then set the variable to 1.
• within (cond) { stm1; stm2; ... }: execute a block of statements (atomically) before cond expires. This corresponds to time invariants in Uppaal timed automata.
• thread <name> { ... }: statically declare a (singleton) thread.
• thread[<id-var>] <name> { ... }: statically declare an infinitely replicated thread.
• clock <name>, duration <name>: declare clocks or variables representing time periods.
• chan <name>: declare a binary (UPPAAL-style) communication channel, which can be used via chan_send and chan_receive.

For more information, see our Github page.