Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

ready for release 1.4

  • Loading branch information...
commit 6438fdb3e1bd291a81d2ff88c06d3ae8e338c8d7 1 parent 6bab635
@LeventErkok authored
View
9 README
@@ -1,8 +1,7 @@
-SBV: Symbolic Bit Vectors in Haskell
-====================================
+SBV: SMT Based Verification
+============================
-Express properties about bit-precise Haskell programs and automatically prove
-them using SMT solvers.
+Express properties about Haskell programs and automatically prove them using SMT solvers.
```haskell
$ ghci -XScopedTypeVariables
@@ -130,5 +129,5 @@ the [BSD3](http://en.wikipedia.org/wiki/BSD_licenses) verbiage.
Thanks
======
The following people reported bugs, provided comments/feedback, or contributed to the development of SBV in various ways:
-Ian Blumenfeld, Ian Calvert, Iavor Diatchki, Tom Hawkins, Lee Pike, Austin Seipp, Don Stewart, Josef Svenningsson,
+Ian Blumenfeld, Ian Calvert, Iavor Diatchki, John Erickson, Tom Hawkins, Lee Pike, Austin Seipp, Don Stewart, Josef Svenningsson,
and Nis Wegmann.
View
9 RELEASENOTES
@@ -1,10 +1,10 @@
Hackage: <http://hackage.haskell.org/package/sbv>
GitHub: <http://github.com/LeventErkok/sbv>
-Latest Hackage released version: 1.3
+Latest Hackage released version: 1.4
======================================================================
-Version 1.4, Not yet released
+Version 1.4, 2012-05-10
The major change in this release is the support for symbolic algebraic reals: SReal.
See http://en.wikipedia.org/wiki/Algebraic_number for details. In brief, algebraic
@@ -25,6 +25,11 @@ Version 1.4, Not yet released
should be printed. The default number of decimal digits to print is 10. (See the
'printRealPrec' field of SMT-solver configuration.)
+ The acronym SBV used to stand for Symbolic Bit Vectors. However, SBV has grown beyond
+ bit-vectors, especially with the addition of support for SInteger and SReal types and
+ other code-generation utilities. Therefore, "SMT Based Verification" is now a better fit
+ for the expansion of the acronym SBV.
+
Other notable changes in the library:
* Add functions s[TYPE] and s[TYPE]s for each symbolic type we support (i.e.,
sBool, sBools, sWord8, sWord8s, etc.), to create symbolic variables of the
View
2  SBVUnitTest/SBVUnitTestBuildTime.hs
@@ -2,4 +2,4 @@
module SBVUnitTestBuildTime (buildTime) where
buildTime :: String
-buildTime = "Wed May 9 20:42:42 PDT 2012"
+buildTime = "Wed May 9 22:17:47 PDT 2012"
View
14 sbv.cabal
@@ -1,11 +1,11 @@
Name: sbv
Version: 1.4
Category: Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math, SMT
-Synopsis: Symbolic bit vectors: Bit-precise verification and automatic C-code generation.
-Description: Express properties about bit-precise Haskell programs and automatically prove
- them using SMT solvers. Automatically generate C programs from Haskell functions.
- The SBV library adds support for symbolic bit vectors, allowing formal models of
- bit-precise programs to be created.
+Synopsis: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.
+Description: Express properties about Haskell programs and automatically prove them using SMT
+ (Satisfiability Modulo Theories) solvers. Automatically generate C programs from
+ Haskell functions. The SBV library adds support for symbolic bit vectors and other
+ symbolic types, allowing formal models of Haskell programs to be created.
.
> $ ghci -XScopedTypeVariables
> Prelude> :m Data.SBV
@@ -66,8 +66,8 @@ Description: Express properties about bit-precise Haskell programs and automat
bug reports, and patches are always welcome.
.
The following people reported bugs, provided comments/feedback, or contributed to the
- development of SBV in various ways: Ian Blumenfeld, Ian Calvert, Iavor Diatchki,
- Tom Hawkins, Lee Pike, Austin Seipp, Don Stewart, Josef Svenningsson, and Nis Wegmann.
+ development of SBV in various ways: Ian Blumenfeld, Ian Calvert, Iavor Diatchki, John
+ Erickson, Tom Hawkins, Lee Pike, Austin Seipp, Don Stewart, Josef Svenningsson, and Nis Wegmann.
.
Release notes can be seen at: <http://github.com/LeventErkok/sbv/blob/master/RELEASENOTES>.
Please sign in to comment.
Something went wrong with that request. Please try again.