Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

Browse thread
[ANN] RegSTAB released
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2009-07-06 (09:34)
From: vincent aravantinos <vincent.aravantinos@y...>
Subject: [ANN] RegSTAB released

[Sorry for multiple post]

Dear list,
I am pleased to announce the first release of RegSTAB.

RegSTAB is a SAT-solver able to deal with formula schemas:
you can give it a scheme of formulas such as "/\i=1..n P_i -> P_i+1" (where n is a variable)
and it will be able to answer you if *all the formulas of this form (i.e. for every value of n) are unsatisfiable*.
i.e. it can treat at once an infinite set of propositional formulas.

Manual: manual
RegSTAB is based on a recent paper:

Vincent Aravantinos
PhD Student - LIG - CAPP Team
Grenoble, France