erwanm974 Goto Github PK

autour_core

AUTOUR is a toolbox for manipulating various automata and regular expression formalisms

autour_process

AUTOUR is a toolbox for manipulating various automata and regular expression formalisms

coq_hibou_label_equivalent_terms

Formal proof with the Coq theorem prover that elements of some equivalence classes defined over a formal language of interactions describing the behavior of distributed systems have the same semantics.

coq_hibou_label_multi_trace_analysis

Formal proof with the Coq theorem prover of the correctness of an oracle algorithm for offline analysis of distributed logs against interaction models

coq_hibou_label_semantics_equivalence

Formal proof with the Coq theorem prover of the equivalence of three semantics for a language describing the behavior of distributed systems.

coq_interaction_semantics_equivalence_with_coregions

Formal proof of the equivalence of a denotational and operational semantics for an interaction language with a concurrent region primitive which covers both interleaving and weak sequencing.

coq_toy_process_algebra

Example of a basic Coq proof for a property on a toy process algebra

erwanm974.github.io

graph_process_manager_core

Utilities to explore parts of a tree-like or graph-like structure that is not known in advance

graph_process_manager_loggers

Generic loggers for graph_process_manager_core

graphviz_dot_builder

A simple library for generating dot files to obtain images of directed graphs with subgraphs/clusters.

hibou_3sat_benchmark_experiment

A small experiment on the use of hibou_label to solve 3SAT instances via a reduction of the problem

hibou_efm

HIBOU EFM implements a small-step operational semantics for interaction models with data and time as well as a trace and multi-trace analysis algorithm

hibou_hiding_usecases

Experiments on using a hiding-based algorithm for ORV from interactions

hibou_label

HIBOU implements a small-step operational semantics for labelled interaction models as well as a trace and multi-trace analysis algorithm

hibou_lfrem_por_loc_graph_size_benchmark

Experimental evaluation of analysis graph size for multi-trace analysis using two techniques for partial order reduction and local analyses

hibou_lfrem_por_loc_time_benchmark

Experimental evaluation of analysis time for multi-trace analysis using two techniques for partial order reduction and local analyses

hibou_mqtt_benchmark_experiment

A small experiment on the use of hibou_label and hibou_efm to test an abstract client-broker mqtt system

hibou_nfa_generation

Experiments on generating NFA with reduced number of states from interaction diagrams

hibou_nfa_synthesis_benchmark

Experiments on comparing two methods for synthesizing NFA from interaction diagrams

hibou_nfa_trace_analysis

Experiments on using NFA generated from Interactions for global trace analysis

hibou_nfa_transformation_usecases_for_monitoring

Experiments on using a NFA monitor generation algorithm from interaction diagrams

hibou_nfagen_concrete_usecases

Applying an incremental method for synthesizing NFAs from Interactions to a few use cases from the literature

hibou_passing

HIBOU for typed message passing

hibou_sensor_partial_observation_experiment

A small experiment for comparing different algorithms implemented in hibou_label to recognize partially observed multi-traces (prefixes)

hibou_simulation_usecases_for_slice_recognition

Experiments on using a simulation-based algorithm for ORV from interactions

hibou_slice_recognition_experiment

A small experiment on the use of hibou_label to recognize slices of accepted multi-traces

hibou_trs_basic

Proof of convergence of a TRS for computing normal forms of interaction terms

hibou_trs_simplify_empty

Proof of convergence of a TRS for simplifying interaction terms

image_colored_text

A basic extension of the image/imageproc crates for writing multiline colored text