Mastodawn

Hafstorsk Tutiluren Rufsgössen May 5, 2024

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

amiloradovsky Aug 18, 2023

"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

Stereophonic

amiloradovsky Aug 9, 2023

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

Stereophonic

Vivien (dentelle & numérique)Jul 17, 2023

J’ai enfin réussi à installer frama-c depuis guix (avec le micro-patch 64675), sans alt-ergo qui est propriétaire, mais avec Z3 qui est libre.

Votre .why3.conf doit contenir la section suivante :

[detected_binary]
exec_name = "/…/bin/z3"
name = "Z3"
version = "4.8.17"

Attention, il faut bien une majuscule à Z3, sinon why3 est perdu.

Il faut bien spécifier à frama-c-wp qu’on utilise Z3 :

frama-c-gui -wp -rte -wp-prover Z3 main.c

#guix #why3 #z3 #framaC

René Dudfield Jan 11, 2023

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

WEBLIB.RE par Samuel Vermeulen Oct 26, 2021

#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

Frama, c’est aussi de la médiation aux communs numériques

De l'édition de livre aux ateliers et conférences, des interviews aux traductions sur le blog et jusqu'au podcast... À Framasoft, nous explorons de nombreuses manières de partager ce que nous savons et d'apporter notre pierre à l'édifice des communs culturels. « Frama, c'est pas que... » Pour l'automne 2021, chaque semaine, nous voulons vous faire...

Framablog

WEBLIB.RE par Samuel Vermeulen Oct 19, 2021

#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

Frama, c’est aussi des services en ligne

Il y a bien plus de gens qui utilisent les Framapad, Framforms, Framadate... que de personnes qui connaissent l'association Framasoft. C'est logique : ces services sont si pratiques que de nombreuxses bénéficiaires les intègrent dans leur quotidien sans forcément savoir comment ça se passe en coulisses. « Frama, c'est pas que... » Pour l'automne 2021,...

Framablog

WEBLIB.RE par Samuel Vermeulen Oct 12, 2021

#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

Frama, c’est aussi des humain·es qui s’associent

Si Framasoft est connue pour ses Framapad, Framaforms, Framadate, etc. « Frama », c'est – avant tout – une association loi de 1901. Nous sommes donc un collectif d'humain·es, avec nos fragilités, envies, colères, rêves et relations... Tout cela joue forcément sur les actions que nous menons. « Frama, c'est pas que... » Pour l'automne...

Framablog