Module functions 

Auto-generated module

🤖 Generated with SplitRS

Functions

abstract_domain_ty

AbstractDomain: predicate abstraction / interval / octagon domain

abstract_states_ty

abstract_states: map concrete states to abstract domain

abstract_transformer_ty

AbstractTransformer: postτ

ag_decomposition_ty

ag_decomposition: decompose a verification task using A-G reasoning ag_decomposition : KripkeStructure → AssumeGuaranteeContract → Bool

alc_concept_ty

ALC: the description logic ALC (attribute language with complement)

alternating_turing_machine_ty

AlternatingTuringMachine: ATM used in alternation-based μ-calculus model checking

ample_set_ty

AmpleSet: an ample set satisfying C0–C3 for POR AmpleSet : KripkeStructure → State → Set (State → State) → Prop

app

app2

app3

arrow

assume_guarantee_contract_ty

AssumeGuaranteeContract: an AG specification (A, G)

atomic_proposition_ty

AtomicProposition: boolean-valued proposition on states

bdd_manager_ty

BDDManager: unique table + apply cache

bdd_ty

BDD: Binary Decision Diagram node

bool_ty

bounded_mc_query_ty

BoundedMCQuery: a bounded model checking problem (BMC) BoundedMCQuery : KripkeStructure → LtlFormula → Nat → Bool

buchi_automaton_ty

BuchiAutomaton: (Q, Σ, δ, q_0, F) ω-automaton

build_env

Register all model checking axioms into the kernel environment.

bvar

cegar_ty

CounterExampleGuidedRefinement: CEGAR loop

check_ctl_ty

check_ctl: check whether K ⊨ φ (CTL)

check_feasibility_ty

check_feasibility: determine if a counterexample is spurious

check_ltl_ty

check_ltl: check whether K ⊨ φ (LTL)

check_mu_ty

check_mu: model check a μ-calculus formula check_mu : KripkeStructure → MuFormula → Bool

check_pctl_ty

check_pctl: check whether M ⊨ φ (PCTL) check_pctl : ProbabilisticKripke → PCTLFormula → Bool

check_psl_ty

check_psl: check a PSL formula against a Kripke structure check_psl : KripkeStructure → PSLFormula → Bool

check_pushdown_ltl_ty

check_pushdown_ltl: model check a pushdown system against an LTL formula check_pushdown_ltl : PushdownSystem → LtlFormula → Bool

check_tctl_ty

check_tctl: verify a timed CTL formula over a timed automaton check_tctl : TimedAutomaton → TCTLFormula → Bool

compute_scc_ty

compute_scc: Tarjan’s SCC decomposition

context_free_ltl_ty

ContextFreeLTL: an LTL formula interpreted over pushdown system runs

counter_example_ty

CounterExample: trace witnessing formula violation

craig_interpolant_ty

CraigInterpolant: a formula I with A ⊨ I and I ∧ B unsatisfiable CraigInterpolant : LtlFormula → LtlFormula → LtlFormula → Prop

cst

ctl_formula_ty

CTL formula type

ctl_model_checker_ty

CtlModelChecker: fixpoint computation for CTL

ctl_star_formula_ty

CTL* formula type

find_counterexample_ty

find_counterexample: produce a counterexample trace if formula fails

flow_condition_ty

FlowCondition: ODE describing continuous evolution in a mode FlowCondition : Type → Prop

guard_region_ty

GuardRegion: a polyhedral region enabling a discrete transition GuardRegion : Type → Prop

hors_model_checking_ty

HORSModelChecking: model check a HORS against an MSO property HORSModelChecking : HigherOrderRecursionScheme → MuFormula → Bool

hors_ty

HigherOrderRecursionScheme: a HORS defining a tree language

hybrid_automaton_ty

HybridAutomaton: automaton with continuous flow conditions

hybrid_reachability_ty

HybridReachability: reachable set of a hybrid system HybridReachability : HybridAutomaton → Set Type

image_ty

image: compute the forward image of a set of states

impl_pi

interface_verification_ty

interface_verification: check compatibility of component interfaces interface_verification : List AssumeGuaranteeContract → Bool

is_connected_ty

is_connected: every state is reachable from some initial state

k_induction_check_ty

k_induction_check: run k-induction for LTL safety properties k_induction_check : KripkeStructure → LtlFormula → Nat → KInductionResult

k_induction_result_ty

KInductionResult: result of a k-induction proof step

kripke_structure_ty

KripkeStructure: (S, S_0, R, L)

lazy_cegar_ty

lazy_cegar: CEGAR with lazy abstraction refinement lazy_cegar : KripkeStructure → LtlFormula → Bool

ltl_formula_ty

LTL formula type

ltl_is_fairness_ty

ltl_is_fairness: φ is a fairness constraint

ltl_is_liveness_ty

ltl_is_liveness: φ is a liveness property

ltl_is_safety_ty

ltl_is_safety: φ is a safety property

ltl_model_checker_ty

LtlModelChecker: automaton-theoretic LTL checking

mazurkiewicz_trace_ty

MazurkiewiczTrace: an equivalence class of runs under independence

mu_calculus_parity_reduction_ty

mu_calculus_parity_reduction: reduction of μ-calc. to parity games mu_calculus_parity_reduction : MuFormula → ParityGame

mu_fixpoint_ty

mu_fixpoint: the least fixpoint operator μX.φ(X) mu_fixpoint : (State → Prop) → (State → Prop)

mu_formula_ty

MuFormula: a μ-calculus formula type

nat_ty

nu_fixpoint_ty

nu_fixpoint: the greatest fixpoint operator νX.φ(X) nu_fixpoint : (State → Prop) → (State → Prop)

parity_condition_ty

ParityCondition: ω-winning condition: the highest priority seen inf-often is even ParityCondition : (Nat → Bool) → Prop

parity_game_ty

ParityGame: a game graph with priority function

parity_game_winner_ty

parity_game_winner: which player wins from a given vertex? parity_game_winner : ParityGame → Nat → Bool

pctl_formula_ty

PCTLFormula: a PCTL (probabilistic CTL) formula type

persistent_set_ty

PersistentSet: a persistent set for partial order reduction PersistentSet : KripkeStructure → State → Set (State → State) → Prop

pi

por_reduction_ty

por_reduction: apply partial order reduction to a Kripke structure por_reduction : KripkeStructure → KripkeStructure

pre_image_ty

pre_image: compute the backward image of a set of states

probabilistic_kripke_ty

ProbabilisticKripke: a Markov Decision Process / Markov chain

prop

psl_formula_ty

PSLFormula: a PSL (Property Specification Language) formula

pushdown_reachability_ty

pushdown_reachability: backwards reachability in a pushdown system pushdown_reachability : PushdownSystem → Set State

pushdown_system_ty

PushdownSystem: a recursive program modeled as a pushdown automaton

reachability_probability_ty

reachability_probability: P[reach(T) from s] in a Markov chain reachability_probability : ProbabilisticKripke → State → Set State → Real

reachable_states_ty

reachable_states: the set of states reachable from initial states

refine_abstraction_ty

refine_abstraction: refine abstract domain using a spurious counterexample

sat_solver_ty

SatSolver: a SAT/SMT oracle used in bounded model checking

spurious_counterexample_ty

SpuriousCounterexample: infeasible concrete path

state_label_ty

StateLabel: set of atomic propositions true in a state

sva_formula_ty

SVAFormula: a SystemVerilog assertion formula

symbolic_transition_relation_ty

SymbolicTransitionRelation: T(s,s’) as BDD

tctl_formula_ty

TCTLFormula: a timed CTL formula

temporal_logic_pattern_ty

TemporalLogicPattern: a reusable specification pattern (Dwyer patterns)

timed_automaton_ty

TimedAutomaton: automaton with clock variables

type0

zielonka_solver_ty

ZielonkaSolver: Zielonka’s recursive parity game algorithm ZielonkaSolver : ParityGame → Bool

zone_graph_ty

ZoneGraph: zone-based abstract state space for timed systems

zone_reachability_ty

zone_reachability: compute the reachable zone graph of a timed automaton zone_reachability : TimedAutomaton → ZoneGraph