We update the slides on the website after each refinement (and each workshop/presentation) so they should get progressively easier to follow. That said, the project is currently incomplete so the missing/to be determined aspects will continue to impede complete understanding for now. We have recorded both community workshops and emailed the links to the mailing list in the hopes that replaying those might help with following the slides.
This project is a great idea. A robust open source model checking framework is what we need.
Question: do you intend for the intermediate language to be a target of translation from C code? If so, it would be good to think through some examples, especially when it comes to the memory model, pointers, dynamic allocation, etc. — all the things that make C hard to reason about.
Thank you for this question. We are creating an intermediate language for the hardware model checking community; there has been some confusion as the applicability to software model checking. Software model checking is outside of the scope of our current project but, since all of our examples and those contributed from the broader research community will be available open-source via this website (linked with GitHub), anyone is welcome to contribute extensions per your question. Perhaps you can lead a future line of papers examining the important considerations you mention above.
We have emailed all registered email addresses including this one, however our messages may be caught in spam or other filters. We are happy to coordinate with you individually.
There was some discussion about choice of logics and support for different logics in yesterday’s feedback workshop.
You’ve made the pragmatic decision to go with trace semantics, which fits many logics, including LTL, but means you can’t support logics with state-based semantics like CTL.
What about trace-based properties like trace refinement, where you want to check whether the traces of one transition system are a subset of another? Given your trace semantics, it might be the most natural way to support assume-guarantee reasoning with richer specifications.
An interesting discussion is definitely worth comment.
There’s no doubt that that you should publish more about this subject, it might not be a
taboo matter but usually people don’t speak about such topics.
To the next! Best wishes!!
I found the slides quite difficult to follow. Is there any sort of text definition of the intermediate language?
We update the slides on the website after each refinement (and each workshop/presentation) so they should get progressively easier to follow. That said, the project is currently incomplete so the missing/to be determined aspects will continue to impede complete understanding for now. We have recorded both community workshops and emailed the links to the mailing list in the hopes that replaying those might help with following the slides.
This project is a great idea. A robust open source model checking framework is what we need.
Question: do you intend for the intermediate language to be a target of translation from C code? If so, it would be good to think through some examples, especially when it comes to the memory model, pointers, dynamic allocation, etc. — all the things that make C hard to reason about.
Thank you for this question. We are creating an intermediate language for the hardware model checking community; there has been some confusion as the applicability to software model checking. Software model checking is outside of the scope of our current project but, since all of our examples and those contributed from the broader research community will be available open-source via this website (linked with GitHub), anyone is welcome to contribute extensions per your question. Perhaps you can lead a future line of papers examining the important considerations you mention above.
Hello, Although I’ve registered for the seminar didn’t receive any link.
We have emailed all registered email addresses including this one, however our messages may be caught in spam or other filters. We are happy to coordinate with you individually.
When will the recordings be made available?
We have emailed a link to the password-protected folder containing workshop recordings. If you did not receive it, we are happy to resend.
There was some discussion about choice of logics and support for different logics in yesterday’s feedback workshop.
You’ve made the pragmatic decision to go with trace semantics, which fits many logics, including LTL, but means you can’t support logics with state-based semantics like CTL.
What about trace-based properties like trace refinement, where you want to check whether the traces of one transition system are a subset of another? Given your trace semantics, it might be the most natural way to support assume-guarantee reasoning with richer specifications.
An interesting discussion is definitely worth comment.
There’s no doubt that that you should publish more about this subject, it might not be a
taboo matter but usually people don’t speak about such topics.
To the next! Best wishes!!