We have two open positions in formal methods/verification at our team at
Intel:
http://jobs.intel.com/ShowJob/Id/1504155/Sr.-Formal-Verification-Engineer/
While the work centers around formal-verification of Intel's microprocessor
offerings, people with background in functional programming and
I'm happy to announce a new release of SBV (v4.0); a library for seamlessly
integrating SMT solvers with Haskell.
https://hackage.haskell.org/package/sbv
Most of the changes in this release are due to Brian Huffman of Galois;
essentially adding capabilities so end-users can define
I'm pleased to announce v3.1 release of SBV, a library for integrating SMT
solvers into Haskell.
This release coincides with GHC 7.8.3: A a prior bug in the 7.8 series
caused SBV to crash under heavy load. GHC 7.8.3 fixes this bug; so if
you're an SBV user, please upgrade to both GHC 7.8.3 and
SBV should be able to pick up Z3 from your path; make sure the z3
executable is in it and you can invoke it from your shell. Alternatively,
you can use the SBV_Z3 environment variable to point to the executable
itself, if adding it to your path is not desirable for whatever reason.
Let me know if
Our formal methods team at Intel has a full-time position available that I
think would be a good fit for functional programming and formal methods
enthusiasts. I'm including the description below. Do not hesitate to
contact me if you've any questions, or just want to talk about it in
general. To
Our formal methods team at Intel has a full-time position available that I
think would be a good fit for functional programming and formal methods
enthusiasts. I'm including the description below. Do not hesitate to
contact me if you've any questions, or just want to talk about it in
general. To
For better or worse; IEEE-754 settled many of these questions.
I personally think the standard is a good compromise of what's practical,
efficiently implementable, and mathematically sensible. I find the
following paper by Rummer and Wahl an especially good read:
I'm happy to announce the first release of conjugateGradient, implementing
the Conjugate Gradient algorithm for solving linear systems of equations
over sparse matrices:
http://hackage.haskell.org/package/conjugateGradient
The conjugate gradient algorithm only applies to the cases when the
, Richard A. O'Keefe o...@cs.otago.ac.nzwrote:
On 8/04/2013, at 11:21 AM, Levent Erkok wrote:
It appears that the consensus is that this is a historical definition
dating back to the times when IEEE754 itself wasn't quite clear on the
topic itself, and so nobody thought that hard about negative
Hello all,
I definitely do not want to create a yet another thread on handling of
floating-point values in Haskell. My intention is only to see what can be
done to make it more compilant with IEEE754. (Also, my interest is not a
theoretical one, but rather entirely practical: I'm interested in
[I'm posting on behalf of my colleague Jesse Bingham. While Jesse and I
work for different groups at Intel, we collaborate quite often, and I do
expect to work with the intern to an extent as well. To that end, I'm happy
to answer any questions you might have. Otherwise, direct all
correspondence
SymArray?
Thanks in advance!
Yours sincerely,
Jun Jie
2013/3/29 Levent Erkok erk...@gmail.com
Sorry, there were a couple of typos in the last example. It should read:
allSat $ \(x::SWord8) - x `shiftL` 2 ./= x
Note that this will return all 255 values that satisfy
Hi Jun Jie:
SBV uses some of the not-yet-officially-released features in Z3. The
version you have, while it's the latest official Z3 release, will not work.
To resolve, you need to install the development version of Z3 (something
that is at least 4.3.2 or better). Here're instructions from the
!
Yours sincerely,
Jun Jie
2013/3/29 Levent Erkok erk...@gmail.com
Hi Jun Jie:
SBV uses some of the not-yet-officially-released features in Z3. The version
you have, while it's the latest official Z3 release, will not work.
To resolve, you need to install the development version
the inversion of equality in the property.)
-Levent.
On Fri, Mar 29, 2013 at 6:49 AM, Levent Erkok erk...@gmail.com wrote:
You're welcome Jun Jie.
Regarding getting a different counter example: That's perfectly normal.
When SMT solvers build models they use random seeds. Furthermore, different
A new release (v0.5) of hArduno is out, now supporting servo-motors,
shift-registers, seven-segment displays, and distance sensors. Comes with a
bunch of examples to play around with:
http://leventerkok.github.com/hArduino/
On Hackage: http://hackage.haskell.org/package/hArduino
-Levent.
A new release (v0.5) of hArduno is out, now supporting servo-motors,
shift-registers, seven-segment displays, and distance sensors. Comes with a
bunch of examples to play around with:
http://leventerkok.github.com/hArduino/
On Hackage: http://hackage.haskell.org/package/hArduino
-Levent.
I'm happy to announce hArduino: a library that allows Arduino boards to be
controlled directly from Haskell. hArduino uses the Firmata protocol (
http://firmata.org), to communicate with and control Arduino boards, making
it possible to implement many controller projects directly in Haskell.
I'm happy to announce hArduino: a library that allows Arduino boards to be
controlled directly from Haskell. hArduino uses the Firmata protocol (
http://firmata.org), to communicate with and control Arduino boards, making
it possible to implement many controller projects directly in Haskell.
I'm happy to announce v2.9 release of the Haskell SBV library:
http://leventerkok.github.com/sbv/
SBV (SMT Based Verification) is a library that allows Haskell programs to
take advantage of modern SMT solvers, by providing a symbolic simulation
engine that can invoke 3rd party SMT solvers
Iavor's pretty-show package is quite handy for these kind of tasks as well.
Highly recommended: http://hackage.haskell.org/package/pretty-show
Since Iavor package is not tree-centric, it'll probably not generate as
nice output as you can for real tree-like-data. However, since it works on
On Oct 17, 2012, at 3:35 AM, Justin Paston-Cooper paston.coo...@gmail.com
wrote:
Thanks for all the informative replies. SBV seems the simplest solution right
now, and speed isn't too much of an issue here. Anything under 20 seconds per
solution should be bearable.
I'm happy to announce the
On Mon, Oct 15, 2012 at 9:00 AM, Johannes Waldmann
waldm...@imn.htwk-leipzig.de wrote:
Justin Paston-Cooper paston.cooper at gmail.com writes:
Can anyone suggest a library written in Haskell which can solve equations
of the form xM(transpose(x)) = y, where x should be an integer vector,
M is
[This message is more appropriate for a hackage mailing list I presume, but
that doesn't seem to exist. Let me know if there's a better place to send
it.]
I'm having a hackage compile failure for a newly uplodaded package that has
a QuickCheck 2.5 dependence. The error message is:
[13 of 13]
alexanderfore...@gmail.com
Date: 2012/7/17
Subject: Re: [Haskell-cafe] hackage compile failure with QuickCheck 2.5
To: Levent Erkok erk...@gmail.com
Dear Levent,
I think this [1] could be related.
Regards,
Alexander Foremny
[1]
http://haskell.1045720.n5.nabble.com/Bad-interface-problem
it. But maybe it's a possible work-around in case you
depend on the package being available on Hackage timely.
Regards,
Alexander Foremny
2012/7/17 Levent Erkok erk...@gmail.com:
It builds fine locally on my box; but not on hackage. Here's the page:
http://hackage.haskell.org/package/sbv-2.2
Ah, that explains why the hackage page mysteriously got fixed. Thanks for
looking into this Ross.
It still feels like this'll start biting more folks down the road. I've
created the following cabal ticket so it can be tracked:
https://github.com/haskell/cabal/issues/978
However, my
Chris: You might be experiencing this issue:
http://hackage.haskell.org/trac/ghc/ticket/5783
Upgrading text and recompiling fast-tags should take care of this problem.
-Levent.
On Sun, Apr 1, 2012 at 10:12 AM, Christopher Done
chrisd...@googlemail.com wrote:
By the way, I'm assuming that this
Neil Mitchell's HLint (http://community.haskell.org/~ndm/hlint/) warns
about extra parens in Haskell code. So, it must have code for
detecting those. I wonder if you can just insert parens liberally in a
first run, and then use his algorithm to remove those that are
unnecessary. The two passes can
Hello all,
SBV 0.9.24 is out: http://hackage.haskell.org/package/sbv
In short, SBV allows for scripting SMT solvers directly within
Haskell, with built-in support for bit-vectors and unbounded integers.
(Microsoft's Z3 SMT solver, and SRI's Yices can be used as backends.)
New in this release
Dimitrios:
The SBV library (http://hackage.haskell.org/package/sbv) can indeed
use Z3 as a backend SBV solver. However, it uses Z3 via SMT-Lib2, not
via it's C-API. It aims to provide a much higher level interface,
integrating with Haskell as smoothly as possible, keeping the
SMT-solver
New release of SBV (0.9.22) is out: http://hackage.haskell.org/package/sbv
Major changes in this release are:
- Support for explicit quantification (including alternating
existentials and universals)
- Ability to use Microsoft's Z3 SMT solver (in addition to Yices).
Full release notes:
On 8/12/2011 10:30 AM, Conal Elliott wrote:
Note that data-reify will only find *some* common/equal sub-expressions,
namely the pointer-equal ones. In all of my code-generating (deep)
DSLs, it's been very important for efficiency to also pull out
equal-but-pointer-unequal expressions.
-
Is there any way of getting the following code to immediately return
True without performing the element-by-element comparison? Essentially
this boils down to checking whether pointers are equal before
comparing the contents.
main = print $ f == f
where f = [1..10^9]
Nikhil,
As
On Jul 19, 2011, at 11:34 PM, Levent Erkok wrote:
import System.Mem.StableName
areEqual :: Eq a = a - a - IO Bool
areEqual x y = do
sx - hashStableName `fmap` (x `seq` makeStableName x)
sy - hashStableName `fmap` (y `seq` makeStableName y)
return $ (sx == sy) || x == y
One
On Mar 11, 2011, at 7:37 PM, Luke Palmer wrote:
On Fri, Mar 11, 2011 at 8:18 PM, Joshua Ball scioli...@gmail.com wrote:
Suppose I want the following functions:
newRef :: a - RefMonad (Ref a)
readRef :: Ref a - RefMonad a
writeRef :: Ref a - a - RefMonad ()
I would be delighted to see a
Andy Gill wrote a very nice recent paper on this topic which can serve
as the basis for a generic implementation:
http://www.ittc.ku.edu/~andygill/paper.php?label=DSLExtract09
As long as you do your reification in the IO monad, Andy's library
gives you the graph conversion for (almost-)
On 3/19/07, Nicolas Frisby [EMAIL PROTECTED] wrote:
Nope, but I believe the two are equipotent. This usage of believe is
one of those I think I remember reading it somewhere usages.
On 3/19/07, Henning Thielemann [EMAIL PROTECTED] wrote:
On Sat, 17 Mar 2007, Nicolas Frisby wrote:
Bekic's
Gracjan:To declare ReadP an instance of MonadFix; you'll first have to make the P monad into a MonadFix instance. That can be done using existing techniques in the literature.ReadP is essentially the continuation monad transformer wrapped around P. It's well known in the value-recursion literature
for the following program:
module Bug wheref :: Maybe Bool
f = g ()
g () = do f error bug?
If I ask ghci (version: 6.4.1) what the type of g is, it says:
*Bug :t g
g :: () - Maybe Bool
welcome.Thanks,Levent Erkok
___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
On the necessity of rec syntax, how is a statement like
do rec binds1
rec binds2
stmts
different from
do BV1 - mdo binds1
return BV1
BV2 - mdo binds2
return BV2
stmts
where BVn is a tuple of all the variables bound in bindsn.
These two
On Wed, 17 Sep 2003, Brandon Michael Moore wrote:
The problem with that is that not all monads support recursive bindings.
We can deal with that, but the desuagring of a do statement wouldn't be so
trivial any more. The most sensible approach I can think of is to analyze
the bindings and
On Wed, 17 Sep 2003, Brandon Michael Moore wrote:
Don't the laws for loop and mfix justify the transformation?
The loop axioms do, but Levent didn't assume right tightening, which
corresponds to moving bindings down from a rec, because monads like
exceptions don't satisfy it. The
On Monday 14 October 2002 09:25 am, you wrote:
While I'm happy that the fix versions outperform the 2-pass versions for
boxed arrays, the discrepency between 79.16 seconds for one million
elements and 4.54 sectons on the same data is alarming. Can anyone
suggest a way to reconcile this?
As
A couple of days ago, Hal Daume III asked
what does fixST do?
Briefly, fixST allows recursive definitions of values in the ST monad. As
you can guess, there's a bunch of such operators for different monads, the
most famous being fixIO, the corresponding operator for the IO monad.
These
On Thursday 25 October 2001 07:21 am, John Hughes wrote:
My proposal is that := should bind *monomorphically* -- just like lambda
binding. The motivation for that is that a polymorphic function can easily
become overloaded after a small change to the program, such as adding
removal of
Thanks for everyone who participated in the recent poll. Here are the results:
Never used: 6
Sometimes used: 1
Common commments:
willing to give it up for something cool
can be easily rewritten
wouldn't make a lot of difference
not sure if used ever, but wouldn't expect it
On Tue, 06 Jun 2000, Koen Claessen wrote:
Now, obviously there are not that many people who use
polymorphic let-bindings in do, but I don't think that is a
reason to introduce this restriction.
I agree. We were just trying to see if such polymorphic
let-generators were used often in
(Apologies to the list: The previous version of this message got out a little
premature, here's the complete version of it..)
Here's the pointer:
http://www.cse.ogi.edu/PacSoft/projects/muHugs/
The paper titled "Recursive Monadic Bindings" explains the ideas. (It also
briefly talks
On Sun, 04 Jun 2000, Koen Claessen wrote:
You cannot ask a question like this without explaining why
you are interested in this subject! :-) Just out of
curiosity... (I think that it is has to do with a recursive
do-translation, am I right?
Yes, we're working on a new semantics for do,
oo.
Thanks for your time.
John Launchbury Levent Erkok
Hi,
I've come accross an interesting bit of code:
class X a where
u :: a b - a b
f :: X a = b - a b
f = f
g :: X a = a b - b
g = g
-- h :: X a = b - a c
h b = f (g (h b))
53 matches
Mail list logo
