and start the recording now and then i'll open up the meeting
Good morning, everyone. So this is welcome to the Nsf.
Common methods in the Ppi meeting from University of Pennsylvania, and I'm.
One of the organizers of this meeting and formal methods in the field.
It's a it's a program started in the set which has been going on for last 5 6 years, and we are very thankful to the program manages at any step. who started this program, and who have been supporting it over the
last 5, 6 years, and and then you know i'm not unhappy. So what's this program about?
So you know many of us, that researchers, informal methods and system design, and the questions that motivate us, and how to specify correctness?
And these are questions rooted in logical foundations, and how to verify correctness. Where?
We. We have been working on developing analysis tools to help us students.
But all of this research makes more sense and it's best done.
If we have some specific applications in mind and so that's why, that's the motivation for this formal methods in the field program where the field means a specific application domain, and the goal.
Of the program is to encourage collaborative research between researchers, informal methods and domain experts.
In in fields. and for the purpose of this Nsf program we have 5 fields, and there are 3 of them operating and distributed systems, network systems and embedded cycle systems.
And the applications of the methods in these areas that have been developed over the last almost 2 decades.
And then there are newly emerging areas such as machine learning and human centered computing, which are also part of this program.
And hopefully, at the end of this meeting we can also think of a new areas where requirement methods could be connected.
Just just a few minutes regarding the agenda.
So in the in this opening session we will have docs by
Margaret and Mattanucci, who is the assistant director of size, and within size.
There are 3 divisions so ccf is one of them.
So it's my desktop with the Division director for Ccf
The lead program director for this program should be the same few months, and then then, maybe that go move on to this term tangled, uniformed methods in industry. and and yeah, the tank phone to a 5
number. great speakers who have agreed to participate in this nicotine, and from Microsoft David from Meta.
Actually a chance from networks, from Amazon, and So 5 ppi meeting, we will have then 2 closed sessions.
So these are open only to the awardies in this program, and you should have got in a link to this.
The you know the word is when you registered for this.
So this is going to be in 5 panelist sessions.
So today 2 to 4 will be a session that there will be liking talks by your bodies, and tomorrow morning there will be an open discussion among the award is in this different groups on success. stories.
But challenges in their particular area and the new opportunities.
And these 5 groups will be led by Cindy Fisher and Jennifer in machine learning.
Diane Stepan, and they call it sandwich on in disputed systems.
Arthur and Kara to imagine in network systems embedded systems and thrust voting and delay in advancement, in human-centered computing.
And then all of you who have, you know, join this open session.
You are welcome again to join the closing session, which will be at 2 Pm.
Tomorrow, and the same link should work, and we will have again some remarks by the division directors of the other 2 divisions within size of the Intelligence Systems Division, which is led by Michael Litman.
And the network systems division, then by the deep thing. and, as you can see actually all the how the 3 divisions within size are interested in formal methods.
So this is this is really great for us, and then we will hear reports from the breakout sessions.
By the provided by the needs of these 5 sessions.
So that was about the agenda. And now, let me welcome.
Margaret Marguerite to a few months.
Thanks very much. Reggie can never hear me. Okay.
Can people hear me? We can hear you wonderful I had some audio problems.
But i'm back wonderful. So good. morning everyone my Name's Margaret Martinosi and I lead the computer and information science and engineering or science Directorate here at the National Science Foundation and I do so as a 4 year term while
on leave from the Princeton computer science faculty it's nice to see so many familiar faces here in what is such an important topic? area?
So, as many of you know. but just to sort of reinforce it.
Nsf is America's Major funder of foundational research across a wide variety of topic areas.
But nowhere is that more true than in computing where Nsf provides about 80% of the Federal funding for academic research.
And so obviously it's important for us to engage you the community as we seek to take that really long term view, identify important research opportunities and challenges across many different time frames from blue sky foundational research to other use
inspired and translational opportunities, and I think formal methods is a great example.
It has gone through such advances and transformations over the decades.
And the goal of this particular program is to move the needle into the in on those advances from foundational out into the field to really move the needle on how reliability and security and other topics get taken on in order to
really fundamentally rethink how we design and build different types of computer and information systems.
So some of you have heard me tell the story some of you may have all actually been players in the story.
But i'm a computer architect and so for many years I did the quantitative empirical computer architecture thing.
But there was a point about 6 or 7 years ago where one of my graduate students really pointed out some of the opportunities to to undertake research using more formal methods, and I was schooled in the matter
by him by the students that followed by some of my colleagues who are here on the zoom today.
It has been for me a really transformational set of years to learn about this new tool in my toolkit, and to sort of think about how it can be applied across many different security and reliability. scenarios.
And so I think what you are doing here today is sort of part of a sequence of many people who, learning because of the work you're doing about these kinds of opportunities from 2,018, and before where there were workshops sort
of standing up this program to where we are now, after a couple solicitations, really recognizing the way that industry is deploying formal methods. The way that these things are getting taken from theory to practice, I think the goal really
is to keep it up. and to make sure that the cross pollination of different topic areas occurs so that the topic areas that are really well versed in this can help train the ones that maybe aren't doing it as much to keep making
that ongoing progress towards our towards our Goals and so with that I'll hand it over now to Dr. Dilma de Silva, who's the lead division director for formal methods in the fields who will
say a bunch of thank yous i'm i'm going to sort of say a blanket thank you to the program officers and the members of the community who have brought us here together today, and with that Delma over to
you. thank you, Margaret, so i'm zoom with the sofa.
I, am a rotator. My home is suspicious. Texas Am.
University. I joined 3 months ago in the i'm really excited to learn more about the formal methods in the field as a pi.
I really admire the program, and and I followed in my own research area the papers that were coming across, and the progress that was done in operating systems in particular, which is, I follow, make me very encouraged to be able to work with the
program directors who are so excited in order to nurture this community.
So, as Margaret said, by role here is a really farmer, because I got to say thank you, and you know it's really nice, is, I think, Thank you.
When we mean so much, because thanking the program directors gives me the opportunity just to also highlight.
How wonderful it is to work with all of them so i'd like to thank Nina Amla because she pioneered all this effort.
She continues to be enthusiastic about the role that formal methods and formal methods in the field can have and improve our society, and and she takes every opportunity to sell to sell the program to whoever wants to listen
and in the computing and communication foundations division we have an integral energy Dummy, then Chef and pavita praba car, and these are Pds.
That I work with daily, but I also work with my colleagues program directors at computer and network systems.
We have Jaso Halstrom, Daniel Loggeda, Augustine absent, and finally in Iis, which I always forget.
If it is intelligent information. Sorry, Michael, You have confused bit more because Michael sometimes trips on the name of his division.
So I, as we have done mostly in waiting. So thank you so much for the program.
Your actors in my 3 months here, and my admiration for the work that program directors do increase.
Of course I love them as a pi but i'm really in of what they work for.
Our what they do for our research community. I end up.
I saw the rest. cleveland isn't the obvious I couldn't find Kosal russell Rao. but I think he's also a meant to be here.
And so let me really thank the form of Ccf Division directors who work with the leadership to allocate funds and really nurture the work group that now continues to work with the api So rest
and cause a Roger. Thank you very much for laying out the in the beginning and getting this going, and I hope you know, to be able to like you.
Continue to nurture this community in terms of up the commodity itself.
I'd like to really thank raji valor from U Penn for being, you know, the chair and organizer of all of this, and for the 5 amazing session the session that we have planned for today and for
tomorrow. I'd like to thank for machine learning sunshit session and Jerusalem for operating and distributed systems.
Nickel is out of each, and they and Stefan for networking art, Gupta and Ratu Mahjan and for embedded system.
Cyan Metra, and, like me, Jose and finally for human-centered computing Raspberg in Elena Glassman. Sorry if I miss pronounce too badly your name but really thank you and i'm looking forward
popping up in many of those sessions, and and and hearing the discussion from the Apis.
Finally our audio minist staff, Antonio coordinates Anita Tyler and Nato.
William really worked closely and made all this happen. So thank you very much.
And of course, thank you also the it support that we are all you know benefiting from now.
So. Thank you. Thank you. Thank you. pavitra!
Nina, I passed to you so that you go to the next person
Great. thank you, don'tma and margaret for your remarks and reg for your intro alright so i'm puppetrack rabaker i'm a program director in the computing
and communication foundations division, which is within the computer and information, science and engineering direct rate.
So Dilma is our division head and Margaret is our directed, and i'm a rotator from Kansas State University, where I do research on cyber physical systems, formal methods.
And ai. so applications or formal methods to Cps and Ai.
Essentially so, Michael today is, to give a brief overview of the kind of awards that we have done as part of this program.
And to briefly talk about the goals of this Pi meeting.
So You've already put it. very Well, the formal methods in the pro Fields motivation was mainly based on the statement from Miller's thesis which emphasize this bidirectional
interaction between theory and practice. We want theory to be informed by practice, and we want practical systems to be built based on strong theoretical foundations.
So there was this market divisional effort within size, and where the Ccf.
Cns and is division came together to support this program, whose broad motivation was to build reliable, robust, and resilient software systems as well as to build this community of researchers that could support this aim where we had
researchers from formal methods as well as those from the fields, working symbiotically towards building, towards doing research that enables reliable and resilient software systems.
So we are currently in the second iteration of this program.
And the next call, which is the last call as part of This iteration is in February of 2,023, and Raj. you already touched upon the 5 areas that we have been it's soliciting proposals in as
part of this program, which is machine learning, operated distributed systems, networks, embedded systems, and human compute centered computing.
But we have all this encouraged proposals from field areas which are beyond these 5 that have been listed, and I will.
I will touch upon those as well. So I want to give a brief overview of the kind of or the breadth of topics that have been
Funny through this program. So here is an overview of the different
This chart basically summarizes or clusters the different words that come up in the titles of the awards made so far, and you can see that all the 5 areas are very well represented.
In this picture I will flash a slide for each of the areas.
Just to give an example of the kind of awards we have done so.
For instance, in networking we have a formal method.
Various kinds of formal method techniques being investigated through program synthesis, verification, satic and dynamic analysis being applied to different applications of networking, including generating update controllers verification of condition control
algorithms and monitoring of data planes, and so on. When When we come to operating systems, again, we have verification methods based on types, systems, smt solvers, symbolic execution techniques being applied to verify operating
systems as well as composition techniques being applied to verify distributed systems.
In the context of machine learning, we have awards that these would explainability.
We have awards that look at efficient transformations of neural network or market architectures to enable scalable verification as well as specification and verification for newer classes of system machine learning, systems like generative
adversarial networks, in fact, with applications to things like medical imaging, and so on.
In the context of embedded systems we have formal methods being applied to autonomous and semi autonomous vehicles, using some advanced predictive analytics verification of embedded system
compilers and verification and program synthesis being applied to hardware default analysis In the context of human-centered computing.
Again, we have formal methods being used to eliminate and minimize human interaction errors.
To build software tools that can help people interactively program and correct back construction, kind of methods being applied to experiment as design.
So these for the 5 areas. But in addition to the traditional research programs, we have also funded.
Summer schools and transition to practice a kind of proposals that advanced tool building.
So many of us. No shankar network has been running the formal math at summer school for over a decade.
Now, and in the last few years he has also organized the formal methods in the field boot camp.
Along with these summer schools, which aim to train students in the applications to formal methods, and this has been an extremely beneficial event for students all over the Us.
Especially for those that come from institutes, which don't have a strong formal methods group, or who don't have access to a lot of formal methods courses.
So we We are truly thankful to Shankar for organizing this events, and this is a great
Give back to the community. So, in terms of the transition to practice a kind of proposals, we have tool.
We have supported tool building efforts in the area of neural network verification into integration of smt solvers to proof assistant formal reasoning for legal conveyances.
As I said, this is just you know, a pick and choose a couple of topics that from the wide range of proposals that we have funded, and in addition to the 5 areas that we mentioned we have also funded proposals in
field areas like synthesizing quantum circuit compilers.
The verification of computational physics and synthesis of microfluidic chips.
So finally, to sort of summarize the goals of the Pi meeting.
We are here to learn about the different projects that have been funded.
So we have lightning talks. being given by almost all of the awards from the program.
We look forward to cross fertilization of ideas.
We have experts here, from formal methods broadly defined as well as the field areas, and really look forward to collaborations and cross fertilization of ideas.
And finally, we are looking forward to identifying challenges and next steps for the broader adoption of formal methods. And we hope to see a lot more discussion on this during the breakout sessions.
And yeah, we look forward to interacting with you today and tomorrow.
Thank you. and I think back to Regina
Yeah, Thanks. Thanks. So I think we are about 5 min ahead of schedule.
But the but let's get started with the next next item on the agenda, the the industry panel.
So we have 5, and this So let me actually just bring up Max Slide 8
Yeah. So So this this panel brings fun with my test experts who are currently working in the industry and trying to transition some of the ideas in common methods to actually impacting the practice of system design
in in in the street, and super. So let me just introduce them, and then we will have short presentations by each of them.
And then they will have questions announces, So the first analyst is a nickel. My owner.
Who is at Microsoft Research. So So Nikolai is work with but the empty solvers, particularly one of the designers of Z 3, which is used widely, and he has been working with applications to
network systems recently. Alright. So thank you.
Our next panelist is David Jeff, who was a professor at Stanford for many years, and is now at Meta, and he has been developing business.
Building a group cryptocurrencies and reliable programming.
Thank you, Dave, for participating in Theana.
Actually, Iraq is at math books and action is working on, designed to embedded control systems and cyber physical systems.
And he has been trying to push on the methods and products which are used widely in the in industry.
So, thanks actually. but Inevita, who is a leader at aws
So the end of Us program group is now kind of a good to place for many of the internal methods.
And they have been working on. Okay? how? how do they? How to give security guarantees in in cloud?
You think and thanks they have for taking time to participate in the panel. And what is the game for?
You know. Oh, who has been working on programming that take me on for many decades, but is now.
I had set around trying to transfer some of this technology to Oh, the distributed systems and smart contracts.
And thanks. Thank you for joining. I saw. So the plan for the you know, for the rest of the session.
Is that each each one of them will give us Some of the sexes can formal methods in that industries of some of the challenges.
And then also some of the opportunities and advice to academically.
So just in this area. if you have any questions please type them in the chat.
So i'll be monitoring the chat and you know i'll ask them at suitable times, and after the presentations.
We also have, hopefully, time for an open Q and a session.
So me so, Nicolai, do you want to go first?
Yeah, Can you allow me to share my screen? Thank you.
The slides up. Yeah. Okay, So I i'll try to keep it with 10 min.
So So former methods from the perspective of Microsoft research research software engineering comprises of a large number of tools, and we have over the years built tools and interacted with product groups and external on
deploying and using these tools so here's an overview of the range that the tools target, so they they target areas from designs to implementation testing deployment, and and also aspirational diagnosis
and the the tools listed below the line are mostly recent tools.
That's a longer history of those and and also the the tool that I mostly work on is not listed.
Here is the underlying most of these tools that's switch somewhere on the side is not directly tied to a scenario.
So a summary of the various areas that Microsoft Research groups have been involved with This is given here in the following slides: Okay, go over them in in more detail.
But just from the overview there's, some major areas of symbolic model, checking and model-based testing of model programs, systems, code, verification, concurrency, testing, fuzzing, and network with So symbolic model
shaking started with the slam project around 2,001 and 1 one thing to
So. So the impact of that was in in shaping in the static driver. Verifier
But one thing to notice I want to make an notice of in this overview.
Is that it was influenced by work developed in academia.
So predicate abstraction influence the the way that Islam static driver verifier operated.
Similarly, there's a thread around a constraint work closes.
And the solving methods were that that i'm employed in set threes or cost solver were influenced by collaborators.
On on ic 3, and there's another angle, which is that the current home class solver is is is a component of set 3, but also it developed in academia.
So there's an academic angle in an insider.
Now model based testing has been pursued as long in different guises the 3 most recent are called Bask Iv.
And sin The targets various different domains past Targets Cloud Api Contracts Iv.
Targets Iv: rfc's specifications and and basically does specification exploration and sin is used in network verification.
There's the systems code verification has been very prolific and with 2 angles, one based on the boogie tool chain that has given been foundation for many program verification. tools.
It's a verification condition, generator but it's There's a different thread around that takes a starting point functional programming and logics and that's a has been a a threat with if star as as a
main language, but there are many others. one of the Miros is targeting a rust verification.
For example, this very recent collaboration with Cmu and Syracuse?
So some of the one of the success stories I like to talk about in the context of the verification is the use of probably correct low-level parser.
So prior to deploying the hypervisors with ever parse.
Historically, 30% of the bugs that were uncovered or have been uncovered in the hypervisor, which have been in the parsing.
And now they're none. there there's also a thread around cryptography and and here's a chart of verifying assembly code versus synthesized cryptographic
code. So this this assembly call is almost half an order of magnitude faster
In terms of throughput than the then the high label, Cryptographic Primitives.
But this also verified So that has had impacts both in Microsoft and Non Microsoft products.
So, for example, there are components of the Linux kernel and firefox browser.
Using these verified cryptographic and libraries concurrency testing again.
It has a prehistory of with very soft and and spin that aimed for stateless resp. enumerative state space exploration, and within microsoft it has a
evolved over a different technology. So with chess and cars systems, it evolved from using systematic schedule expiration into randomized scheduling.
The main tools today are called torch and Coyote.
And they target development and testing modes. So coyote, just, in short, is deployed since 2,017.
First it was had a self-contained language for state machines.
They need was in 2,000 made dot net intrinsic.
So you could that programming dot net and more squeezedly.
Your target C programs is used in various clouds services.
Torch is used in is an internal tool at coyote is open source torch is internal runs for testing it.
It re it reverse engineers concurrency primitives to say it's in a rough way, and it's one.
It finds box for various agnostic of the applications fosing again
And a started with dart and cute
And it is this day going strong, with a wrestler and and hyperfos that I will just mention.
Briefly, Wrestler is a api forcing tool that fuses web services.
It's open source. hypervisor is an internal tool that was built for fuzzing the
Again the hypervisor virtual machine it uses symbolic execution and and set 3 theorem proving to find bug paths.
It found 11 bucks and and that's in a in a component with a bounty is a quarter of 1 million dollars.
Network. verification is a larger area that where we have invested to the past decade one of the tools takes routing forward in in in data centers with lots of queries of correctness checks done
on the fly every day on hundreds of thousands of routers.
It. and your development is a domain specific language for writing these checkers.
It's called zen spark isn't is a way of getting configurations.
And these tools are then integrated in a what's called a network change verification system that is used in deployments of new configurations so-called network repaves which are major sources of potential
major outages, and so far it's been running in a couple of years now, and the verified hundreds of migrations, and prevented outages every quarter.
It prevents. what could have been significant outages so that's my summary
Thank you. the the call, if you have any, give me a question when you collide, is, you know, type in in chat. but we will have also plenty of time for our questions how about specific
documents, but also, you know the broader questions about adoption of formal methods.
At the end of all the talks we will have vital discussion.
So yeah, I I don't see any talk so let's let's move to the next month.
So yesterday your next
Hi! I realize I've usually had a struggle getting the slides to show in the right way.
So. let me quickly I think maybe i'll just get presentation mode, and so show the the slides is there edited?
Hang on a second. Okay, So actually they would set it slides.
There are 2 questions for you as a from June.
Does Microsoft use only their own tools what about other open source tools?
I I didn't catch the last part of the question with my Microsoft users.
What Do you just use your own tools, or do you also use other open source?
Microsoft uses open source tools. I I presented it from the perspective of Microsoft research that develops tools as well.
Microsoft as a company uses open source so for example. there's an infer there's an infer adaption, which is from the major as as one example.
And then answer the question, how do you handle training? But, efforts in Microsoft training depends on.
So so depends on the tools and groups, so for example, they're training in Tla plus driven by Marcus Cooper, who develops an old steel a plus tools. there.
So some of the interactive tools have associated training on others.
It's more peer pure training or period oriented.
So there's no training for set 3 for example. Okay, so is my is my screen halfway legible.
Yes, yeah, we can see here at the screen. Okay, so I can't give a sweeping overview of formal methods work at at Meta.
I have been. it is not as extensive as Microsoft or Amazon which are really the industry leaders and applied formal methods, at least among large companies.
So there are scattered efforts here. and there and i'm going to talk about what I know, and the project I worked on for 3 years, which is the development of the Move prover, which is a formal verification system, for smart
contracts, and so i'll give a little background on where the project came from.
Talk about what we did, and some of the things we learned.
So. yeah, So i'll mention also that I can't claim that this is and on ambiguous success story, because, in fact, the project was was cancelled at meta i'll talk about that a little bit
more. but the move prover still lives it's an open source project, and it is being used by some Spin-offs from Meta and other companies that are using the infrastructure that we developed so this was part of
the Libra Dm Project at Facebook which there's a lot of renewing that's got on here, which is already a bad sign.
But at at Meta now and so and I think 2,018.
There was an ambitious project conceived, and I think it was launched in mid 2,019, with great fanfare, and got a ton of publicity.
So it was to build a blockchain to serve the financially underserved.
So more than half of the world population. doesn't have bank accounts, for example, and we were targeting people who are not served well by the current financial system. or That's what we hope to do.
And so we built a system from scratch, a whole new blockchain, whole new cryptocurrency, based on large-scale Byzantine consensus.
No proof of work. We developed a new language for programming smart contracts called the Move language, and that was intended to be formally verified.
And so, as part of the project, we developed the move prover i'll mention that the interest in formal verification really came from one guy who's leading the manager who recruited the team to do the the language and whatever and I
think, you know, I went around our organization at some point and got questions from senior engineers like what's formal verification.
So there's kind of one visionary who was pushing for this, and recruited and assembled the team to work on it.
The project was ultimately never launched. It was actually formally canceled this year. the reason seem to be non-technical.
And I they're above my pay grade so it's regulatory problems of an unspecified nature.
But the system was fully open source, and there are 2 startups that are both supposedly worth over a 1 billion dollars.
Now The form from the technology and some of the staff of the project and the move language of the move prover are still used by these startups and a few other companies outside Meta.
So I wanted to. You know I spent a lot of time thinking about what we were trying to do is hard and their their known failures.
And so why did we think that this project might be successful?
One of the reasons was the need for it. So that already been a track record of hundreds of millions of dollars in losses from bugs and smart contracts, and those losses have escalated since then.
So. So there's basically smart contracts in a blockchain, which i'll say for people who aren't into blockchain land is just something that updates the state of the blockchain.
So basically the most important financial transactions are handled by software which are called smart contracts.
So that said, These things are a high assurance system by which there are many definitions out there.
I will say something that is designed to have a low likelihood of major failures, which in this case would be inability to use the blockchain, or, more importantly, large financial losses.
So blockchain should be and aren't always high assurance systems.
There are large amounts of assets. at stake transactions are hard to reverse compared with banks or the traditional financial system.
It's the kind of usually open source and whatever so it's likely to be targeted by highly motivated and well-resourced adversary.
So you can see the complete design of the system, and there have been large losses already.
The Move programming language was conceived by others at Facebook.
It was already well under design by the time I got started and It's a programming language for implementing smart contracts on the Dm.
Blockchain. It is designed for safety. not specifically to enable formal verification, but the formal verification team had some input into the design of the language.
A module and move can only be call. You can only call modules that already exist, so that eliminates
A number of problems, including the ranchancy problems that are famous in more traditional blockchains with the solidity, programming language. And one of the most novel thing about move is a resource type which models physical
assets. So it's a value that cannot be deleted or copied outside of the module that defines it.
So the move Language has limited expressive power which is good for formal verification.
People there are references, but they can't be stored permanently.
They're only they can only be kept in local variables and passes parameters there's really effectively.
No aliasing which is enforced by static analysis of the programs.
There are no first class procedures and no dynamic dispatch, so it has fewer hard problems than many languages for formal verification.
The move prover is really a traditional employee, horse-style, verifier.
So the idea is that you write specifications in the form of pre conditions, post conditions.
In our case, global invariance. and for the move prover, the front and technology dealing with the semantics, the language.
We implemented our group, but we made heavy use of off the shelf technology, and in fact, the project would not have been feasible without that.
And so we relied on existing S. and T. solvers, particularly Z.
3 and Cvc 5, and the boogie intermediate verified language.
Yeah, which we may change as to Boogie and We worked with a Clark Barrett's group at Stanford, and the group of the University of Iowa, to get changes in Cvc 5 to make it more
suitable for the task. So this is a really hard project.
I mean people have been working on floyd horror verification since Floyd and Horror were inventing it.
And so that's something like 60 or 70 years and it's tough. but we felt we had some keys to success.
The the make it worth ItNo. Only today. Okay. please.
Mute, I guess. So we were starting with a clean, slight which is pretty unusual in industry.
We tried to avoid problems with verifying traditional software, such as programming languages that were very complicated or ill-defined.
We weren't dealing with a legacy programming language in this case.
I was pushing for a methodology, and I may not have been successful where we verify as we go.
So instead of somebody designing and writing code and then tossing it over offense for a verification team to work on, we hoped to have the verifier be a part of the development process, and in a lot of the world
There's not that great a concern with bugs but there's ample reason for people in the smart contract world to be concerned about bugs, because the losses are quantifiable, and have killed many businesses and so we are also
co-designing the tools, the problem, programming style, and the verification method, dialogy together to try to maximize our chances for success.
So the results of the project at Meta. This is before
It started being used externally. Where do we? All of the the really the business logic and the the foundations of our blockchain were implemented in the move programming language, And we wrote extensive specifications for the move
infrastructure. So it's called the Dm. framework, and so we specified and verified all of the access control requirements for which there existed a public document.
And the specifications pointed back to that, and we found several bugs in the process of doing that had much more confidence in our access control.
After doing it. we specified and verified the documented abort conditions and transcripts.
In transaction scripts we so in a blockchain.
Transactions are atomic and can abort. and so we check that.
The documentation was accurate, and we specified many other properties as well.
What we're most proud of is that These specialifications could be used during continuous integration.
So anytime that somebody checked in their changes, we would rerun formal verification on them and flag anything where a change in the code or a change in the specification or anything else in the environment caused verification to fail and so
verification worked reliably enough and quickly enough that you could just push a button.
Wait a minute or 2, and it would finish so this stuff is all open source, and it's all out there in github repositories.
I think it's called moved, dash language at the moment the prover source code is out there, too, as is documentation.
I still think it's in a preliminary state or other people using it, and I, I wish the project had been able to continue for a couple of years at Meta with the working on it, so that we could have taken on some
of the remaining challenges. So let me talk about some of those challenges.
So. You know. One of the great things about working on industry in a project is that you can't dodge problems.
I mean one of the great things about working in academia is, you can redefine the scope of your research to do whatever is most likely to have the maximum impacts in industry.
You. Finally, I have to confront all those problems where you in my case.
I've worked in both kick the can down the road in academia, so we don't want to worry about that problem.
You'd actually have to worry about it in industry so I feel that this kind of formal verification where specifications are written.
And you're actually trying to prove the correctness of code has to be part of a programming the program development methodology.
So systems have to be designed for formal verification. the hardest thing you're gonna do with a program is formally verified.
And so the programming language and everything else ought to be optimized for formal verification.
Not something where you write it for speed, or you know ease of programming. and then let somebody else deal with the formal verification problem, because that makes formal verification even harder when it starts off being the hardest problem.
So i've looked at the design of safety critical systems fairly closely in another context, and it's like incredibly costly.
It works, you get systems that are actually safe, say for avionics, but at incredible cost in time and delay.
So I think the challenge before us, in formal verification for critical systems is to figure out, How can you do it at?
You know, necessarily more cost than normal development processes, but at a fraction of the cost that the methods we use for safety critical systems entail
So other challenges. you know, you got, in this case a system which requires somebody to write specifications, writing, debugging, and testing of coverage and specifications is is something that at least in the software area is not an advanced
art, and we put some work into that. we would have put more work into it, and it's an area that I think deserves further exploration.
I think we had some fairly good ideas for that. They were preliminary.
We just had them explored by an intern smt!
Solvers still are not perfect. I mean we're relying on 20 years of prior work, and actually truly amazing programs.
I got in on the ground floor working with smt solvers and I really can't believe how much better Z.
3 is than the it was, you know, 10 years ago, or the the programs I used in the past were so.
Those advances enabled this, but there were some deficiencies, and we were surprised to discover the reasoning about vectors was actually difficult, given.
How commonly used vectors are in programs. One of the things we did was collaborate with the Cvc.
Team at Stanford and the University of Iowa to develop a special theory of vectors and supports concatenation, and as well as indexing into finite length vectors.
And they actually published a pretty good paper on that last summer.
Generating small, meaningful counter examples. is still a challenge, or was for us, anyway, and one of the things that's frustrating is when you know, for example, Z 3 has really almost magical ability to deal with quantifiers I thought it
was incredible how well it worked, but it doesn't always work. and sometimes the the problem you get is a timeout and so trying to figure out why something is taking a long time in decision procedures.
So you can figure out what you might be able to do to to fix it is very, very hard, and I think, support. Better support for that in smt solvers would be very welcome for the intervened language boogie
boogie once was also for us something that enabled us to complete this project.
I don't think we could have done it without it, but we did struggle a bit to present good counter examples to our users, and sometimes extracting that information from Bogey was not as easy as we hoped it would
be, in fact, shares. Kadir, who had some experience with Boogie in the past and was on our team, made changes in Boogie to improve our ability to get counter examples, finally is the issue of time and
patience and development of these systems i've thought about why haven't formal methods had even more impact and achieved the dreams that people had 30 or 40 years ago, and i've concluded that a lot of it
is. It's just hard and I know I have ideas for how we can solve some of the longstanding problems with application of formal methods, particularly for you know straight.
You know what we were trying to do in the move pro, and is trailing 10 or 20 years behind the kind of research that was described in the formal methods in the field program.
But still not all the problems are solved. And yeah, the technology that we use to enable this project was developed over a period of 20 or 30 years.
And so I think that some of this is just gonna take if it's ever going to be have the impact we would like He's gonna have to just take more resources and a sustained effort you know sometimes that's
what's required to get over the hump with something I feel that's where we are with formal methods.
It's a little difficult to justify in an industrial context, or even in a government funding context.
Any experience in academia I wanted to get. This is my last slide.
I wanted to give a shout out to the previous work in this area.
So in itself, I think. Well, it is. have provided my first funding.
When I was a junior faculty member and provided a lot of funding on on the way.
Nsf. is the most visionary funding agency, and as a university professor I found to be the easiest to work with.
They understood research and out, worked in universities and maximize the the productivity impact of university researchers.
This. This work is is based on as i've said Decades of government funded research much of for men as F. a lot of it from Darpa, and from other sources as well.
There's a huge contribution of Industrial research goes well beyond impact on the companies doing the research,
Particularly Microsoft, which we use very heavily. before Microsoft.
Some of the people who developed this technology we're at universities.
Some of them were a decade systems research. center I guess it was in Palo Alto which we collaborated with a little bit a long, long time ago. I don't know the deck ever benefited financially from that work but the world
certainly did and work at Sri International. So the benefits.
Yeah, these these things benefit of the world and we're really Lucky that these companies have chosen to do this kind of work.
Sri International is a government contractor, but the other ones I mentioned. I should include Amazon in this list because I know they're doing a tremendous amount of work and exporting it to the world.
We didn't happen to take advantage of that in our project but I should have included it on the slide, and did not, and finally see, people on our project and on industrial projects in general are all trained and supported by or
generally by government funded research, often in the United States.
And you know, it would be really interesting to trace any what back from any one of these projects, and where the technology, and particularly where the people came from, and how they were trained, and how they were supported But i'm pretty confident that it would
all get back to Us. Government funding agencies in many cases, although one of the key members of our team got his PHD.
In Germany, where his research was funded by, I believe, the German Government
So I wanted to acknowledge the explicitly acknowledge the contributions of government funded and industrial research to the effort we were trying to do, which was completely necessary to enable us to go
forward. Thank you, thank you, Dan. hi, betty quick questions before being one to the next. Yep.
It's again. Yeah, if you have any questions ?
I'm So yeah, I guess the because actually your next I'm trying to figure out how to unscreen share.
And now i've lost my window is that gonna cause a problem, or can somebody else do it for me?
Do you see? Stop here somewhere
This is ridiculous. i'm sorry i've lost my zoom window somebody has stopped sharing to stop cool.
I pick up the icon. There we go. Okay.
Okay, you guys are okay. i'm not taking over the screen anymore. yeah, Actually, you can share your screen.
Yeah, Yeah. Can you hear me? Okay, And can you see my slides?
Okay, this is good. Yeah. Thanks. Okay, So let me start my talk by thanking the Nsf and Raji for for this wonderful panel.
And special thanks to myself in particular, because, my PHD research was funded by National Science Foundation.
A large part of it via what was then the goalie program, grandpa? opportunities for academic teasers with industry and Toyota was the industry partner on that particular project.
And so I really command Nsf for continuing to fund this.
This line of research in this important area that bridges the gap between academia and industry.
So the outline of my talk is gonna be i'll. i'll maybe take a couple of slides to put some context about verification and validation at mathworks, and then talk about the the 3 things
that we have been requested to talk about, which is the success stories challenges in our future case.
Okay, So those of you who may not know what math works is we are.
We are 2 developers, and probably the most famous tool that comes out of networks is Matlab.
It's a graphical, it's a programming language, but algorithm development, data, analysis, visualization, etc., based on linear algebra.
Then there is simple languages or a platform for a block diagram modeling environment for design, simulating, analyzing and testing systems.
And then there are more more than 2,120.
Add-on products that build on either Matlab or civil link, or both.
Like the competition toolbox here. So in terms of new number of users, we have, you know, over 5 million users in the world, basically pretty much. And we are lucky to have users both from industry in
terms of, you know, aerospace and automotive shown here on the slide as well as you know.
Lots of lots of users from Academia as well, and some of the trade-offs. that that sort of get discussed are have to do with You know how to bridge this this whole spectrum of people who build
established products that require, you know, rigorous tools to complete their workflows as well as you know, those who are building sort of new groundbreaking and breakthrough research.
Ideas. So, on the one hand, you know, there are concerns about what is even possible to solve, and, on the other hand, you know, making tooling and and and what we provide more robust and user ball, etc.
So verification of valuation at mathworks has to do with basically lots of different products and and supports several different workflows.
Some of them use formal methods, others are more practitioner oriented.
They are more principle approaches I want to acknowledge that polypace and simulating design verifier, are a couple of products that do use formal methods, but they are not the focus of
today's presentation so what I wanted to talk instead about today is a couple of recent success stories mainly on the specification side.
One is specification, formalization using temporal assessments and the other one is specification modeling using deployment stable block.
So let's get right into it for the specification formalization.
Recently we've seen in the research community at least on the sort of embedded inside the physical system side that, using temporal logics or formalizing specifications in general helps uncover mistakes and what you see on
the bottom left of the screen is an example of the kinds of mistakes that it can uncover; that one being from a a model from Toyota.
Oh, at the same time. basically, this use of symbols and vocabulary for for temporal logics is really hard for for industry practitioners.
And this slide comes from jordan's first slide from the Fcc.
Keynote from 2,015, and this still rings true. right.
So what we have done in the recent past is basically taken that approach, where, we have tried to combine the best of both worlds.
Where, we allow users to specify temporal properties without really having them to specify temporal formulas.
So we have developed this Ui as part of simulating test manager, which is part of simulating test which lets you kind of fill in the templates for specifications and talking with our industry.
Customers, I mean most of our specifications are of the for trigger response.
So there is some trigger, and eventually there is some response.
Oh, right! And so you can just fill in the various components of this formula template, which is, you know, the pre condition, the temporal nature of it, of the response, and the the response itself.
And then you can basically iteratively fold this expression to read it like an English language sentence.
So you know this is more familiar to the practitioners it's it's familiar.
It, because it, you know, reads more naturally like a English language sentence, but it's a valid logical formula, and you can use it to to test whether it it it holds and again, this is
this is an example that shows a painting test result.
So there is a graphical and textual explanation of the top, and at the bottom, you see.
You can zoom in temporarily as well as i'm porting the expression tree to uncover where the mistakes are.
And so one thing i'd like to highlight here is the sort of 3 3 level answer shown on the top of the blocks here one that shows fail pass and untested, and that's because for for
practitioners. when the precondition is false, then the formula evaluating vectors due to true, you know, does not mean sense.
So we had to basically show it, you know, does not make sense. So we had to basically show it.
As satisfied only when the pre-condition is satisfied and the rest of the time is is kind of shown as untested.
So those are some of the trade-offs that go behind the scenes in terms of introducing these to the to the community, and more for more details.
I would refer to our tool paper that came out in runtime education compounds of last year.
So. let me move on to the second success story, which is about specification modeling, using requirement, stable block and the workflow.
There is that you want to verify the requirements themselves before you have put together the design model.
So really making it early into the design design cycle. And the stable talk is basically a sequence of rows which had each have a precondition and a post condition.
And it basically says, If condition is true, then requirement, that the output conditions through our post-condition store and optionally has some duration which means that you know the the input condition works for 10 s And So
The benefit like, I said, is that we can really do this before even the design model is built.
And we can analyze this set of requirements together.
To to check for things like. Are these requirements consistent with each other?
So what that problem turns out to be is basically a Smt problem.
So consistency is basically can these requirements be satisfied together?
And the negation of that is basically is there a setup input combination.
It's a combination of inputs for which no matter what combination you choose.
You can always find a you know a way that the requirements are are false.
So there is no design that you can Come up with that'll make them true for that set of inputs right.
So that's a pretty strong check that We can do. And we can turn this into an smt query. and then if that smt query is unsatisfiable, then the answer is the table is okay, because the negation
is unsatisfiable. and if the negation is satisfied, then you know, that becomes a counter example for the for the analysis.
And we use actually z 3 for this smt solving.
And here is a account for example, how it's shown to the user.
Basically, things that are inconsistent or highlighted.
And in this example the inconsistency is that, under a normal operating condition and under an emergency subdivision something that checks the locking variable to it basically requires them to be both locked and
unlocked at the same time. So this is not possible, no matter what kind of design.
You come up with right so so that's the example of the kinds of checks.
This can do. There is also a completeness check that this table can do.
But i'll not go into that today. the other workflow is when you have a design model.
How do we check sort of that? This particular design model satisfies the the requirements the earlier was like any possible design model, right?
And now we are talking about this particular one, so that one is a model setting problem.
And then we send this out to simulating design verifier, which can formally correct a formally basically find a counter example.
Whether for this particular model, you find that these requirements are not satisfied.
And an example is shown here where a couple of rows are shown together, and then there is a hyperlink to the counter example that you can use to debug either your design models or your requirements
themselves. So with that, let me briefly talk about now.
Some challenges based on what I have seen.
And then move on to opportunities. And I chose this order because I want to.
You know, finish on, and you know, positive note of opportunities.
So challenges remain. in terms of system, complexity, basically.
So this heterogeneity of modern formalism was a topic of my PHD.
Thesis, and this it's still a bit of an unsolved problem, I would say, and to to you know, make it more interesting and challenging.
There is more learning elements that are into the mix which is making analysis even more difficult to to basically reason about the correctness of the underlying system.
When elements of the model are across, you know different kinds of formalisms, and they make interdependent assumptions on each other.
Right. So there are some still challenges about solving this problem.
To add to the mix with the advent of intimate of things and industrial Internet.
And all these paradigms you don't know where exactly the model is some elements might live on an edge device next to and an embedded physical asset.
Some might live in the cloud etc. Right?
So how do we put together something that is compositional?
And works across different platforms and and and infrastructure where the the model elements live.
And last, maybe you've seen recently that the model based design approach, where models you know, are used for at the design phase is now increasingly turning into a model based operations where models are still used in operation
and you've seen this sort of devops workflow of, you know, continuous integration and continuous deployment.
That makes the questions about. Can we do sort of incremental verification?
David, touched about it a little bit. but there are, you know, problems to be solved here about.
You know, What can we do about you know making sure that earlier analysis still hold and and things like that. for the opportunities let me maybe focus on ai enable engineering systems which is the recent trend where people are
using Ai enabled blocks into in engineered systems.
So as part of symbolic, we have introduced, you know, blocks that have Ai elements into them, from either statistics and machine learning approaches, or some neural network approaches or reinforcement
learning as well as just you know embedded C code, which is which would be say using computer vision kind of algorithms right where you can exercise, you can use them to exercise them as if it's like any
other symboling blog to to make sure that your analysis is working.
Okay, and it's buck free right but the challenge Here is that specifications, especially for more specifications is, still a hard problem. and people are mostly doing sort of robustness style of analysis on these neural networks where If you port up the
system a little bit can you, guarantee something about the output of the network?
So in that period. this is very recent work.
So this has come out as a support package maybe one or 2 weeks ago. it's called a deep learning tool.
What's verification library and it's based on this work out of eth zoom that came out in purple of 2,019 and the kinds of things that this can do is you know
given a network and some limits on my input participation.
What is my output? perturbation, etc.?
And I just want to acknowledge that there are other people, maybe, in on this call who are working on this.
Raji is a very sick and taylor Johnson's N.
Andb are a couple of examples that come to mind i'm Sure, there are a lot more. then, in this similar spirit there is another line of work that we have recently open source which is called neuron coverage
for deployment. And the idea here is to use coverage metrics that are used for code coverage.
To basically, you know, see whether whether it can provide any sort of analysis benefit to the users as well.
We It remains to me it's still only days and It remains to be seen whether this is a useful metric for sort of robustness, and and, you know all these properties of off the underlying system, performance.
if you were to do coverage sort of analysis on the network it's It's not it's not clear yet.
Oh, and so this is some examples that blocks about this.
And Let me mention one more block, which is the constraint enforcement block.
This is sort of based on the control barrier function, and etc., like a line of research from the controls community, right?
And what it's doing is basically adding a layer of safety enforcement for reinforcement learning algorithms.
But you could also use it for traditional control design. And the idea is basically whenever you get an answer that is, that does not satisfy a a constraint that you would like it to satisfy you solve a optimization problem
that gives you the nearest value that does satisfy the enforcement, so that you don't learn any unsafe variables.
Whatever you've done is is safe so this is again, The formal methods adjacent line of work, I would say so.
With that, I mean that's the so when my that is the you know end of my talk.
I would like to summarize that, you know. we have seen recent success stories of formal methods being turned into sort of practice without burdening the users challenges still remain about you know complexity, of
the system. So so, that's what motivates us and lots of future opportunities.
We see in this in this area of Ai enable systems where domain specific, you know, standards and best practices are beginning to emerge across sort of embedded medical devices abr next automotive.
And so on. So with that I'd like to conclude my talk and hand it back to Rajiv.
Thank you. So there are a couple of questions.
So my name's from and you thoughts and applications on the that the component don't shared a global clock
Well, we're working I i'm thinking about it but I think it's a little bit more advanced, I think, at the practitioner levels like immediately.
We don't have much to say that Okay, and There is a question from Steve Segal the work on temporary formula offering reminded me of academic work.
Front 22,000 by the propell property, and which was a nice tool for editing temporal properties and viewing them in different languages, including English offices in Lpa, just wondering if this work influence the work of
networks I wouldn't say directly. influenced I would I would say, we work with our industry sort of customers in terms of what would it make sense to them?
So at the specification time I mean there I didn't get time to go into all the details.
But there's probably some screenshots in the paper that show like at edit time, when the signal the actual behavior is not available.
You know what kinds of sample cartoon behaviors we should show to evoke the kinds of things that they should be thinking about while writing the property in a particular way, etc.
And then, when you show this why are you? Why right?
So there is also also a trade-off about expressivity versus what will become like for cumbersome in terms of, you know, specifying wire a ui, etc.
So those kind of when some of those decisions went into, you know, implementing the way that we have.
Okay, thanks. So let's let's move on can share your screen and
I think this thing my browser needs to give access to.
Given that i'm gonna have to quit and reopen because my browser does have to quit and reopen, I'll be back in a second.
Okay, So Oxford is another question for you from Osama Bass.
So on the team of making the Tc. to create from formal specifications. do customers benefit?
Are asked for automatic learning of specifications from the crisis generated by legacy designs
So I guess specification mining is that, like a good research direction from the traces from data?
Oh, maybe i'm i'm not sure we we've kind of heard it in the in the context of you know, managing experiments, and so on.
But not specifically. You know, mining specifications. One of the challenges is because, you know, models get developed for different purposes.
Right. So with different purposes in mind. So if not done via formal specification.
Manager. it's not clear whether you know we should be using the results from another model for a different context.
Okay, Thanks. yeah. i'm back But it's somehow not letting me share this screen for some bizarre reason the who dns that?
I guess the it folks that's I guess she is they have a badness to that.
She have permission to share
Yeah, I think Chief, she does do you want to send send me, or Nina, your your Yeah, it's gonna be hard.
Just let me let me try one quick thing i'll be back again.
Just one more minute. She just became co-host, so maybe no, she can
Okay, meet by anyone. If you have any questions for actually or Dave or Nicolai, it's, you know.
Yeah, we have
We have. we have had, you know, give you a diversity of application, the units could be used, so that That's great
I think the the computer is not allowing the recording. I actually think that might be the problem.
Yeah, You can email anyone up as you like me or be your slides.
That would be please
I just sent you a request. if you want to send them to me.
I left you my email in the chat, and I can display them for you.
Okay, because i'm doing what it says here and i'll be able to
So actually, I don't pay maybe maybe have the whatever it was like.
Next go first, and then i'll by the time i'll send slides to Yeah.
So I saw some movie, maybe. Why, don't you go ahead and fine.
Yeah, hi, everybody. I also wanna is that slide. I think it should be easy.
Can you see my slides? Yes, we can see your screen.
Yeah, okay. So first of all, I also want that acknowledge.
And I said, especially I was working extensively in my career with Tom Max, and generous support for Minnesota.
Many of the people in my team actually are graduate from medicine.
And the talk that i'm gonna talk today. is our startups which we started Actually, we'll we'll be celebrating 4 years in the in actually a few days.
And this is actually taking the techniques of formal method.
Specifically smd and static analysis, and putting them actually to find huge bugs in the area of smart contract.
So our team actually is up grow quite quickly. We have about 90 people in the team, many of them actually have Phds from, I said, and they actually we have you fantastic group in the Us.
And also fantastic group in Europe, supported by upn and also fantastic group in in Israel.
The old domain expert in the of smt and static analysis. and we need them.
Actually the problem that we are solving are very hard, and we need them.
We feel that we need to push the R and D to make these techniques work, and we actually contributing already to static and as an smt in order to solve the problem which are raised by our customers, we also have actually
fantastic people that we are hiring which are not actually domain expert in the area study guys in S and T.
But they are domain expert in code security. In particular, I wanna come back, I mean, Levy was actually used to be head of the security in the idea.
So these are people actually helping our customer with with actually writing the specification.
And actually using this technology, this is equally important. This technology is actually used now and actually, but our software is not open source.
But you can. If you want, you can access the software from our website, there's a free version.
You can use it to check called at the moment it's working solidly, but coming back is coming next is right there, and then vast, and then move.
All of them are actually being checked so it's related to David, Stop!
We have this technique, and It's under the boot of course it calls tools like Yeah, Z 3 Cbc. 5.
It's actually combined, and simply sold by queues A lot of smt solving under the hood the pain point that we are addressed is actually has nothing to do with each other.
It's a pain point that everybody is worried about is basically exploitable software.
But in the area of smart contents, actually very interesting, because you have a small code which is manipulating a lot of money, and you can make mistakes which actually will cost you 1 billion dollars.
And actually they were already found by a tool. Also, the code is immutable.
So once the code is deployed it's hard to change and the concept here is called as low.
So if you have a wrong call, it's a long long the other part that we are addressing is the problem is sort of how do people actually?
And this is, how do people check the code in the air of smart contract?
The standard that is influenced usually by Vcs.
And other is what's called manual auditing so man you already think these are people security with security, minds that you are reading your call.
Some of them do fantastic job. but still it's very very hard to find these people, and also these people we are finding even box after them.
The other problem which we are twice is the ineffectiveness of tools.
Basically tools fail and tool can fail by false, positive force, negative.
And also the very hard to use, and how the tool we are pushing very hard to make it easier to use.
We have still far. I think we have to make it much easier to use in the in the next.
In this talk you have to talk about box, and actually done a lot of box.
But this year there have been many, many fantastic box. The bug is I, and many of these, and these are the ones here. some time, of course not.
Coding arrows, but these are all called cordials, and they are all logical errors.
So these are mistakes in the code that were exploited to still demise.
So the Norman bridge is a very very interesting example it's a case that somebody update the code to change the very recent.
But and basically the heck actually was a nice guy. He just told a little money. but then people after him, they saw it, and they stole the best.
So basically, what happens is actually a very recent thing. Compound is a very interesting case, because they actually do work with Saturday.
But what happened? People who built on top of them didn't use our technology, and as a result they lost their 18 million dollars.
So basically, and we are actually working now together, making this tool available, not just to developers, but also to people who built on top of the development.
So we are making this tool available now to to more people so that they can check the code. and it's of course, related to David to talk about using the technology in in part of Ci as part of continuous integration.
How does our tool work? It work exactly as you expect, Like you.
You write your environment, and then you write your code. It could be installed.
It can be another language. And then we have this prover, and this prover can either tell you that the environment is full.
But the more interesting cases it can give your back. and this can be a potentially whereabout.
And this is how we work. We provide the invite to our customer working environment.
And basically they use this technology to check and this is a technology that the moment is it's running on the cloud Austin aws.
There is a very powerful machine, and under the whole it's one smt soldo.
Actually it combined many ascent tools as simply solve them together.
To solve this problem. Of course we know in this domain, and this is our enemy is that we have time out of the Smt.
And our our smt formulas are very complex. So, in fact, there are a lot of failures of the tool.
We are working on them, together with a lot of support from N.
Equalized Z 3 Cbc. 5 team, everybody who can help us, And we have to get as many hope as we can to to basically show these Smt phone ones.
The the other use case. And this is what imagine in in David Deals talk is that we integrated in part of the Ci.
And many of our customers. They integrate this in part of the development pipeline.
So basically every time they change the call, assuming that the advance remains the same, they run the tool again and again and again.
Notice in our domain. I like tools like Daphne. we only write the invalion.
So this means that there is actually more complex score for the technology to hand.
So basically, every time you you, you change the code, you want this technology in order to prove options of bug or find new bugs.
Okay, I think, David ended with the complicated problem. So I wanna start with the complicated problem.
So Smt solver it's a huge success but in our experience. There's a lot of things that need to be improved to make them useful in our domain.
So we are talking about financial systems. so no lady i'm mathematics is very heavy used there, and in fact, our tool phase a lot in nonlinear.
We have our own solution, but the, I think many more are needed also in crypto currency.
The number of so very big, so if you're trying to Use something like big vectors, So that's basically very, very hard, because you have 202 2 or 56 meet integers.
It's very, very, hard hard to scale it and another problem that we see is that the usage we and we are handling low level code. And but it's also the case for high-level code that if you want to go
using a rate theory. It doesn't scale we have our own methods, and we rely on static and early.
But still it it has to be improved I don't think that we worry about this quantification because we want to make the environment useable.
We don't want to use quantifies and and If you are what have quantify, especially quantified donation.
This is where Smt Solver do not work for us for us. since we work in financial system.
Also we need high order visiting in particular, you need something like summation, and this is, of course, something which is hard for the Sd.
I also want to point out, and maybe this is august in this community that even if you have something working in a single turkey once you combine to you, it's very, very high and in another August probably is size, what was
you formula, and it's very very very hard for smt to scale to these new formula we do have some kind of reliability that we are doing for a reason.
But still it's very, very, for hard for us to scale So the lot of research to be done to make this technology more broadcast, and we we have to tell you we have the white paper and we have to share with have papers describing some
of the academic wealth. But we love to get as many help as we can to solve this problem.
How is this tool working? So this is a basically the the way the tool works?
It's actually takes the solidity call and then it goes to the Evm.
Ebm is a by code of detail, and then we have our own decompile, something which is actually go back to the work of Floyd handling.
And the University of Mcgee. Basically, you can find bounds on the stack and get some symbolic presentation.
We call it that we have this call, and then we combine the invite also to talk.
And then we have the verification condition, where we do a lot of things in order to get an smt formula.
And then there isn't 2 phone lines is fed to a one seldom or many sober in order to either find a bag or prove an absence of that interesting thing that we found out that actually is, it's a game change
of wise, especially because we let work on low level code.
Do we need to specialize the code, And we actually do a lot of static analysis.
But the users of static analysis in order to simplify the code.
So this we are doing something which is, you can call it a cheat.
What we do is actually, we enforce certain stronger environment on the code.
And we change this invite. we call it trust and verify and there we're using opposite interpretation.
This is actually where we can recover storage. We can recall a high high level type, and we are doing it without restricting the program.
So basically we are taking 2 into account, some kind of assumptions on the compiler itself, and we are doing it for solidity.
We are doing it for us. The interesting thing about this thing is that it actually give us a lot of bug in the compiler itself.
And you can read out, basically, we find box that the compiler itself, unintentionally both this environment, because they were back in the compiler itself.
So we are finding these bugs automatically with the user static analysis of object interpretation.
The other things that we are doing in I won't be able to explain here.
But a lot of expert in the team. specifically also a very basically show you all kind of techniques how to solve the basically to avoid the the, the, the Np.
Complete, or the the understandable problem of solving smt.
And of course we need to probably learn more. The community has a lot of metals, and maybe we need to learn more in order to actually make smt solving more tractable.
I wanna actually use the rest, of the talk to actually show you the good things that there's and the thing that they'll send the good thing with the smt.
And you guys have done for us. Actually, these are the cases that we found many, many interesting bucks.
And the most interesting, probably bugs is a solvent issue.
So what does the solvency mean? Solving c. you can define it formally in temporary logic?
But I'm defining here. it in informally basically if everybody wants to the bank.
The bank is still and this is sort of an interesting property that you want to inform.
We don't write this property. we write it actually a stronger inf environment which implies this property, and here you find bugs that found by the Smt.
And all of these they were found before the call was deployed.
They were fine after the call was carefully audited by the best teams.
And here you see the box that we found, and you see the amount of money which is safe.
Okay, So this is sushi. swap for example this driving is the case that the smt find this bug. we allow you to completely drink during the money. I don't know if you know it's one of the biggest one
compound. So these are bugs that are found by our tool.
We will divide in this case. So the subtraction, we will the environment, and then we use them with the smt to solve.
To find a box. So this is a case that bugs will find by the smt.
But this is to our team. Actually we will be invited for them.
The other thing, which is even more interesting. And this is actually something.
I know that a lot of people say bad things about cryptocurrency, but in cryptocurrency the lot of very good people.
And one of the things that we are finding out that some of our customers they know how to use our tool better than us, and without.
So basically, for example, this is make here I don't know if you know.
Make your doubt it's actually it's called it's actually holding about 15% of the cryptocurrency in the world, and they use the tool.
You see it's basically the the the code implement something which is called a stable coin.
So they statement. They they launch this code in 2,018, and they run the tool actually. did you see it?
And the tool actually there's something found the back that allow you to actually break the the the basic advantage of the system.
So this is about 10 billion, which were at least, and actually this.
The environment was written by cool. is that If you actually wrote this environment, And actually it's very interesting.
It was surprising, basically, what happened. The tool found that the basic environment is not in that.
And it was found by Smt. So thank you, Nikola.
It was fine by the Smt solder after the cool world.
The environment. And I think that actually very interesting, that another customer.
So this is another customer called 2 5, they're all the own environment. and then they did something which I don't know if you think it's fair or not, they actually call it auditing thing, and they ask them to check.
The box, and they basically insert manually box, And they ask the smt solver to find the pack, and also the the the auditing team to find about.
And what you see, actually that the auditors which are human they missed actually many.
But okay, and and basically, you see that the formal verification is found.
The more the most significant number of bugs. You see, also, the formal verification missed on that.
Actually, I think, one or 2. and this is, of course, due to the inappropriate environment.
We have already few customers. we just use our tool and actually they don't have the right environment that's a problem. And we are actually implementing now open source technology, which is mutation testing led by Chanda Nadi also
actually supported by Nsf: So we have tools that are checking the device.
Are not vacuums. they have their caring support.
And what? So that's what we are doing in terms of what we are. Now, I think that this technology is actually used by the top players.
I think about 50% of them. They actually use this to secure the code this is running actually on the lot of programs, And it's actually integrated into Ci.
We have particularly healthy of the box that we found before the call deploy.
We actually can run the 2 after the code deploy, because we are running on the X one executable, and we have found you of them.
But we have specifically happy about the box that were found by these technology before the call was declared.
Holy thinking about standardizing it so that's actually a huge effort for us.
It bolts in the Ivan D, but also in the adoption.
So we used to. Basically, this is a software service that we send to our customer.
But we are trying to make this more usable, and one of the the problems of making it user.
But of course, making the tool better, but also making the task of writing invariant easier.
And this is where we are at the moment trying to use community.
So we have now and of course, it's not as the community it's a quadrina is a community which is actually in the Us.
So actually encouraging people to review, call, and what we are doing now.
We are partnering with them that people when they view the call, the lighting value, and for for the call, and then they would use the tool, and from there and back bounty.
So these are mechanism that encourage community to write specification and from down.
We are going to what's called down which we already started is basically I already mentioned that not just the the people who write the code.
Also the people who build on top of it. they they actually use it.
And for that they are basically we have the people in the down.
They have to vote for them. The people on the down have to vote for the adoption of the formal method.
We have done the first one if we completed it. I think yesterday, and all the proposal actually got the now the highest number of to people. It means that people really like formal verification in this case.
You can read about it. Look at the other proposal.
People really like usage of formal verification here to make the code more secure.
That's just my presentation. Thanks thank you thank you mode any in any questions for I mean, this is like a great application. last couple of years.
And they have okay Now I'm gonna try once again
Yeah, it's not somehow I think it's the recording part that probably so. Karen, maybe you can.
You have slide, so maybe you can share them
I think Karen will have to do the driving
I'm Karen and Edgar are you guys gonna share the slides
Karen did say that she got the slides.
I got it. Okay.
Okay, great softer we finally get there. so thank you for inviting me.
I'm very glad to be presenting all the work and and learning about all the work that's been done, that there are great success stories for foreign methods across industry and an opportunity to present how formal methods is transforming development
both inside Amazon as well as externally. next the the driving factor
Here has been security, and as earlier it came up like, how do we ensure security, durability, availability, and correctness?
So in the early days when folks were like, Hey, I have my workloads, my sensitive data.
All on my on my on-prem systems but as i've put them on the cloud.
But I have to go access them over the Internet security. becomes a key part, and that's been one of the driving factors that has led to this growth of automated reasoning across Amazon.
So there's a whole website around approval security next there's also a a whole science page dedicated to all the publications.
The blog post. The talks across various different groups. so the the way automated reasoning works at Amazon is it's actually distributed there isn't a separation between this is a science organization versus engineering and product each of
the different automated reasoning folks are distributed and are close to the businesses themselves, so they're embedded in the engineering and service teams.
So how are we applying automated reasoning i'll give a quick overview next, and it it starts with foundational Co.
Next and the foundational code really is there's numerous foundational systems.
You have custom, hypervisors, encryption, code, bootloaders and iot operating systems, and we are leveraging formal methods to prove the correctness of foundational low-level c systems.
And use them to do automated test case generation where we validate that it actually, satisfies certain criteria.
And we're we're, doing some tests but we're also using like proofs of memory safety to ensure that the code is both secure and correct, and the proof is around memory safety infinite loops and
other defined loops. next. So one success story is free. our toss, which is an open source, real-time operating system for microcontrollers that essentially makes small low power edge. devices that are easy to program deployed
secure, connect, and manage. and last year one version of this was downloaded every 170 s next, and we have proofs of memory, safety, thread, safety, and functional correctness of the correct queue implementation, and
free artists. where there's also provides high level of assurance that the free artists enterprise communication mechanism which uses the data structure is also correct, and these proofs are publicly available and are run as part of the continuous
integration to ensure the continued maintenance. next another example, is a foundational library called Big Number, which is used for hyp, precision, inter integer, arithmetic.
That's about a 1,000 bits and most asymmetric, public private key cryptosystems like rse.
Use these big numb libraries, and it's also used in something called S.
2 N. S. 2 n tls is an aws implementation of tls as a cell protocols that's designed to be simple, small, fast, and with security as a priority, and there is a proof that it is free of side
Channel analysis attack. And again, you can reference it online.
So we move next. So we move from foundational code to the next level, and we move up the stack.
And here it is about how we leveraging phone methods to ensure that the protocols are safe.
Next. So one place we're looking at it is where are the critical systems. we have authorization cryptograph, and cryptography are the 2 main protocols that we are working to prove collect so kms is an aws.
Managed service that allows a users to manage their cryptographic keys and control its use.
Next. So we've been applying verification techniques to ensure that the protocols that describe how customer data is handled in transit and in rest holds true.
Next, and we have machine checked proof that the cryptographic keys protecting customer keys are maintained securely across aws, and you have a paper on that.
And the connection to Code and protocol is also checked continuously.
Next, the protocol description proofs are open source, and you can independently verify them.
So as you can see, there is a theme here where it's like, hey?
We we the theme is we make open source what's available There's a tie to the code there is Ci CD.
To instrument that they don't they are always insane.
Okay, so we'll keep going up the stack next as we move.
We, we wanna make sure that the applications where customer and user workloads and data run are also secure.
So we'll continue with our encryption theme and we wanna close the loop and go on step further. So we want to ensure that all internal services that handle customer data and use these crypto api's are doing it
securely. So here we use program verification techniques to ensure that the Service code in the Service code that all customer data is encrypted before it's stored log or pass to another service.
Next. so we also are using it in different applications.
So this is Amazon dot com That sold over 386 billion dollars worth of products to customers.
And one of the things that requires to maintain this trust is the ability to safely and securely store critical payment information for all our customers, and we want our customers to trust us.
So when they enter the data into these fields that it's secured correctly, and amazon's building a secure payment wall on aws.
And it's using a lot of these technologies on proof, and the larger product than like proof of security to verify it.
Next So just to good this was you you can just keep clicking to the end of the slide, because this is
It's gonna be hard. I had some animation here. So at the root you have an Api call.
We have the application that makes a request. The request must be allowed by some organization policies or permissions, and then we have the Im permissions that get attached to the resource.
And finally, we have the network level, and the request has to get from the top, from the principle to aws over the network.
And if you keep clicking through in order to secure our payment, we essentially have, like different analysis layers.
We have network analysis, we have policy analysis, and we have coded analysis.
And so e here's a way of like all the things I talked about, and how they get applied.
So this is all internal right like we're doing all of this work internally to prove correctness of systems making it part of the development cycle.
It's in continuous ci CD we're also using it to verify the stack of our entire applications.
So i'm gonna talk next i'm gonna talk briefly about how it's gonna how it's actually being used in a lot of customer facing services.
Next. So there's a the way we talk about this to end Users and customers is now with these services and features.
They can make universal statements about their security. and we're talking about like quantifies like a cro none of my easy 2 instance are, and unintentionally public and all ssh traffic to my instances go through a
firewall. Now, you and we look at this criterion we're like, Okay, how does it manifest the next?
So this one is something called F. 3 block public access, and if you go to the S.
3 console, and you look at a permission of a bucket.
You'll see something called s 3 block public access and when you turn it on.
It blocks all public access to the bucket. So what does it do under the hood?
Can you click one? So it essentially translates the policy into an smt formula that checks.
Does there exist some allow statement that violates my trust policy?
So this is for the end user all they're doing is checking a box, a one check box.
It's abstracting away all the complexity of having to specify an invariant or a specification, and ensuring that it's cutting it's all done under the whole 300.
So and when it's when it's done when now, if a if a user tries to attach a policy that is not, that is public, there is a in line a simplest call made to the smt solver and the result of
that smt solver gets bubbled up to the end user.
So this is a big deal, because this synchronous, called an smt solver is in an Api of a control plane.
Api of a low latency service, such as s 3 next.
So we talked about like, Hey, you're the specification is embedded.
But what about other services? So we provided this service call I don't have the I don't have the time to get into each of these, but we have a story for how each of these service does a lot of analysis under the
hood and provides to the end user and abstraction.
The access analyzer is one such a service that analyzes whether a user resources have public or cross-count findings, and we use stratified, predicate abstraction to ensure what are the set of sound findings that
we return to a user next. We have other services for networking, such as Inspector.
Next you know again we have a findings model it's like hey?
You have a so you can see there is consistency.
We are not launching multiple services with an inconsistent Format, because that adds more cognitive load to the user. Here, again, it's actually chalk checking properties that says, Hey does there exist a port where this property
holds or it doesn't but it's presented to the user in a format that's consumable to them, and it matches their mental model.
Actually I talked about this mental model, but it's like hey?
You don't want to do it in a they represent you you don't want to do it in Ltl, which nobody will be able to use next
So there's also i I talked about how we are doing it in a consistent format, and one of the keys is just a security hub that aggregates findings across different services next.
And this is where, like universal statements that you're making about different parts of the Cloud assets come together next.
So you see here, like the things that are true and access analyzer and things that are true.
And inspector actually come together into like, Hey, This is what is not holding true of your system.
And again. This is all in a way in a format that's accessible to them.
Next. So the the the problem of like, how do we do?
Specification, like keeps coming up, and part of it is again, How do we like?
We are providing users, templates, templates, that they can fill in without having to understand logic.
So this is again a part of if you look at the words it's like, identify access to Internet gateway example.
And here all of these are in the way, getting you end users to write specification without them having to like know that they're writing specifications next.
So it just. these are just different types of specification that they're writing without having to know.
And next so 8 all of these you'll have to click through a few, because it's yeah get to the next slide, and all these services are allowing end users customers to be using formal methods under the
herd without them having to be formal methods, experts, logicians, even computer scientists, because they are interacting with the service and the tool that they need.
And want to use, rather than having to think about specifications and properties and proof systems, and all of those things.
Next. So all of this is driving us using a So one other thing that I I didn't talk about is all of the customer facing tools that we talked about is using smt under the hood and what's that
driving. It is like a 1 billion smt queries a day that next.
And i'm gonna talk about a very specific challenge next about that we had here.
So the engine here, I'm talking about zulcova It uses a portfolio solver to discharge its query.
So Del Cova involves multiple solvers in the back end and uses the results from the result that returns first, and it's a winner.
Take all strategy 2. So the portfolio approach allows us to really leverage the diversity among solvers.
So we were like, Okay, we have a new solver. come out Cbc: 5, and we want to replace our Cbc for implementation with 65 next.
So we we run it on a Next we run it on a large set of benchmarks to check its timeliness requirements.
So this is just a representation representative set of queries across like 15,000, and we just select a distribution to show, like the queries that are sold between one and 30 s.
And we see here that some of the queries that are not solved by Cbc.
4 within the time bound of 30 s, are now being sold by Cbc.
5 by the points in the graph along the Vi axis.
On the extreme right, however. Cbc. 5 times out on some queries that are being sold by Cbc.
4, as we see on top of the graph. So we next.
So we worked with the Cbc developers and got this fixed.
And but there was another issue here. Cbc. 4 was Twox faster than Cbc.
5, for many of the easier problems that took 1 s to solve.
Originally, and the results are not surprising. Given that the space is computationally hard, and there is an inherent randomness in search heuristics with an smt solver.
But this was posing a challenge for us, because we are using the results of these solvers in security controls and services, and we can't have a regression and a solver impact customer. behavior.
We saw all of these services. The point was like of showing those services is like.
I cannot have my bucket go from, not public to public because my smt solver time dog.
But then that end user hasn't done anything on their end.
That would be a terrible experience for them next. So we we ran some experiments.
So here's Cbc. 5 with the winner take all and portfolio solver without Cv. 5, and but Cvc.
4 is part of the portfolio, and we see it doing well next, and
We had a new version of Cvc. 5 with the winner.
Take all, and portfolio solver and that's even doing better.
So given that it led to our decision of next adding, Cbc.
5 to the portfolio solvers, containing Cv. 4 Z. 3, and the sequence we have a custom sequence change solver, and the plan was never to add a new version, but because we expected to just the latest version of
Cmc. 5 to be comparable in timeliness and correctness to Cmc.
For, and and we did work closely with a lot of them.
But yet we ended up adding to the server, So like, Okay, are we done?
Not quite because we rinse and repeat, we are like the cycle repeats with Cbc.
1.4. And now the question is, do we upgrade?
Do we add it to another version to we and some of our early experiments is like, Hey, there, isn't a clear answer.
Yet next. So we're like okay, we are the clown and what works when the cloud setting is a massive port for you, or sometimes even considering all versions of soul was there's 2 problems.
Right. If we discover a bug in the older version of the solver, we'd need to patch that old version.
And now this creates what's called an operational burden of maintaining many different versions of the solvents and 2 When the number of solar increases, we need to ensure that the each of the solvers is providing
a correct result, now checking the correctness of queries inside the straightforward.
But for smt solvers we need to provide proof for the Msat queries and the proof checking, and the proof.
Generation needs to be timely as well next and next so i'm gonna in like i've talked about a broad set of things in a broad set of, and i've I have opportunities, misspelled but
what are some of the things like? There are very interesting areas of research and opportunities for the broader area.
Monotonous city and stability in runtimes of smt solvers.
But essentially all analysis tools, because a little chain and we've known like, we accept it like, hey?
We are in this computationally hard, pspace domain np-hard domain.
And of course you're not gonna have consistency. But if we want to make it more mainstream.
If we want to make it part of the development process, if we want to make it part of the Ci CD.
The pipeline predictability is important. predictability in versions, predictability in upgrades approved generation.
How do we know that the answer is correct? When now we are driving security controls?
Based on the results of our tools. How do we just like a lot of the development of our tools has been on a very sequential world?
How do we transition it to a distributed world like?
Should. How do we make our tools themselves? leverage more of the micro services?
Architecture such as the one that cloud computing offer better support for quantifiers in general.
Thinking about developer tools and better usability. again, if we want to, have more developers using our tool as part of their workflow.
How can we integrate better in the way that developers develop today?
How it's Not an additional step they have to do I think that's gonna go a long way in driving a large scale adoption of such tools and services.
One of my personal things is, how do we drive domain, specific verification?
And how do we incentivize folks in academia to work on it?
Because oftentimes we say, Hey, here's a paper this is great, but it only works for this domain.
So, if it's not a general absence to work on just general or resolution.
But for techniques to work, we have to leverage the domain, and if the domain is big enough, i'd love for us to find ways to infernalize a research in this area concurrency in mainstream tools like even
like Daphne and other tools would be a great thing, and I learned on something called idiomatic compilation, like A.
For for tools such as staff need to be used more broader and mainstream.
Like either, we say, hey, run Daphne in production.
But that would be a really hard sell. So because you know it doesn't have the required developers support, or you know, expertise.
So if you generate if you're so saying hey? let's run the code that's generated from Daphne.
It has to be something that developers can read, understand.
So then they would be comfortable, saying, Hey, Yes, I know if i'm gonna operate this code.
I know what this means. thank you again, i'm happy to take any questions.
And on answer them and thank you. thank you, Edgar and Karen for helping.
Yeah, thanks, That did a couple of questions. So Nate faster asks: So verification needs a model of the system, and the distributed systems are incredibly complex.
So what models are you using, and how you check that?
They like reality. Yeah, and that's a great you know point where this is web connecting to the code is very important.
Where and how it's through some differential testing approaches where it's like, hey generate tests on the model generate tests on the code and try to ensure that there is a conformance taking models turning
them into runtime monitors so there's also one area where we are saying, the model is the system.
So that the actual system code is generated from the model itself.
So we are doing it. in a couple of areas the encryption. Sdk: is using a daphne model and generating code like Java code, and go code a dot net code from from the Daphne model itself. So here.
It's. The model is essentially not like an abstract model, but a representation of the behaviors.
But there, isn't, a one there's no I I mean i'm preaching to require. but of course there's no silver bullet right like and one of the things is we should not view verification as an all or none law
like, How can we, inject more development techniques based on testing validation?
To start to make the bridges between the model and the code and the like.
The tests are great. the test that end users right are a great example of in a way specification so like, how do we use that?
So I think, leveraging more of that, and will help.
But it requires building a lot of tooling and building a lot of infrastructure to make that happen.
Okay. There are actually a couple more questions from Matthew Bolton.
Is there a cognitive theory gender design principle behind a war usable user specification are defined.
If it's based onmented models how do you know that the human mental model is Yeah, that's a interesting aspect with
The constructs we've ended up using are based on the domain?
So how do security engineers talk about constructs like It's through talking to a lot of and this is also some.
It's called something called persona based and the personas are different, like who's doing what task you have security engineers.
You have developers. you have it Adm. administrators, and based on how we come up with the mental model.
Is. each of them have a defined like, Hey, This is their job.
This is their workflow. This is what they go through.
If and we translate them into these higher level constructs of for a for a developer or security engineer.
The notion of I have a finding about like the city that's related to the security of my system that matches their mental model of what they're doing, because, like findings are things that come in pen tests and like abstract reviews
it gets generated. so like if you said here's a violation of your property.
Also in like here's the potential counter example that would not make any sense.
But here's a finding that demonstrate this account can access your resource under these conditions.
So there, isn't a gin generic cognitive theory, but it's really related to who the product is targeted for like what's their role in their company?
And how how they how they go about doing their job, and then matching the constructs and the tools for that Actually, more questions.
But we are kind of over over time, and we've been hoping actually for some discussion for everyone.
But so let me just take one question, which is, for all of you.
This is from getting Walker. So one way to incentivize academics, maybe to supply open challenge problems with charity data sets.
And the Academics need real world data which can be difficult to obtain unless we have personal connection to industrial partners.
So if any of you want to, you know, address this. that would be great.
Okay, I think Smt: Comp is a great model, and has, you know, benchmarking and competitions always have a dark side of occasionally pushing research in the wrong direction.
But on balance it's been a great sanity check and a great way to drive research.
And as you know. I think sons people in industry ought to be motivated to work with academic partners to get benchmarks into that, because then you've got all kinds of people hammering on whatever problem
you you came up with. and so that was one of the things we did with Cvc.
5 was we, since since our system was open source. Anyway, we we could take the problems we were running into that were problematic.
Give them a collection of benchmarks for vectors and other things, and they could try to use that for Cvc. 5. and then we got permission for them to share that in the competition.
So that's something that I would highly recommend for anybody who's a user of Smt Solvers that is having some struggles.
So to what David said. we did the same right like we have like our examples of what a hard benchmarks with the Cbc. team.
One of the things, though. is there is a there's a dual side to the coin of like leading benchmarkets. A.
You know there is a process that goes through like, Hey, what are the benchmarks being supported?
2 we like parts of it is so here's what I would love to like.
Think about synthesis approaches, or generation of benchmarks, or just, you know, getting more.
Diversity like sharing is one approach. but thinking about how to benchmark techniques, how to think about especially with respect to monotonicity I love for the Smt com to have a new category
where it takes into account how you did last year. on these sets of benchmarks, right? like, Because right now the incentive is to solve more problems and solve how the problems which can allow the tools to regress on yeah
the previously saw, like the performance of previously on again.
And I understand these are hard problems like I. I understand why, theoretically it happens.
But that to me, I think, would be would be one way, but also looking at synthesis of bridge box like, how do?
Just even using the shuffler right like we say, Hey, we We can create such a huge variance in the
The runtime. So I I think, indeed, in general, and this maybe this is something like the tool development process, and I think the Cbc team is a great example of it.
But You know where the the challenges for academics are in publication, to apply tools at an industry level.
You have to invest in tool development, and of course you know that is that there's the cost associated with it.
And industry should be funding it, but also like
How to ensure that there is a path for success both in terms of publication as well as external government funding for these, for academics like, I think it's it needs to be a combination of all 3 for for
us to push. and I when I say tool development I don't necessarily just mean engineering, right like, but making robust tools like a that take over years to get there.
Okay. So let me ask one final question again. You know other few.
So I think. it seemed like, you know, the the solution to folks not ingenious, not clearly understanding problem.
Space specification. The solution that you, many of you, seem to be able to be advocating is that we come up with this pattern or something, but the other one could be actually incentivized.
You know, undergraduates to learn a bit more about department specifications and listening.
And when chat that we face in academia is that in the industry recruiting process seem to incentivize, studying our marketing, thinking but very little about in a formal logic and specifications.
And so on. So I wonder if it is any any way, you folks can help questions about this into the interview process.
Basically. Yeah, yeah, and it's a bit of a chicken and a leg problem like we can't hire engineers would, you know, could could be able to write specific stable for internal things.
And there's a lot. We go through and so we should think about how we can see it.
And pilots and programs around this we're pushing it under the in like undergraduate education programs with the path to future jobs
You you say that the there's emphasis of algorithmic thinking that might reflect on people who are conducting interviews.
If you get an algorithmic interview and and it.
But the reality is, of course, that in in a job situation. you'll you need a combination of algorithmic and and formal thinking, And so I think it's a question of it's stealing a the
culture.
Yeah from from audit, I think, having a background in formal specification.
And yeah, you know, that sort of background is definitely a plus. And much of our, you know, developers who work on this sort of pipeline have Phds in either programming languages or follow verification.
So would say, for that team but definitely it's beneficial, and we have incentives for the right kind of Ion
Okay, Thank you. I think we are getting over the time. But thank you. Thank you.
And This was wonderful. and we, you know we had, as you can see we.
You know we had participants from all over. This is the end of this session.
So you know the for those of you who are not part of the and they said, program, You know, we have a session tomorrow at 2 o'clock, and we're welcome to join that using the same link we're just
focusing on future directions and those who are part of the bi meeting.
I I guess the next session starts at 2 o'clock, and you can to join using the this. the other thing which was for the closed session. and then they will have ring I think it sounded so thank you thanks