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 display is weird 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