Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Frama-c-discuss Digest, Vol 97, Issue 4
  • From: prasuna.drdo at gmail.com (Prasuna Saka)
  • Date: Mon, 11 Jul 2016 15:43:01 +0530
  • In-reply-to: <mailman.5.1468231213.17967.frama-c-discuss@lists.gforge.inria.fr>
  • References: <mailman.5.1468231213.17967.frama-c-discuss@lists.gforge.inria.fr>
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>