[Spark2014-discuss] [L621-012] formal semantics of SPARK 2014

Robby robby at ksu.edu
Thu May 2 20:07:20 CEST 2013


>> We have posted an updated Sireum Bakar documentation that includes
>> tool installation as well as development environment setup at:
>>
>> http://sireum.github.io/doc/bakar/
>
> Already? Great! I'll try it as soon as I get a free slot. (tonight? ;))

I should perhaps qualify "tool" here.  :)
It is mostly for the translators at this point; for example, it does
not include Alir and Kiasan v2 targeting Spark 2014 (however, you can
install Bakar v1 under Eclipse that were used for the HILT tutorial --
see https://www.sireum.org/features).
The GPS plugin (Bakar v1, and later for v2 when they are ready to be
integrated) is not ready yet; Jakub is creating a presentation to show
case some of its features that we hope to share soon.


Robby

PS: Note that in the doc, we direct people to ask AdaCore for a
specific GNAT Pro (and ASIS) wavefront. Of course, once we have a GPL
version, the tool installation would be seamless. ;) *hint*

--
-------------------------------------------------------------------------
Robby                             Phone: 785-532-6350
Associate Professor                      785-532-7904 (direct)
Department of Computing and       Fax:   785-532-7353
 Information Sciences
324B Nichols Hall                 Email: robby at k-state.edu
Kansas State University           WWW:   http://people.cis.ksu.edu/~robby
Manhattan, KS 66506
-------------------------------------------------------------------------


More information about the Spark2014-discuss mailing list