Projects
-
- ARC
The ARC model-checker syndicates developments on the two AltaRica based model-checkers Altatools and Mec 5.
Main features implemented in ARC are listed below:- Support of the AltaRica language with extension proposed during ACI Persee
- support for compound types (arrays, structures)
- definition of abstract types and signatures of functions
- Acheck specifications are supported using explicit or symbolic representation (however not all the set of commands are supported in both encoding)
- Mec 5 specifications with Decision Diagrams encoding. ARC extends the set of predefined sets with, for instance,
N!reachthat specifies the set of reachable configurations of the node N. - ARC integrates an small graphical simulator that replaces the old one implemented in Altatools
- Large relations can be serialized in binary files for future use.
- Preprocessors can be specified using the configuration file of ARC
- CTL* logic is supported in Acheck specs.
Go to the wiki page here.
- Support of the AltaRica language with extension proposed during ACI Persee
- ARsyntax
This library contains the parser for the AltaRica language. In fact it supports more than AltaRica because it recognize MEC 5 and Acheck specifications languages.
- CCL
This library gathers many routines used by several projects of the AltaRica forge.
- FASTer
FASTer is an extension of the well-known FAST tool originally developped at LSV laboratory at ENS Cachan.
FASTer is a tool dedicated to the analysis of infinite systems. It performs automatic verification of systems augmented with (unbounded) integer variables. The main issue addressed by FAST is the computation of the exact (infinite) set of configurations reachable from a given set of initial configurations. Although such sets are in general not computable, FAST uses a semi-algorithm which is expected to terminate in most practical cases. ...
- Mec 5
Mec 5 is a model-checker for finite AltaRica models, using a very expressive specification language (systems of fixpoint equations over finite relations with first-order quantifiers and equality testing).
- TALALIB
TAlence Linear Algebra Library
- AltaRica Models
A set of AltaRica models, with benchmarks scripts.
- AltaRica Benchs
A set of AltaRica benchs models.
- Public AltaRica Models
A set of public AltaRica models, with slides and scripts.
- Analysis of Concurrent Systems
This forge unites the outcome of our small workgroup around the analysis and verification of distributed, concurrent software systems. Our work tries to attack the verification of automata-based models by different paradigms and by transferring ideas from other research areas. In addition, we will also publish some of the libraries and tools we use to implement our ideas in this forge. Please refer to the appropriate pages of sub projects for detailed information. ...
- McScM
McScM (Model Checker for Systems of Communicating fifo Machines) is a small framework for implementing model checking algorithms in the context of infinite state systems of the form "finite control plus infinite data". The main constituent is the verify tool for the safety verification of distributed machines that communicate asynchronously via reliable fifo channels. The framework is implemented in Objective Caml and published under a BSD license....
- ProMcScM
Parser library for the (Pro)cess (Me)ta (La)anguate (PROMELA), that additionally enhances the basic language with constructs needed for McScM (unbounded channels, etc.). The library is implemented in Objective Caml and published under a BSD license....
Also available in: Atom