mild democracy for October's paperclub

[Quinn Dougherty]

Hey! As a reminder, September's paperclub is tomorrow at 10a on USA's Pacific timezone. Click here for gcal ticket.

I'm inclined toward two options for October paper club.

1. Models that Prove their Own Correctness https://arxiv.org/abs/2405.15722, in fairly top down fashion where myself or someone spends 20 minutes on a summary slide deck before group discussion (this is tomorrow's format for the assume-guarantee composition on ACAS Xu paper). Ronak sent me this paper the other day, but it's from June, and it'll be in the newsletter next week.
2. Collaborative dive into aviation software, even if the only stuff we can find is very old. Have in mind resources like this http://www.chilton-computing.org.uk/acd/pdfs/acsl.pdf or this https://dl.acm.org/doi/abs/10.1145/800233.807048, but if we can find more recent innovations that would be great. In this format, we'd have like 4 resources summarized by 4 people at 5-10 minutes each

i've been flipping through this book at lighthaven, and it'd also be good to assign chapters from that in the same setup as option two.

I'm open to some third thing, but suggesting is volunteering. If you don't like those options, and you want to cover a different paper instead, I'll ask you to do the summary slide deck of it. If you vote for the second option, you're certainly volunteering to do a 5-10 minute presentation.

Having typed this out, let's say by default if I get 4 volunteers (3 + me + 1 x redundancy) we do the second option. But if people don't volunteer for collaborative deep dive, then default is the first option. Feel free to also vote for Apollo Guidance Computer book.

[Yudhister Joel Kumar]

Out of curiosity, why the focus on avionics? If the point is to get a case study, why not focus on the seL4 whitepaper or something like CompCert? 

--
You received this message because you are subscribed to the Google Groups "guaranteed-safe-ai" group.
To unsubscribe from this group and stop receiving emails from it, send an email to guaranteed-safe...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/guaranteed-safe-ai/CAGaOgAQqUe2%2BYOoN1T9F%2Be2V38Oscg9jeQo5LEuGH%2BZVoLhGmw%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.

[Quinn Dougherty]

We can run those. 

Avionics seems more to the point because it impinges on physics. 

Moreover, I expect GSAI practitioners need to know about a great breadth of QA techniques, many of which don't look like "proof" but nevertheless have ridiculously high assurance. 

Selfishly, I just know more about seL4 and compcert than I do about aviation, so aviation feels more like a target (to me). 

Additionally, avionics is hard to study because of how much is trade or defense secret, which makes it a good candidate for group study (more eyes tracking down more public resources)

Super open to getting overruled here. It's as democratic as the enthusiasm is :), depends on what most people want to do. We'll try to take a few minutes to discuss this tomorrow 

Btw, I forgot in my last message: I'm thinking third Thursday of every month at 10 pacific, so the October edition would be the 17th 

[Kris Carlson]

It appears this bounced due to the book attachment, here's a link instead.

Karmakar, Development of Safety-Critical Systems-Springer

I think avionics, as an example of a successful safety-critical system, is highly germane. Coincidentally, the guy who is building the crash-proof low-level language says he previously designed a safety-critical USDOT traffic control system, national critical infrastructure.

Along those lines, I've collected a few papers and a book on the topic (e.g. attached), but still know little about it, so I share Quinn's curiosity. I also had an expert in this area review Provably Safe Systems, but the results weren't quite as good as I intended.

When I was invited to co-chair the Seminar on Natural and Artificial Intelligence at the Rowland Institute, I insisted that recommendations for readings had to come from people *who had done the reading*, not just 'this looks interesting', which had resulted in wasting our time reading some dud papers. We didn't have many duds after that. I recommend that policy and so I'm not yet recommending anything in what I've sent, but endorse the topic. I'd be happy to invited a guest speaker.

Hope to attend but have a tight schedule.

- Kris

To view this discussion on the web visit https://groups.google.com/d/msgid/guaranteed-safe-ai/CAGaOgASYo0Aa6ZaYbVrT0LjxQCitf9PmM5NRBULtD%3D%2Bb95DWHg%40mail.gmail.com.

[Syed Jafri]

I'm pretty interested in Models that Prove their Own Correctness but that might be because I have a bit more familiarity. I'd be open to making a summary slide deck as well.

[Jason Gross]

As I understand it avionics is actually one of the primary customers of CompCert.  I haven't read these (my understanding comes from a keynote Xavier Leroy gave a while ago), but you may be interested in

@inproceedings{Leroy-PPES-2011,

  author = {Ricardo {Bedin França} and Denis Favre-Felix and Xavier Leroy

            and Marc Pantel and Jean Souyris},

  title = {Towards Optimizing Certified Compilation in Flight Control Software},

  booktitle = {Workshop on Predictability and Performance in Embedded Systems (PPES 2011)},

  pages = {59--68},

  series = {OpenAccess Series in Informatics},

  volume = 18,

  publisher = {Dagstuhl Publishing},

  year = {2011},

  url = {http://hal.archives-ouvertes.fr/inria-00551370/},

  urlpublisher = {http://dx.doi.org/10.4230/OASIcs.PPES.2011.59},

  xtopic = {compcert},

  abstract = {

This work presents a preliminary evaluation of the use of the CompCert formally specified and verified optimizing compiler for the development of level A critical flight control software. First, the motivation for choosing CompCert is presented, as well as the requirements and constraints for safety-critical avionics software. The main point is to allow optimized code generation by relying on the formal proof of correctness instead of the current un-optimized generation required to produce assembly code structurally similar to the algorithmic language (and even the initial models) source code. The evaluation of its performance (measured using WCET) is presented and the results are compared to those obtained with the currently used compiler. Finally, the paper discusses verification and certification issues that are raised when one seeks to use CompCert for the development of such critical software. }

}

@inproceedings{Bedin-Franca-ERTS-2012,

  author = {Ricardo {Bedin França} and Sandrine Blazy and Denis Favre-Felix

            and Xavier Leroy and Marc Pantel and Jean Souyris},

  title = {Formally verified optimizing compilation in {ACG}-based

           flight control software},

  booktitle = {Embedded Real Time Software and Systems (ERTS 2012)},

  year = 2012,

  url = {http://hal.inria.fr/hal-00653367/},

  xtopic = {compcert},

  abstract = {This work presents an evaluation of the CompCert formally specified

and verified optimizing compiler for the development of DO-178 level A

flight control software. First, some fundamental characteristics of

flight control software are presented and the case study program is

described. Then, the use of CompCert is justified: its main point is

to allow optimized code generation by relying on the formal proof of

correctness and additional compilation information instead of the

current un-optimized generation required to produce predictable

assembly code patterns. The evaluation of its performance (measured

using WCET and code size) is presented and the results are compared to

those obtained with the currently used compiler.}

}

(From https://compcert.org/compcert_bib.html)

To view this discussion on the web visit https://groups.google.com/d/msgid/guaranteed-safe-ai/c9a0112c-2457-41c1-8385-b85905f4dc57n%40googlegroups.com.

[Quinn Dougherty]

thanks for all the insight and resources! I'll keep this in mind for future months (the people who showed up seemed pretty psyched about models that prove their own correctness)

Do people think it'd be spammy to just add the google group to the calendar event? i just realized that was a functionality. It'd be easy to respond "no" to and get it off your calendar.

To view this discussion on the web visit https://groups.google.com/d/msgid/guaranteed-safe-ai/CAKObCapX0AMTVUaL7xXVWMXroayDV44FY-n%2Bc%2BPxm1Jsntf%2BTQ%40mail.gmail.com.