2022-02-03 13:29:14 EST June Andronick: small technical question: I didn't get why the shallow embedding in ATC is "inverse"? It sounded like just normal shallow embedding.
2022-02-03 13:29:37 EST Greg Shannon: have you consider applying this to firmware programing?
2022-02-03 13:30:02 EST Greg Shannon: where HW semantics might vary
2022-02-03 13:30:08 EST David Hardin: How long until structs will be supported?
2022-02-03 13:30:43 EST Greg Shannon: yes
2022-02-03 13:30:57 EST David Hardin: Any thought on supporting Russinoff's RAC subset for h/w-s/w co-design?
2022-02-03 13:44:44 EST Alessandro Coglio: Dave, to elaborate on structs, it mainly depends on how they fare in priority compared to our things I’m working on.
2022-02-03 13:45:04 EST Alessandro Coglio: Good point/idea about RAC. No explicit thought on that so far.
2022-02-03 13:46:22 EST Raymond Richards: Please comment on Logika's maturity. Could I start building production code on it today? Is the technology baseline stable, or is there continual churn? BTW, in my current role, I have had very senior technical people patiently explain to me that embedded systems will always be implemented in C...
2022-02-03 13:47:12 EST John Hatcliff: The next section of the talk speaks to that to some extent.
2022-02-03 13:47:32 EST Greg Shannon: Ray, i hear the same about C-forever for firmware and microcodes. We have to change that
2022-02-03 13:47:51 EST David Hardin: On CASE, we routinely translate Slang to C.
2022-02-03 13:47:55 EST John Hatcliff: Slang is actually used in implement HAMR, and HAMR generates Slang, which is translated to C.
2022-02-03 13:48:35 EST David Hardin: Robby's tools do this translation automatically.
2022-02-03 13:48:51 EST John Hatcliff: The DARPA CASE Phase III demo carried out by the Collins product groups used HAMR (and indirectly slang) to generate modules of the CH-47 mission control software deployed on seL4
2022-02-03 13:49:58 EST Raymond Richards: Will you be making this video available?
2022-02-03 13:50:28 EST David Hardin: Also, Ray, these same people 30 years ago would've told you that embedded systems will always be implemented in assembly...🐵
2022-02-03 13:51:47 EST John Hatcliff: Regarding "forever C", we'll never get the tight/deep integration of formal verification that moves the world forward if we don't move to something other than C. We think we have a nice balance: a language designed for verification that can compile to C and that can interface with C. That let's us interface with legacy code while "moving the ball down the field" so to speak, with better language technology.
2022-02-03 13:52:11 EST Raymond Richards: David, I do believe that. When I asked why they think that the answer was simply, large amounts of legacy code in C, too expensive to start over. /*eye roll*/
2022-02-03 13:53:53 EST David Hardin: At Google, they're replacing C code with Rust incrementally as they find flaws in their C code. This seems like a sensible strategy.
2022-02-03 13:54:11 EST John Hatcliff: Again, because Slang can integrate (and compile to C) and because HAMR can work directly with C workflows (you don't even have to see Slang), you can gradually migrate from C, or easily do some modules in C and some in Slang.
2022-02-03 13:55:04 EST John Hatcliff: Ray, if you send me an email, I can send you a link to the video.
2022-02-03 14:00:59 EST John Hatcliff: Coming back to the maturity question, while Slang has been used to develop and generate code deployed in industrial contexts (at least by industrial research teams), we are still working expand Logika coverage to the entire Slang language. For example, not all forms of Slang/Scala for loops are covered currently.
2022-02-03 14:01:18 EST Renato Levy: mute
2022-02-03 14:04:05 EST Raymond Richards: John, are there plans for long-term sustainment of Logika? Perhaps through Adventium?
2022-02-03 14:05:17 EST John Hatcliff: While Logika checking in general works well and fast, there are some situations that you run into where the underlying SMT solvers bog down. The community would benefit from having deep discussions between people like us working on source level verification with people working on SMT solvers.
2022-02-03 14:05:21 EST John Hatcliff: A lot of times, the SMT teams drive their research and optimizations based on the SMT benchmarks and competitions, which have examples that are somewhat different in character from the SMT outputs produced by our program verifier. We are hoping to have some meetings with the U Iowa team to explore some optimization directions with CVC.
2022-02-03 14:07:55 EST John Hatcliff: For sustainment of Logika, I don't think Adventium sees their mission as a "tool / support shop". So we need to keep brainstorming about that. Of course, we would be happy to eventually create an entity, or partner with an existing small business to stand up something for the "long-term sustainment".
2022-02-03 14:09:43 EST John Hatcliff: Overall, the technology transition pathway that I think would be most of effective for us is: get people using HAMR with different backends using C development only, then show them Slang (we have a lot of nice testing, simulation infrastructure for that), then finally get them using Logika (whose contracts can also support randomized testing)
2022-02-03 14:11:03 EST Todd Carpenter: Ray, for the sustainment, we still have more to do to mature Logika. We've been pushing on real-world requirements driven by cyber physical systems, and uncovering additional research challenges. As John said, we're all looking at business-level options.
2022-02-03 14:19:45 EST Raymond Richards: Todd, lets connect outside of this event. raymond.j.richards@leidos.com
2022-02-03 14:33:00 EST Danielle Stewart: This is a really interesting application of the safety annex! When using the "fault" definitions as attacks, did you use the min cut set analysis, and if so, how is that interpreted in terms of attacks?
2022-02-03 14:33:05 EST Olin Sibert: Those MITRE and NIST catalogs all have substantial size, can CADA assist with choosing appropriate elements?
2022-02-03 14:34:02 EST Greg Shannon: What's your biggest challenge for scaling up in system complexity
2022-02-03 14:34:07 EST Danielle Stewart: Id love to talk offline!
2022-02-03 14:36:08 EST Danielle Stewart: The use of compositional analysis (via AGREE) certainly helps with scalability - as analysis is concerned.
2022-02-03 14:36:57 EST Danielle Stewart: Matthew, Gabriela, and Duminda: danielle.stewart@adventiumlabs.com
2022-02-03 14:56:30 EST Jerry Dussault: Welcome to Session#12. A brief schedule update: I believe Dr. Renato Levy will be filling in for Pat Hurley, to give the final presentation in this session.
2022-02-03 14:58:15 EST Renato Levy: That is correct, I will stick around after my presentation to give Pat's