Frama-C-discuss mailing list archives

siegel at udel.edu (Stephen Siegel) · Sun, 1 Sep 2013 11:51:26 -0400

On Aug 30, 2013, at 3:00 AM, Claude March? <Claude.Marche at inria.fr> wrote:

> 
> Dear Stephen,
> 
> I'm happy to learn that you are using Frama-C/Jessie for teaching, I did
> not know before. From your web page, I guess it in your course CISC
> 475/675? Is there any public web page where one can access to the
> exercises you give to students?

The class is CISC 414/614 "Formal Methods for Software Engineering".
I cover three approaches: structural analysis with Alloy, verification
condition generation and contracts with Frama-C, and model checking
and concurrency with Spin.  The site is restricted to students taking
the class but I would be happy to share exercises and examples and
will look at the why3 site and the others recommended by people on this list.

I'll try WP and Jessie and let you know what I find.

Best,

Steve

> 
> I'm asking that because I'm trying to record existing use of Jessie/Why3
> in teaching, and I'd like to encourage people to share the exercises
> they invent. (see http://why3.lri.fr/, section "Other Student Lectures
> using Why3", and I'd like to improve it)
> 
> Regarding your original question: for sure WP is newer and still
> evolves, whereas Jessie is mainly just maintained for the existing users
> (in teaching in particular!). They have different features and I don't
> think one is definitely better than the other, it depends on the kind of
> program you consider, and also the kind of property. I'd like to
> encourage you to test the examples you use for teaching with the WP
> plugin, an report to us about your experiments.
> 
> 
> - Claude
> 
> 
> Le 29/08/2013 18:26, Stephen Siegel a ?crit :
>> Which is better: WP or Jessie?  I have been using Jessie in my class for a couple of years, but it looks like WP is the newer thing.  Should I start using WP now?   I'm not sure what the advantages/disadvantages are of each.  Any advice or pointers to info. are appreciated. Thanks,
>> Steve
>> 
>> 
>> _______________________________________________
>> Frama-c-discuss mailing list
>> Frama-c-discuss at lists.gforge.inria.fr
>> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>> 
> 
> -- 
> Claude March?                          | tel: +33 1 72 92 59 69
> INRIA Saclay - ?le-de-France           |
> Universit? Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
> F-91405 ORSAY Cedex                    |
> 
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss

Frama-C-discuss mailing list archives

[Frama-c-discuss] wp vs. jessie?