π’Β We are happy to inform you that ππ§ππ«ππ’ πππ¦π¨π€π’π¬π‘ will make a presentation at ππ
ππ ππππ. He will present a translation from arKItect models into Coq theorem prover. This provides the opportunity to specify and demonstrate formally π©π«π¨π©ππ«ππ’ππ¬ π¨π ππ«ππππππ π¬π²π¬πππ¦ π¦π¨πππ₯π¬ with a best-in-class formal environment. Our focus here is π¬πππππ² ππ§ππ₯π²π¬π’π¬.
Β
Choice of Coq was natural because systems are inductive definitions (systems are made of systems), and arKItect is managing system models as set of trees reflecting this structure. That fits well with inductive types in Coq.
Of course, many issues come around: what is a complete and correct system model?Β what is a complete and correct safety analysis/safety case. The other stake is to make all this transparent to end user who is interested in doing things right with a simple and intuitive interface and not complex language stuff.
π Wednesday, February 1, 2023
