--- layout: fc_discuss_archives title: Message 9 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 4



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>:

> Send Frama-c-discuss mailing list submissions to
>         frama-c-discuss at lists.gforge.inria.fr
>
> 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
>
> You can reach the person managing the list at
>         frama-c-discuss-owner at lists.gforge.inria.fr
>
> 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>
> To: "frama-c-discuss at lists.gforge.inria.fr"
>         <frama-c-discuss at lists.gforge.inria.fr>
> Subject: [Frama-c-discuss] JFLA 2017 : premier appel à communications
> Message-ID:
>         <D8D4FC26B114714EB1FAE173346799BB2C1B447F at EXDAG0-A1.intra.cea.fr>
> 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>
> To: frama-c-discuss at lists.gforge.inria.fr
> Subject: [Frama-c-discuss] A problem with math functions
> Message-ID:
>         <
> CAA80GKO_sieHDpu3-1E_sTE1TgU0Lw+BwkVNLbia8t0+v_CCsQ at mail.gmail.com>
> 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>
> To: Frama-C public discussion <frama-c-discuss at lists.gforge.inria.fr>
> Subject: Re: [Frama-c-discuss] A problem with math functions
> Message-ID: <F3ED5FA7-7D8D-41B6-BCD2-A5D2F5A3982F at cea.fr>
> 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>
> To: frama-c-discuss at lists.gforge.inria.fr
> Subject: Re: [Frama-c-discuss] A problem with math functions
> Message-ID: <57835A9F.2080702 at inria.fr>
> 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
> 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-0001.html>