otrack

Spécification formelle assistée par l'IA pour les systèmes répartis

Le sujet de ce projet est inspiré du récent GenAI-accelerated TLA+ challenge organisé par la Fondation TLA+ [1]. Il vise à utiliser des outils assistés par l’IA pour la spécification formelle de systèmes répartis. L'objectif principal est de produire, valider et affiner des modèles formels de protocoles de réplication des données.

Contexte et Motivation

Les protocoles de réplication sont centraux dans les infrastructures informatiques modernes où ils assurent la haute disponibilité des données. Des exemples bien connus de protoocols de réplications sont Raft et Paxos.

otrack

package tsp.pacman;

import java.lang.Math;

class Position {

    int row, col;

    public Position(int row, int col) {
	this.row = row;

otrack

import java.util.function.Function;

// 1

interface F {int call(); }

class Q1 {
    public static void main(String[] args) {
	F a = () -> {return 42;};
	System.out.println(a instanceof F);

otrack

package tsp.ast;

class Add extends Operation {

    Add(Node left, Node right) {
	super(left, right);
    }

    @Override
    public int execute() {

otrack

#!/bin/sh
# setup.sh

MAX=1
PREFIX=semaphore_counter_

for r in cabine panier;
do
    for i in $(seq 1 1 ${MAX})
    do

otrack

class Monster {
    String name;
    int health;

    public static void main(String args[]) {
	Monster aMonster;
	for (int i=0; i<8; i++) {
	    aMonster = Pokedex.createMonster("Pikachu"+i, 0);
	    Pokedex.displayMonster(aMonster);	
	}

otrack

class Monster {
    String name;
    int health;

    public static void main(String args[]) {
	Monster aMonster;
	for (int i=0; i<8; i++) {
	    aMonster = Pokedex.createMonster("Pikachu"+i, 0);
	    Pokedex.displayMonster(aMonster);	
	}

otrack

#!/bin/bash

if [ -f arene.txt ];
then
    while read pid;
    do
	kill -USR1 $pid
    done < arene.txt
    rm arene.txt
else

otrack

#!/bin/bash

trap 'echo $$: Morituri te salutant; exit 0' USR1
trap ./cesar.sh INT TERM

if [ $# -ne 1 ]; then
    echo "Usage: $0 N"
    exit 1
fi

otrack

# Cassandra storage config YAML

# NOTE:
#   See https://cassandra.apache.org/doc/latest/configuration/ for
#   full explanations of configuration directives
# /NOTE

# The name of the cluster. This is mainly used to prevent machines in
# one logical cluster from joining another.