Module Linear

module Linear: sig .. end

References:

• Vafeiadis, V.: Automatically proving linearizability. In CAV 2010. Springer, Heidelberg (2010)
• Henzinger, T. A., Sezgin, A., Vafeiadis, V.: Aspect-oriented linearizability proofs. In CONCUR 2013. LNCS, vol. 8052. Springer, Heidelberg (August 2013)

val check_props : Assertions.prover ->
       Genarith.abstraction ->
       string list * Misc.StringSet.t * Exp.IdSet.t *
       (string, Tycheck.protocol_item) Hashtbl.t *
       (string, Tycheck.escrow_item) Hashtbl.t *
       (string, Commands.fun_info) Hashtbl.t *
       (Misc.component, Assertions.act list * Assertions.act list) Hashtbl.t *
       (Misc.component * Commands.res_init) list *
       (string * Commands.can_entailment) list -> bool

Configuration parameters & statistics

val verbose : int Pervasives.ref

val infer : int Pervasives.ref

val args : (Arg.key * Arg.spec * Arg.doc) list