Lmst

I started looking at ACSL in Frama-C. Looks promising, although a bit complex at first.

I wonder if I can convey it to output its proofs in some readable format for archiving. And it would be swell with some test report or so. Perhaps also a non-zero return code so that it becomes more easily integrated in a regression test CI/CD pipeline.

#FramaC #ACSL

"The current verification tool for #ACSL is #FramaC. It also implements a sister language, ANSI/ISO C++ Specification Language (ACSL++), defined for C++."

https://en.wikipedia.org/wiki/ANSI/ISO_C_Specification_Language

last time I checked, C++ was left out, only C was supported — times have changed?

now I wonder where #Rust is in the process — there seems to be an ongoing work but nothing that would stand out yet

for #Ada there is #SPARK

https://en.wikipedia.org/wiki/SPARK_(programming_language)

and #PSL is actually independent from the HDLs, can be added on top of VHDL, SV, or Synthesizable #SystemC as well, though the implementations are uncertain

https://en.wikipedia.org/wiki/Property_Specification_Language

p.s. #Accelera good, IEEE bad

naive random thought: #FramaC and the like should not need human interaction and be able to always check automatically that the post-conditions follow from pre-conditions -- it's proof checking (the C code is the proof term), not search (for which there may be no generic algorithm)
well actually no: this proof term (C code) is only concerned with the explicit arguments (passed as C function arguments) and ignores the implicit hypotheses (pre-conditions); what's more important is that this function returns only the C value and not Cartesian product (dependent sum) of it with the post-conditions
the dependence of the post-conditions on the pre-conditions, the C function arguments, and the result is yet to be constructed, e.g.

forall x, A x -> exists y, B x y

A x is the pre-condition, B x y is the post-condition, x is input argument, and y is the result of C function

y_t f (x_t x) { ... }

f alone isn't enough to build a term of type B x y

to be even more specific, let x_t and y_t be uint8_t, f be increment by one, A x be x < 255, and B x y be x < y

Glad to see #FramaC get a shout out from #AdaCore. #C is one language with tooling for using solvers to prove correctness. Glad to see competition here. They’re moving the whole industry forward.

https://www.adacore.com/uploads/technical-papers/2016-10-SPARK-MisraC-FramaC.pdf

#ActuLibre Ce que Framasoft pourrait faire en 2022, grâce à vos dons, à lire sur https://framablog.org/2021/12/08/ce-que-framasoft-pourrait-faire-en-2022-grace-a-vos-dons/ #accompagnementnumérique #cohérencenumérique #deslivresencommuns #Deframasoftisons #Framac'estaussi #logicielslibres #justicesociale #Contributopia #contributions #contributopia #associations #Degooglisons #Emancip'Asso #militantisme #Association #bénévalibre #framaforms #librecours #rencontres #Framabook #framadate #manifeste

#ActuLibre PeerTube v4, more power to help you present your videos, à lire sur https://framablog.org/2021/11/30/peertube-v4-more-power-to-help-you-present-your-videos/ #Framac'estaussi #Contributopia #contributopia #Developpement #Degooglisons #ActivityPub #Framasoft #pairàpair #Peer2peer #PeerTube #Donation #RezoTIC #YouTube #direct #Planet #GAFAM #Video #live

#ActuLibre Mobilizon v2, now matured, like a good French wine, à lire sur https://framablog.org/2021/11/23/mobilizon-v2-now-matured-like-a-good-french-wine/ #Framac'estaussi #Contributopia #contributopia #Degooglisons #ActivityPub #Communaute #Innovation #Mobilizon #framameet #Framasoft #Facebook #Internet #English #RezoTIC #MeetUp #Planet #Event #GAFAM

#ActuLibre Frama, c’est aussi des logiciels pour libérer les usages, à lire sur https://framablog.org/2021/11/23/frama-cest-aussi-des-logiciels-pour-liberer-les-usages/ #Framac'estaussi #Contributopia #Contribution #Contribuer #framaforms #framadate #Mobilizon #Nextcloud #Etherpad #PeerTube #yakforms

#ActuLibre Frama c’est aussi des contributions dans un archipel, à lire sur https://framablog.org/2021/11/16/frama-cest-aussi-des-contributions-dans-un-archipel/ #accompagnementnumérique #cohérencenumérique #Framac'estaussi #archipélisation #contribatelier #framapetitions #Contributopia #confinatelier #contributions #associations #BiensCommuns #Contribution #émancipation #bénévalibre #Partenariat #Contribuer #solidarité #manifeste #Annuaire #archipel #Entraide #Libertés #pytition #chatons #Libre

#ActuLibre Frama, c’est aussi des outils pour s’émanciper, à lire sur https://framablog.org/2021/11/09/frama-cest-aussi-des-outils-pour-semanciper/ #accompagnementnumérique #cohérencenumérique #Framac'estaussi #Contributopia #contributopia #Documentation #alternatives #émancipation #Metacartes #Mobilizon #numerique #PeerTube #Services #yakforms #chatons #EducPop #resolu #mooc #ESS

#ActuLibre Frama, c’est aussi des personnes au service des services, à lire sur https://framablog.org/2021/11/02/frama-cest-aussi-des-personnes-au-service-des-services/ #Deframasoftisons #Framac'estaussi #infrastructure #Contributopia #alternatives #Degooglisons #serveurs #Services #soutenir #Accueil #chatons #contact #Service #support #forum

#ActuLibre Frama, c’est aussi de la médiation aux communs numériques à lire sur https://framablog.org/2021/10/26/frama-cest-aussi-de-la-mediation-aux-communs-numeriques/ #Framac'estaussi #Contributopia #contributopia #Conferences #Communaute #Conference #Framablog #Framabook #Framalang #médiation #communs #Commun #Médias #UPLOAD

#ActuLibre Frama, c’est aussi des services en ligne à lire sur https://framablog.org/2021/10/19/frama-cest-aussi-des-services-en-ligne/ #DégooglisonsInternet #Framac'estaussi #Contributopia #contributopia #Degooglisons #Communaute #framaforms #framadate #Framapad #Services #RezoTIC #Planet #GAFAM

#ActuLibre Frama, c’est aussi des humain·es qui s’associent à lire sur https://framablog.org/2021/10/12/frama-cest-aussi-des-humain%c2%b7es-qui-sassocient/ #Framac'estaussi #Contributopia #contributopia #Communaute #Framasoft #RezoTIC #Humour #Planet

#FramaC WP just threw at me that #ACSL lambdas are not supported yet. How the hell am i supposed to use \numof ?! #framacWP #formalmethods

I have time to figure it out till Dec30

It's of course ”with Frama-C” and let me add a few tags: #FramaC #FormalMethods #DeductiveVerification

Messing around with #Frama-C again. Managed to prove that a gcd() function actually has the property that there is no number greater than the return value which divides both arguments. Or in ACSL parlance: ensures ! (\exists integer x; x > \result && a % x == 0 && b % x == 0)

I wrote a blog post about my recent experiences with #Frama-C, a tool for doing formal verification of C code. Check it out: http://www.härdin.se/blog/2018/11/20/trying-out-frama-c/

Tried implementing some basic string manipulation functions in #frama-c today. Specifically, strlcpy() and my own strlen(). Quite tricky. But I did learn one can take a gander at /usr/share/frama-c/libc/string.h to get some ideas for more ACSL to decorate one's contracts with. #langsec

#Framac

Client Info