Protocol buffers are Google's language-neutral, platform-neutral, specification for data serialization. While Google provides implementations for a lot of languages, Elixir is not one of them. Protox is a pure Elixir implementation of Protocol Buffers: written using meta-programming, it provides very good performances and expose data with standard structures.
Network coding is a technique to improve network efficiency through the usage of redundancy packets to avoid retransmissions. Netcode is a library which implements network coding using Galois fields. It provides C bindings.
Model checkers are a category of tools that automatically explore all the states of a system, given a formal description, to verify properties (e.g. "Does my system have a deadlock?"). It's a memory and CPU intensive process, making C++ the right language. This tool features parsers for several Petri net formats, JSON and DOT export of results; it relies on the Boost libraries to provide portability.
This tool had the second place at the Model Checking Contest (2014 and 2015 editions). On all given systems' descriptions ("models"), it was the tool with the smallest memory footprint on 50% of models, and was the fastest on 75% of the models. All in all, it was the tool which was able to handle the maximum number of models.
This library is an implementation of the Hierarchical Set Decision Diagram (SDD) data structure. SDDs provide the ability to store arbitrary types, making this structure a generic one. C++ templates are a natural way of implementing SDDs, thus providing efficient and generic algorithms. It features a custom reference-counted garbage collector, which is required by the nature of decision diagrams, and a custom tagged union (like Boost.Variant) to provide a fast and safe visitor mechanism. Also, it uses type traits, whenever possible, to statically choose the best algorithms at compile time. Finally, great care is taken to allocate and use memory in a contiguous way to ensure caches are used at their best.
Model checking is a technique of verification which has the major advantage of being fully automatic. However, the model checking process exhaustively explores the states of the analyzed models. This causes a major problem: combinatorial explosion due to the state spaces of large systems, which can easily have more than 10100 states.
This thesis offers two types of solutions to address more effectively larger spaces of states. The first relies on the resources of parallel machines with multiple CPUs or multi-core and those of clusters, achieving linear speedups. The second solution deals with Hierarchical Set Decision Diagrams (an enhancement of the Binary Decision Diagrams) by automating and generalizing a technique called "saturation", whose empirically shown effectiveness (in orders of magnitude) is very difficult to achieve manually.
This degree is a specialization in "Distributed Systems Engineering". It covers topics such as: conception, modeling and formal verification of parallel and distributed systems; metamodeling; code generation; distributed algorithms.