LIPN - Paris North Computer Science Laboratory

sogMBT

2023

Symbolic Observation Graph-Based Generation of Test Paths

Jaime Arias, Mohamed Taha Bennani, Jörg Desel, Kais Klai, Hanène Ochi

PITPN2Maude

2023

Rewriting Logic Semantics for Parametric Time Petri Nets with Inhibitor Arcs

Jaime Arias, Kyungmin Bae, Laure Petrucci, Carlos Olarte, Peter Ölveczky, Fredrik Rømming

coq-num-analysis opam package (Numerical Analysis in Coq)

2022

Sylvie Boldo, François Clément, Martin Vincent, Micaela Mayero, Florian Faissole, Houda Mouhcine, Louise Leclerc, Stephane Aubry

Description

Formal developments and proofs in Coq of numerical analysis problems. This archive includes several Coq developments: - Lebesgue directory is about the Lebesgue Integration of Nonnegative Functions (see paper, paper, and report); - Lebesgue/bochner_integral directory is about the Bochner integral (see report); - LM directory is about the Lax–Milgram theorem (see paper, paper, and report); - Opam package coq-num-analysis: version 1.0 provides Lebesgue, and LM. - Lebesgue and LM are compiling in Coq 8.12 to 8.16.

PTA2Maude

2022

Rewriting Logic Semantics for Parametric Timed Automata

Jaime Arias, Kyungmin Bae, Laure Petrucci, Carlos Olarte, Peter Ölveczky, Fredrik Rømming

L-Framework

2022

Carlos Olarte, Elaine Pimentel, Camilo Rocha

Description

The L-Framework uses rewrite-based reasoning for proving crucial properties of sequent systems such as admissibility of structural rules, invertibility of rules and cut-elimination. Such procedures have been fully mechanized in Maude, achieving a great degree of automation when used on several sequent systems including intuitionistic and classical logics, linear logic, and normal modal logics.