--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on July 2016 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-c-discuss Digest, Vol 97, Issue 5



Thanks Mr.Claude. Will try with Jessie.

On Monday, July 11, 2016, <frama-c-discuss-request at lists.gforge.inria.fr>
wrote:

> Send Frama-c-discuss mailing list submissions to
>         frama-c-discuss at lists.gforge.inria.fr <javascript:;>
>
> To subscribe or unsubscribe via the World Wide Web, visit
>         http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
> or, via email, send a message with subject or body 'help' to
>         frama-c-discuss-request at lists.gforge.inria.fr <javascript:;>
>
> You can reach the person managing the list at
>         frama-c-discuss-owner at lists.gforge.inria.fr <javascript:;>
>
> When replying, please edit your Subject line so it is more specific
> than "Re: Contents of Frama-c-discuss digest..."
>
>
> Today's Topics:
>
>    1. Re: Frama-c-discuss Digest, Vol 97, Issue 4 (Prasuna Saka)
>
>
> ----------------------------------------------------------------------
>
> Message: 1
> Date: Mon, 11 Jul 2016 15:43:01 +0530
> From: Prasuna Saka <prasuna.drdo at gmail.com <javascript:;>>
> To: frama-c-discuss at lists.gforge.inria.fr <javascript:;>
> Subject: Re: [Frama-c-discuss] Frama-c-discuss Digest, Vol 97, Issue 4
> Message-ID:
>         <
> CAA80GKPysEEhSBTeXdKHER1nHgZz1Q0it_DpRcww8bMhWU+azQ at mail.gmail.com
> <javascript:;>>
> Content-Type: text/plain; charset="utf-8"
>
> Many Thanks for the quick replies. Wanted to know whether
> Jessie plug-in is able to handle trigonometric functions? If so, can I use
> Jessie with Coq?
>
> Thanks
> Prasuna
>
> 2016-07-11 15:30 GMT+05:30 <frama-c-discuss-request at lists.gforge.inria.fr
> <javascript:;>>:
>
> > Send Frama-c-discuss mailing list submissions to
> >         frama-c-discuss at lists.gforge.inria.fr <javascript:;>
> >
> > To subscribe or unsubscribe via the World Wide Web, visit
> >         http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
> > or, via email, send a message with subject or body 'help' to
> >         frama-c-discuss-request at lists.gforge.inria.fr <javascript:;>
> >
> > You can reach the person managing the list at
> >         frama-c-discuss-owner at lists.gforge.inria.fr <javascript:;>
> >
> > When replying, please edit your Subject line so it is more specific
> > than "Re: Contents of Frama-c-discuss digest..."
> >
> >
> > Today's Topics:
> >
> >    1. JFLA 2017 : premier appel à communications (SIGNOLES Julien)
> >    2. A problem with math functions (Prasuna Saka)
> >    3. Re: A problem with math functions (Loïc Correnson)
> >    4. Re: A problem with math functions (Claude Marché)
> >
> >
> > ----------------------------------------------------------------------
> >
> > Message: 1
> > Date: Sun, 10 Jul 2016 18:19:51 +0000
> > From: SIGNOLES Julien <julien.signoles at cea.fr <javascript:;>>
> > To: "frama-c-discuss at lists.gforge.inria.fr <javascript:;>"
> >         <frama-c-discuss at lists.gforge.inria.fr <javascript:;>>
> > Subject: [Frama-c-discuss] JFLA 2017 : premier appel à communications
> > Message-ID:
> >         <D8D4FC26B114714EB1FAE173346799BB2C1B447F at EXDAG0-A1.intra.cea.fr
> <javascript:;>>
> > Content-Type: text/plain; charset="iso-8859-1"
> >
> > [ This message is intentionally written in French. ]
> >
> >     * Merci de faire circuler : premier appel à communications *
> >
> >               JFLA'2017 (http://jfla.inria.fr/2017/)
> >
> >           Journées Francophones des Langages Applicatifs
> >
> >              dans les Pyrénées, du 4 au 7 janvier 2017
> >
> >
> > Dates importantes
> > -----------------
> >
> > 25 septembre 2016 : date limite de soumission des résumés
> > 09 octobre 2016   : date limite de soumission des articles
> > 18 novembre 2016  : notification aux auteurs
> > 27 novembre 2016  : remise des articles définitifs
> > 04 au 07 janvier 2017 : journées
> >
> > Les JFLA réunissent concepteurs, utilisateurs et théoriciens ; elles
> > ont pour ambition de couvrir les domaines des langages applicatifs, de
> > la preuve formelle, de la vérification de programmes, et des objets
> > mathématiques qui sous-tendent ces outils. Ces domaines doivent être
> > pris au sens large : nous souhaitons promouvoir les ponts entre
> > les différentes thématiques.
> >
> > . Langages fonctionnels et applicatifs : sémantique, compilation,
> >   optimisation, typage, mesures, extensions par d'autres paradigmes.
> >
> > . Assistants de preuve : implémentation, nouvelles tactiques,
> >   développements présentant un intérêt technique ou méthodologique.
> >
> > . Logique, correspondance de Curry-Howard, réalisabilité, extraction
> >   de programmes, modèles.
> >
> > . Spécification, prototypage, développements formels d'algorithmes.
> >
> > . Vérification de programmes ou de modèles, méthode déductive,
> >   interprétation abstraite, raffinement.
> >
> > . Utilisation industrielle des langages fonctionnels et applicatifs,
> >   ou des méthodes issues des preuves formelles, outils pour le web.
> >
> > Les articles soumis aux JFLA sont relus par au moins deux personnes
> > s'ils sont acceptés, trois personnes s'ils sont rejetés. Les critiques
> > des relecteurs sont toujours bienveillantes et la plupart du temps
> > encourageantes et constructives, même en cas de rejet.
> >
> > Il n'y a donc pas de raison de ne pas soumettre aux JFLA !
> >
> > Cours invités
> > -------------
> >
> > . Guillaume Burel (ENSIIE)
> >   sur "Dedukti, un vérificateur de preuve universel" (titre exact à
> > préciser)
> >
> > . Benjamin Canou (OCamlPro SAS)
> >   sur "comment programmer en OCaml aujourd'hui" (titre exact à préciser)
> >
> > Exposés invités
> > -------------
> >
> > . Stéphane Lescuyer et Florence Plateau (Prove and Run)
> >   sur "langage, prouveur et autres outils dédiés à la preuve d'un
> > micro-noyau"
> >   (titre exact à préciser)
> >
> > . second orateur invité à préciser
> >
> > Comité de programme
> > -------------------
> >
> > Julien     Signoles       CEA LIST (président)
> > Sylvie     Boldo          Inria Saclay-ÃŽle de France, LRI
> (vice-présidente)
> > June       Andronick      Data61/CSIRO et UNSW
> > Anne-Gwenn Bosser         ENIB, Lab-STICC
> > Thomas     Gazagnaire     Docker
> > Mohamed    Iguernlala     OCamlPro SAS
> > Frédéric   Loulergue      Université d'Orléans
> > Laurent    Mounier        Verimag, Université Grenoble Alpes
> > François   Pottier        Inria Paris
> > Sylvain    Salvati        Inria Bordeaux-Sud Ouest
> > Mihaela    Sighireanu     IRIF, Université Paris 7
> > Francesco  Zappa Nardeli  Inria Paris
> >
> > Soumissions
> > -----------
> >
> > Nous acceptons deux types de soumissions :
> >
> > . Article de recherche de quinze pages au plus, portant sur des
> >   travaux originaux. Nous acceptons des travaux en cours, pour lesquels
> >   l'aspect recherche n'est pas entièrement finalisé.
> >
> > . Article court de six pages au plus, pour décrire un prototype,
> >   faire la démonstration d'un outil, rechercher de l'aide pour résoudre
> >   un problème particulier, ou reparler d'un papier déjà publié.
> >
> > Dans tous les cas, la forme de l'article devra soignée. Les articles
> > sélectionnés seront publiés dans les actes de la conférence, et les
> > auteurs seront invités à faire une présentation lors des journées,
> > de vingt-cinq minutes pour les articles longs et de quinze minutes pour
> > les courts.
> >
> > L'article peut être rédigé en anglais, auquel cas la présentation devra
> > être effectuée en français. Néanmoins, dans le cas où il s'agit d'une
> > republication au format court d'un article déjà publié, la publication
> > doit être en français et la publication originale en anglais.
> >
> > Le style LaTeX est imposé :
> >
> >   http://jfla.inria.fr/2017/actes.sty
> >
> > date limite de soumission des résumés  : 25 septembre 2016
> > date limite de soumission des articles : 09 octobre 2016
> >
> > -------------- next part --------------
> > An HTML attachment was scrubbed...
> > URL: <
> >
> http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160710/f8012b98/attachment-0001.html
> > >
> >
> > ------------------------------
> >
> > Message: 2
> > Date: Mon, 11 Jul 2016 11:26:24 +0530
> > From: Prasuna Saka <prasuna.drdo at gmail.com <javascript:;>>
> > To: frama-c-discuss at lists.gforge.inria.fr <javascript:;>
> > Subject: [Frama-c-discuss] A problem with math functions
> > Message-ID:
> >         <
> > CAA80GKO_sieHDpu3-1E_sTE1TgU0Lw+BwkVNLbia8t0+v_CCsQ at mail.gmail.com
> <javascript:;>>
> > Content-Type: text/plain; charset="utf-8"
> >
> > Hi,
> >
> > I am trying to solve a simple problem having math function "cos". In the
> > annotations, I have used the built-in function \cos. However, when run
> with
> > WP plug-in using the Frama-C Neon Version, following error is thrown :
> >
> > [wp} user error: Builtin \cos(real) not defined
> > [wp] failure: Logic \cos undefined.
> >
> > Please let em know the reason for the above errors. How do I make the
> > built-in function available at run-time.
> >
> > Thanks & Regards,
> >
> > Prasuna
> > -------------- next part --------------
> > An HTML attachment was scrubbed...
> > URL: <
> >
> http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160711/d30e47da/attachment-0001.html
> > >
> >
> > ------------------------------
> >
> > Message: 3
> > Date: Mon, 11 Jul 2016 09:30:58 +0200
> > From: Loïc Correnson <loic.correnson at cea.fr <javascript:;>>
> > To: Frama-C public discussion <frama-c-discuss at lists.gforge.inria.fr
> <javascript:;>>
> > Subject: Re: [Frama-c-discuss] A problem with math functions
> > Message-ID: <F3ED5FA7-7D8D-41B6-BCD2-A5D2F5A3982F at cea.fr <javascript:;>>
> > Content-Type: text/plain; charset=utf-8
> >
> > > [wp} user error: Builtin \cos(real) not defined
> > > [wp] failure: Logic \cos undefined.
> >
> > We simply did not implement all built-ins in WP.
> > One reason is that many SMT solvers (if not all) lack interesting
> > properties about trigonometry.
> >
> > Workarounds:
> >  - either use another name, like ‘cos’, and declare it using standard
> ACSL
> > « logic real cos(real x); » within an axiomatic bloc, and add desired
> > axioms and lemmas ;
> >  - or use a WP driver (WP manual § 2.4.10, p28) to bind `\cos` to some
> > symbol in  your favorite SMT solver (or Coq or Why3) ; for instance, see
> > how we handle the ‘\max’ function in '$(frama-c
> > -print-share-path)/wp/wp.driver’
> >
> > In all cases, consider using -wp-model float
> >
> >         L.
> >
> >
> >
> >
> > ------------------------------
> >
> > Message: 4
> > Date: Mon, 11 Jul 2016 10:36:47 +0200
> > From: Claude Marché <Claude.Marche at inria.fr <javascript:;>>
> > To: frama-c-discuss at lists.gforge.inria.fr <javascript:;>
> > Subject: Re: [Frama-c-discuss] A problem with math functions
> > Message-ID: <57835A9F.2080702 at inria.fr <javascript:;>>
> > Content-Type: text/plain; charset=utf-8
> >
> >
> >
> > Le 11/07/2016 09:30, Loïc Correnson a écrit :
> > > One reason is that many SMT solvers (if not all) lack interesting
> > properties about trigonometry.
> >
> > Yes, as far as I know, no SMT solver know about trigonometry. But there
> > are other provers available as Why3 back-end that do, and Why3 drivers
> > indeed know how to use them : MetiTarski, Coq, Isabelle/HOL
> >
> > For proving floating-point programs correct w.r.t a specification
> > involving real numbers, it is mandatory to use provers outside the SMT
> > world.
> >
> > See for examples http://toccata.lri.fr/gallery/fp.en.html
> >
> >
> > - Claude
> >
> > --
> > Claude Marché                          | tel: +33 1 69 15 66 08
> > INRIA Saclay - ÃŽle-de-France           |
> > Université Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
> > F-91405 ORSAY Cedex                    |
> >
> >
> > ------------------------------
> >
> > Subject: Digest Footer
> >
> > _______________________________________________
> > Frama-c-discuss mailing list
> > Frama-c-discuss at lists.gforge.inria.fr <javascript:;>
> > http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
> >
> > ------------------------------
> >
> > End of Frama-c-discuss Digest, Vol 97, Issue 4
> > **********************************************
> >
> -------------- next part --------------
> An HTML attachment was scrubbed...
> URL: <
> http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160711/deb68f9e/attachment.html
> >
>
> ------------------------------
>
> Subject: Digest Footer
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr <javascript:;>
> http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
>
> ------------------------------
>
> End of Frama-c-discuss Digest, Vol 97, Issue 5
> **********************************************
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160711/7b6e58e2/attachment-0001.html>