Welcome to RegSTAB Home Page!

RegSTAB is a SAT-Solver able to deal with formulae patterns.

e.g. any SAT-Solver can tell you that each of the following formulae is unsatisfiable:

  • P1 Λ (P1 => P2) Λ ¬P2
  • P1 Λ (P1 => P2) Λ (P2 => P3) Λ ¬P3
  • P1 Λ (P1 => P2) Λ (P2 => P3) Λ (P3 => P4) Λ ¬P4
But RegSTAB can tell you directly that this is unsatisfiable for all n≥0:

P1 Λ Λi=1..n (Pi => Pi+1) Λ ¬Pn+1

This may be useful e.g. to prove circuit specifications independently of the number of bits.

(if you don't know logic click here :)


Download RegSTAB


Quickstart
Manual
Developper Documentation
Contact

Latest News

RegSTAB 2.0.0 released

Vincent Aravantinos - 2012-05-06 15:34 -

RegSTAB 1.4.6 released

Vincent Aravantinos - 2010-11-20 17:31 -

RegSTAB 1.4.4 released

Vincent Aravantinos - 2010-05-19 16:26 -

RegSTAB 1.4.2 released !

Vincent Aravantinos - 2009-12-09 19:26 -

RegSTAB 1.4

Vincent Aravantinos - 2009-09-29 07:41 -

RegSTAB new release

Vincent Aravantinos - 2009-08-17 18:02 -

RegSTAB first release

Vincent Aravantinos - 2009-07-06 10:33 -

 

 


Powered By GForge Collaborative Development Environment