Pinned Repositories
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
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_label
HIBOU implements a small-step operational semantics for labelled interaction models as well as a trace and multi-trace analysis algorithm
erwanM974's Repositories
erwanM974/autour_core
AUTOUR is a toolbox for manipulating various automata and regular expression formalisms
erwanM974/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.
erwanM974/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
erwanM974/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
erwanM974/hibou_label
HIBOU implements a small-step operational semantics for labelled interaction models as well as a trace and multi-trace analysis algorithm
erwanM974/autour_process
AUTOUR is a toolbox for manipulating various automata and regular expression formalisms
erwanM974/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.
erwanM974/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.
erwanM974/coq_toy_process_algebra
Example of a basic Coq proof for a property on a toy process algebra
erwanM974/erwanM974.github.io
erwanM974/graph_process_manager_core
Utilities to explore parts of a tree-like or graph-like structure that is not known in advance
erwanM974/graph_process_manager_loggers
Generic loggers for graph_process_manager_core
erwanM974/hibou_3sat_benchmark_experiment
A small experiment on the use of hibou_label to solve 3SAT instances via a reduction of the problem
erwanM974/hibou_hiding_usecases
Experiments on using a hiding-based algorithm for ORV from interactions
erwanM974/hibou_mqtt_benchmark_experiment
A small experiment on the use of hibou_label and hibou_efm to test an abstract client-broker mqtt system
erwanM974/graphviz_dot_builder
A simple library for generating dot files to obtain images of directed graphs with subgraphs/clusters.
erwanM974/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
erwanM974/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
erwanM974/hibou_nfa_generation
Experiments on generating NFA with reduced number of states from interaction diagrams
erwanM974/hibou_nfa_synthesis_benchmark
Experiments on comparing two methods for synthesizing NFA from interaction diagrams
erwanM974/hibou_nfa_trace_analysis
Experiments on using NFA generated from Interactions for global trace analysis
erwanM974/hibou_nfa_transformation_usecases_for_monitoring
Experiments on using a NFA monitor generation algorithm from interaction diagrams
erwanM974/hibou_nfagen_concrete_usecases
Applying an incremental method for synthesizing NFAs from Interactions to a few use cases from the literature
erwanM974/hibou_passing
HIBOU for typed message passing
erwanM974/hibou_sensor_partial_observation_experiment
A small experiment for comparing different algorithms implemented in hibou_label to recognize partially observed multi-traces (prefixes)
erwanM974/hibou_simulation_usecases_for_slice_recognition
Experiments on using a simulation-based algorithm for ORV from interactions
erwanM974/hibou_slice_recognition_experiment
A small experiment on the use of hibou_label to recognize slices of accepted multi-traces
erwanM974/hibou_trs_basic
Proof of convergence of a TRS for computing normal forms of interaction terms
erwanM974/hibou_trs_simplify_empty
Proof of convergence of a TRS for simplifying interaction terms
erwanM974/image_colored_text
A basic extension of the image/imageproc crates for writing multiline colored text