kdrag.solvers.verus

Functions

install()

run_verus(args)

Classes

TransitionSystem(name, fields, init, ...)

class kdrag.solvers.verus.TransitionSystem(name: str, fields: list[z3.z3.ExprRef], init: tuple[str, z3.z3.BoolRef], transitions: tuple[str, z3.z3.BoolRef], invariants: dict[str, z3.z3.BoolRef] = <factory>)

Bases: object

Parameters:

  • name (str)

  • fields (list[ExprRef])

  • init (tuple[str, BoolRef])

  • transitions (tuple[str, BoolRef])

  • invariants (dict[str, BoolRef])

fields: list[ExprRef]
init: tuple[str, BoolRef]
invariants: dict[str, BoolRef]
name: str
transitions: tuple[str, BoolRef]
kdrag.solvers.verus.install()
kdrag.solvers.verus.run_verus(args: list[str]) → CompletedProcess
Parameters:

args (list[str])

Return type:

CompletedProcess