AV-Portal 3.23.3 (4dfb8a34932102951b25870966c61d06d6b97156)

SPARK Language: Historical Perspective & FOSS Development

Video in TIB AV-Portal: SPARK Language: Historical Perspective & FOSS Development

Formal Metadata

SPARK Language: Historical Perspective & FOSS Development
Title of Series
CC Attribution 2.0 Belgium:
You are free to use, adapt and copy, distribute and transmit the work or content in adapted or unchanged form for any legal purpose as long as the work is attributed to the author in the manner specified by the author or licensor.
Release Date

Content Metadata

Subject Area
Augmented reality Website Musical ensemble Gauge theory Perspective (visual) Formal language Perspective (visual)
Building Group action Code Java applet INTEGRAL Direction (geometry) Multiplication sign Decision theory Execution unit Design by contract Client (computing) Mereology Computer font Semantics (computer science) Computer programming Predictability Formal language Subset Neuroinformatik Mathematics Cube Formal verification Electronic visual display Information security Multiplication Position operator Physical system Intelligent Network Block (periodic table) Data storage device Menu (computing) Range (statistics) Bit Special unitary group Computer Opcode Formal language Product (business) Category of being Arithmetic mean output Regular expression Resultant Software engineering Game controller Functional (mathematics) Service (economics) GUI widget Open source Adaptive behavior Similarity (geometry) Online help Limit (category theory) Event horizon Thresholding (image processing) Portable communications device Automatic differentiation Machine vision Product (business) Hypothesis Number Revision control Intermediate language Goodness of fit Well-formed formula Term (mathematics) Gastropod shell output Condition number Addition Dependent and independent variables Inheritance (object-oriented programming) Validity (statistics) Assembly language Projective plane Mathematical analysis Planning Line (geometry) Symbol table Perspective (visual) Sign (mathematics) Number Word Software Intrusion detection system Personal digital assistant Logic Function (mathematics) Collision Library (computing)
Axiom of choice Complex (psychology) Wechselseitige Information Group action Dynamical system Context awareness Boolean algebra Concurrency (computer science) Computer programming Software bug Pointer (computer programming) Invariant (mathematics) Type theory Different (Kate Ryan album) Error message Social class Exception handling Proof theory Constraint (mathematics) Constructor (object-oriented programming) Bit Instance (computer science) Control flow Complete metric space Formal language Demoscene Electronic signature Category of being Arithmetic mean Hexagon Regular expression Reading (process) Recursion Spacetime Point (geometry) Slide rule Patch (Unix) Raw image format Event horizon Code Automatic differentiation Number Frequency Latent heat Goodness of fit Term (mathematics) Profil (magazine) Hierarchy Energy level Regular expression Standard deviation Dataflow Code Plastikkarte Multilateration Line (geometry) Group action Gauge theory Cartesian coordinate system System call Preconditioner Word Radius Loop (music) Personal digital assistant Function (mathematics) Revision control Formal verification Code State of matter INTEGRAL Multiplication sign View (database) 1 (number) Design by contract 8 (number) Mereology Food energy Subset Usability Duality (mathematics) Circle Series (mathematics) Recursion Extension (kinesiology) Category of being Position operator Stability theory Curve Concurrency (computer science) Flow separation Substitute good Proof theory Type theory output Right angle Asynchronous Transfer Mode Dataflow Asynchronous Transfer Mode Functional (mathematics) Service (economics) Observational study Numerical digit Image resolution Generic programming Well-formed formula Operator (mathematics) Software testing output Gamma function Hydraulic jump Condition number Task (computing) Module (mathematics) Addition Inheritance (object-oriented programming) Mathematical analysis Bound state Variance Computer programming Subset Pointer (computer programming) Invariant (mathematics) Vertex (graph theory) Object (grammar) Communications protocol
System call State of matter Code Direction (geometry) Multiplication sign Execution unit Numbering scheme Design by contract Function (mathematics) Electronic signature Computer programming Variable (mathematics) Permutation Formal language Fluid statics Pointer (computer programming) Mechanism design Invariant (mathematics) Cryptography Type theory Semiconductor memory Different (Kate Ryan album) Hash function Resource allocation Factorization Eccentricity (mathematics) Proof theory Theory of relativity Concurrency (computer science) Web page Sound effect Bit Variable (mathematics) 10 (number) Electronic signature Mechanism design Type theory Proof theory Data management Arithmetic mean Googol output Quicksort Functional (mathematics) Optical disc drive Programmschleife Resultant Reading (process) Point (geometry) Divisor Algorithm Rule of inference Event horizon Scalability Number Latent heat Programmschleife Natural number Well-formed formula Term (mathematics) Green's function Codierung <Programmierung> Lie group output Summierbarkeit Loop (music) Condition number Default (computer science) Module (mathematics) Default (computer science) Standard deviation Graph (mathematics) Information Mathematical analysis Expert system Code Line (geometry) Limit (category theory) Computer programming Sphere Preconditioner Subset Positional notation Pointer (computer programming) Voting Invariant (mathematics) Loop (music) Personal digital assistant Network topology Design by contract Interpreter (computing) Data center Library (computing)
Topological vector space Group action Code Multiplication sign Demo (music) Source code Design by contract Parsing Shape (magazine) Mereology Formal language Web 2.0 Geometry Hash function Logic Repository (publishing) Videoconferencing Process (computing) Geometric quantization Library (computing) Stability theory Proof theory Middleware Data integrity Area Email Streaming media Bit Mereology Control flow Web crawler Flow separation Proof theory Category of being Process (computing) Repository (publishing) Telecommunication Chain Right angle Prototype Functional (mathematics) Middleware Reverse engineering Arc (geometry) Point (geometry) Code generation Functional (mathematics) Game controller Observational study Adaptive behavior Quantification Maxima and minima Control flow Directory service Distance Code Pi Goodness of fit Prototype Centralizer and normalizer Well-formed formula Vector graphics Software Energy level Computing platform Dean number Computer architecture Standard deviation Demo (music) Projective plane Code Core dump Uniform resource locator Software String (computer science) Strategy game Musical ensemble Fingerprint Library (computing)
Axiom of choice Intel Presentation of a group Context awareness Code Multiplication sign Demo (music) Execution unit 1 (number) Materialization (paranormal) Design by contract Set (mathematics) Open set Mereology Formal language Data model Mathematics Blog Different (Kate Ryan album) Computer configuration Kernel (computing) Endliche Modelltheorie Organic computing Website James Waddell Alexander II Information security Social class Physical system Proof theory Covering space Source code Email Decision theory Block (periodic table) Open source Non-standard analysis Virtualization Control flow Degree (graph theory) Proof theory Category of being Website Hill differential equation Quicksort Information security Functional (mathematics) Resultant Reading (process) Electric current Row (database) Point (geometry) Web page Frame problem Functional (mathematics) Statistics Module (mathematics) Open source MIDI Maxima and minima Translation (relic) Event horizon Rule of inference Power (physics) Wave packet Number Product (business) Revision control Architecture Frequency Flow separation Software Reduction of order Energy level Software testing Hydraulic jump Spontaneous symmetry breaking Metropolitan area network Mathematical optimization Condition number Multiplication Electronic program guide Projective plane Core dump Total S.A. Line (geometry) Similarity (geometry) Error message Event horizon Software Blog Universe (mathematics) Revision control Computing platform
Projective plane Collaborationism
this year every year for thank you [Music] which usually I do the augmentation reasons or tutorials the next day because of this you can find support websites so that's easy today I'm gonna use this ability to create something that you will show otherwise a historical perspective of why you
thought there and you can see that on this this line as going from team to team building project leader for women for each of the books a building and we end up with a small library of books and maybe a tenth of a shelf and it's not finished maybe one day we have called for them something else I want to get chocolates something more recent that we see interesting first projects that you spot as we're going to encourage these of course small talk about those that our particularly so going back to the east
where spark it store tips long time ago more than 30 now 1987 our company is a great thing program validation widget so the at least over indeed doing giving warranties so this company went through polish good meanings and the positions now it's a nice to be some time they they add right projects or one of the first really big with these c-130j which is a big military plane and the mission the mission computer application is only they are also security for the safety I am cpt palette I took in here which was the project done by Ultron for the NSA it is an invite and we'll talk about it a bit later because in 2008 this project was a contortion because of this because of this event so ad front partners with Air Corps and we convinced them that there was some value in pushing the technology forward you know this would bring a GPL system so these be the fastest way I won't cover much today if you are interested there's this article by workshop Rhonda really covered this experiment so number of things evolved and Susan 8 we started something new so we started this project highlights small sideline is simplifying the use of commodities and what we ended up doing in this project is we built the wall painting so the previous technology kept the good ideas and at the result was this spot 2014 in which means so while we were rebuilding the Kamaria projects for similar things also two notable projects are the iPads project so hypotheses part that's what we control over the UK so when you travel to the UK usually my clients use the shuttle you're using this software which helps a traffic controllers to foresee possible collisions drive the decision making in asking place some actions to avoid and it wasn't for 13 the men say Percy alone first version was issued and we'll talk a bit more about this because this one is open-source an interesting fact is that these two were initially the previous version of part obviously and in the past years they are both negates its to Spartan support so you may say well migration isn't it's a big word for great for from success we have to succeed enough because it's precisely not as so let's see an example so this was through his vision of Scott it's not a subset of it it's boys present its days as really a different language it was it was heretic to say that the cicada it was using a subset of ADA as the operational code on which it was imprinting illogical adaptations logical language the word to language and here you can see an API about computational ins and price of something with something like that looked like the first conditions these conventions and says that when ads returns and it was written something the Sun which has some properties same turned off and and then this one returns this exact value and you can see that already they have voiced some unit which expressions that these quantified expressions that you can see mathematics to quantifiable question you had that thing in the tango is a purely logical language we got relationship to English so only for consumption by the innate system so we transformed it into that so maybe at the first loop that doesn't prove so different from virtual before maybe a bit of syntax in fact so all these things now our part of the language so that executable that's really code code that expressing properties so we really tied through the specific before this these are the past conditions using Mitchell properties and these are additions that we thought were needed in spark ensue outlets yet in Ada and we so here without these contract disease why do you think the company then allowed to specify three paths by cases it's very common services functionalities that behave differently on the inputs inputs or now sets up in post are only available here ads it's saturating addition so if the results is less than imagery show the result will really be the addition otherwise if the results the expected result would be rather than the threshold then it saturates so this project is have this semantics that we deployed in Putin and this can be checked either so I'm just showing it here with a really nice ER display of symbols when you have a ligature in in your monospaced fonts some of my colleagues hate it but I take this occasion to advocate very cool really nice to display properties that makes it easier to I so what we did during the silent project is this echoes tim of open source tools so we built our own ecosystem based on the building blocks away after go CB signals these realities about all these are automatic coolers here to the tech formulas say who falls below interactive coolers here today as super important help him work out the food system and all of these are communities some other sort of easy portable as a useful dozens and dozens of resistance those that are most interest to us are these the atomic tours and widely is this Altice favor of approving so what we've done is this product is really built from other programs to this intermediates Wi-Fi code so by 3 is or intermediate language super code intermediate verification language is the assembly language for doing this kind of deep analysis of products include the deliberate teaching and from wisely there is something called vc directives of ratification condition generator all use with a simple term formula that is problem java code that represent the code here is going to generate and the other shells knob canoes between the US and England out which develops this possible because you've got spark and white P so they have so that they have a really great integration yeah so this all these impacts is for the truth analysis the responders there's a door
to analysis in fact the pyramid there's proof I am there as flawless flawless this is something simpler that checks all the flows in program and this is done at this level really at the level of this lateral - so this is depicting the harder more complex but in two slides I will represent now what we do Bispo analysis and true because I'm going to say two stuff to take me come true but just so that you have an idea of raw analysis that here is the signature of service and now we can add to it with the L a 2012 syntax some aspects there with and this has PEC global is an aspect introduced or spark so the tools that for this party was ten it matters and here we are completing the new signature of stabilize with the new both are both are exists here it has additional inputs are not transparent micrometer and you guys and it show the marble butters might be more than one bar bollocks but you name it which is partially and once you've done that specifying FX that you want the function to respect then the tool can do this flow analysis and check that the program implements this specification so that's the exquisite specification you might add also implicit specifications name in terms of flows that's everything that he computes serves a purpose otherwise you will get watch here you think that's a mistake typo or that's everything that you read is in this line is typically we check most explicit and implicit specification so let's put on our seats and the cygwin is proof so proof using the same signature for stabilized we can now specify functional behavior what it expects an entry speed condition that's the moods event we should be off and kiss by first condition so here is a bummer if expressions condition well that's II in the case of success then there should be a relationship between the once these specification are added to the code the proof tool can check that the program implements this resolution so this is for the explicit from some specification but there are in pisac ones namely that there are no right time errors in the good so all axes are excesses or will in bounce all the ivory is also within the and respects the right checks of the guys so to talk a bit about how we got to the grants solution technical solutions I chose to present to you in terms of objectives that we had for this revamp of these particular G and so we had really high level goals but technical was like let's use these technologies in our zombies so we had some of these but the re-roll goes were these first functional contracts can be executed tested developed that because we want them to be reconsidered as my coop so we don't want to wait score promote proof of these two activities for my name to be replace less precise comments we want them to be able to replace some of the testing articles that you belong otherwise in the separate artifacts at the booth so yeah so that was one of the things which the error subsets supported things possibly as not as possible indeed the main reason not to use the technology because it doesn't apply in your a so definitely people who see what anything at Purdue we like people who use era so that what that was I will to more detail to that will be change the user needs no addition to start to be good without large levels at which it's a pretty good I'm I'm using it here in a large sense of eating warranties in the code whether it's much Mondavi series of my crew and in the booklets that you will find the urine who's on the far side on the right in my first night indicate that number two studies we have defined five levels analysis of proof achievements and so at the lowest level if you didn't have to know too much should be yeah I have a program that gives it a ten starts by me he's funny bit you might want to go further than that that's of course but you want few other patients to fully prove the group well we'll say about few minutes but what we want really here is that it's what super hard to get beyond the initial steps the last one will also little bit a background is manual truth is something very hard that couple that with the you little too want to do unless you approve me so we want money or food to be so looking at at these one of these in more details we all contract to be executed T States and debugs so cool that's using the eloquent about preconditions and postconditions if you are here in the produce Tokyo all about them as less this aspect three and posture so really our view now is that contracts are cool you can do as as well with contracts as we could in terms of usability integration you can do probably as as bad as in codes to pray these things spark helps you hear more respective but that maybe there's some additions to ADA so we were very pushy with the energy so that the including you gotta have some of the features which we really need it for proof qualify expression the ability to states properties of a collections expression functions the ability to abstract properties that you don't have to inline everything it's time or have to go to the body to state something that you will need in aspect will be crazy and will be completely contrary to this spirit of separating the spec and the body in particularly when we want to read to specifically properties just pounds or or things so so for these two will have we right but we pushed in up the alt and particularly so that this these two features were part of the the fact that the ADA are subsets is large there was a departure from the previous technology previous technology adds this correct by construction mode that sort of if you followed seven steps and restrictions was far easier to verify formally your program this is true unfortunately that's very rare that so you can follow all these constraints from the start you have to be in the reach nice situation where you start over and do everything as you're told from the start and you may need then to
completely change your ways of doing things that's really your pick up space so in the optic for something difference we say all these constraints they're going to be your colleague standard other tools we are bringing some of them are the troops we're gonna opt for every feature that doesn't make for modification across so we included almost everything but we still excluded to this day our pointers and exceptions all the rest is it so the particular all types these period types types with dynamic bounds restriction no no restriction from flows we can return from doing the loop anywhere it have complex hierarchy of packages that's not our business we know how to make sense of this is a separate issue preclusion again in many applications education in some talented or otherwise you might and that's okay because we can make sensitive generates there wasn't a template supportive generates in the position of ADA which was quite limited because the attempt was to change Eric's once and for all we will sit through allow any generates that below so we have it for something much simpler which is to analyze each instance we support drinks but in a way that may be less principled and before but much more progressive so for all these pictures or all types no restriction or to perform occasion particular the impact are there of good reason why they've all that supported because there are good reasons why they were so not supported before they can be quite difficult and and when when we implemented these we ended up with two birds along the years in the interference of types with dynamic ground particular complex upfront flow recursion really subtle bugs in how we generate the formula and which ended up in possible and soundness in the truth so when I leave today that's we have a good exists for these birds but that's that's one of the reasons why yeah ideally you want to put onto the hexagonal we made this choice to know as much as we could do and to focus on Sundays so of course each one of these these few banks that I mentioned were very very carefully to be sure that today we don't add them or anything that still the initialization of squad 2014 did not support in the markings so we felt when Dunham picked up here some people we're saying well you don't support of concurrency tags don't support data invariants at work just so we're thus acting as well if that's where you were doing a big jump over this we were going to be backward and oh honey you can see the previous business part with support things like leo so no dispatching calls with time type soon that will you over to a bit of bagpipes I was supporting some currencies in the booth called the heavens watch so restrictions of the rhythms card 4.0 but we opted for yeah let's let's get the tool set out and and we'll have a roadmap to ads these I start goodbye something else that's spark code from 20 starts after a few experiments were we were looking at the solution to mix it and for code we opted for something quite fine grain and at the same time prescribed by the user the reader can say exactly in their code word despot who leaves the tool can analyze this and not that that's quite possible to mix things that were supported with exceptional needs so the ADA subject is still expanding so we have a need among the years go programming including these patching combs and for this we use the the best that Tamiya has shown it's possible to do which is to show that derived classes are providing subsets of behaviors of the parent classes let's go the new name is this curve substitution principle for suppose that as that's one of the means to comply with own in a viola context now the do 178 is an external allows for a special supplement 200 400 that I tasting by so essentially this that's a true thing if I can precisely to but on the proof scene it means that when you derive the function sakaram your precondition must be weakened so you will accept to be called in more comfort than you do but you're potentially will be only stronger you know tell you four more deeply particular because you might be cold through this patching call with the static type that that is apology so that makes the kind of erases that we doing here function by function possible we re Circle protocol see the one year later so again using what pinned only produced energy so we support resins ribbon Scott really even the extensive reading stuff profile defined and contract to the previous technology we insisted on not adding host of annotations that you need to put in a good so it's mostly generate see all the things that are itself by wound worry about if I which tasks how to detect the podraces first I sanitation but let's user work when it means also it's it's next module so it will it be else on the program to really detect all possible support for type radius packing variance so I'm going to merge detail with our two types of data and variance Elena I will be now support those for why we have to do it one by one because in fact ADA is defining what this means you know time predictable 10:00 tomorrow dynamically which means that it takes at some points in the execution that's some completion of the required this is not enough people type pretty kids these are the things that should always hold true vertical scrolling Marines and type in various things that should hold outside of the defining package whether we can balance means that you're less good than this phony right just means that sometimes you have to break them when you define operations over you object I am to be able to prove them you have to be much quicker and much cooler to know these mentioned in any group of armed all you have to be able to assume them for couple when you enter a packet that is responsible for other objects and how painful that really these grantees are strong always the Englishman and so that we are to define stronger goals in implementing I find in annexing exciting one on which we are working now is the support for Polish under ship access parts in Iran inspire so era is really
which access types of pointers which protect no more problems one which is not regarded and is explicit when you do unchecked to the allocation the in check thing that can worry you is yeah but thematic saved allocation management of the brain and it's something that's all the languages like breasts are solves for programs by using this ownership we're a Puerto really hold really owns everything that the tree of memory that that sees underneath with mechanisms to borrow this this ownership when you are doing a temporary modification to move and so we have experimented with that last year we're lucky submissions have scientific conference for the underlying scientific mechanisms and to allow Europe for the proposal for the future data center you can also read the ADA issues 2014 if you go to the language library so so that's that's the thing that's cooking for I'll say the next two years because let's not be too ambitious the rules will be will take time to be verified for ADA and it that's a great technical work ADA in Sparta moving in the same directions although we we will certainly other slightly different and suppose package from the inspector than okay so users are lazy where our users but we want to have all result without in green work and in particular when we starts and we want to try out we rather just see what but good is needed for us before we test anymore it work that's why it was important that we can you can start will be Spanish in this book we know for the Jews so every surprise nature in fact it has a precondition and the first religion which is implicit needs a signature but all inputs of the programming are in there types and when you return all outputs are in their time there are some consequences in terms of what finish lies of course the spot is a bit scripted then either that when you passing things around it they have to be fully initialized in the pipes but that gives it a very reasonable there are defaults for sort of that then you need to know what are I mean inputs and outputs what are these down partners that's is it dark in the signature and give all marbles my D believe global in terms of having the lifetime of the program or syntactically scopes and so these what we call these global variables there are read and written by any given surprise directly indirectly suppose they are generated by Google so here again this analysis nationally is not modular it goes physical graph and collects all effects so that you don't have to do this work now when you would want to go beyond to your sphere satisfied with the tool you want to achieve more and you have to start do to work safely but what we claim now is that you can you need few or fewer annotations because Q is quite relative to where you start from Q for many would be no no no no agendas not possible and again it depends where you put your aim for something easy you will less work for something harder more party he was addicted so yeah poof and I said is mostly Madeira so blue Google analyzed using the very complex tools very rich eccentric solvers so program as a program which means that to analyze coves Google needs whatever information you give us additional conditions in particular in some cases we can do without because we have in line a mechanisms so internals of programs that have no contracts the tool unites them some some loops so but because the sepal for loops we involved so that you don't have to add the annotations in simple cases and things that that do not participate in the API with a device we leave the specification but things into no we'd like to skip all of them if possible you can factorize annotations example they tied variants they were really important to add to make support for this type of a stock events because not putting them means that you you should specify then for every pre first everywhere well many likes some of these they so that there's maybe 40 party relation here and now a lot also of these these benefits has to do with how we don't read formulas units I'm going to that that's the technology behind it completely replace with moji using state-of-the-art and all this direction of formulas you need much fewer loop invariants special kind of annotations daily forward sometimes you don't need to cut points so ways to simplify the the poop work just to show it in practice an example world you really need fewer deductions scheme that was contender for Shockley and the Western standards c-elysee permutation of death of Adam and rut Chapman who was at the time a leader of this movement Itron create wrote the export interpretation of that so this packet annotation so there's a skill about it and the spark ignition will be quite a lot of what you had many annotations for effects and appearances global amateur and depends there were many preconditions and postconditions I don't come here just a precondition because the precondition could be tens of lines of clothes so I counts conditions the things that you end together with our new conditions and there were lots of conditions in appearance as well there are loops there were a number of other patients to just do with the limitations of the tool in terms of scalability and even with that's yet to complete and about proof money so I was a huge effort for someone revolver expert in technology that's what some effort to prove absence of retainers from this point that's the situation to do today with different technologies we achieve evolved by anyone and that's that's religion so to end up with these supports manual proof so you don't so with that that's why you saw smoke on the left you have a formula that was directed by that could improve and some there but there's an encoding of your of place in the program of static path in your code and this H 1 H 2 correspond to the assignments calls or a state that were this bad we are encoding of all the other types and you have to prove this to children that might correspond to position or well when the estimated voters of the time didn't do you have to go through new module Pro possibly so this is no manual speeds were on the number of instructions to disprove that by this book and read these instantiate that and say from manipulating this this so this we will do at least not in this
shape because these formulas are really far from this is different language this is yet another language obviously place to develop language is so require too much efforts for the two people protect even though so what we do now is that we
don't get atomic Buddhist we support more with the shape of the arcs I sent you saw Bruce Oscar goes to be supposedly and the whole platform really targets all of these with adaptations to the for minerals and this really underworld art break and quantify properties that arise from you code the thing that we do at apart from this specialization the natural and feeling that we do is also terror in this is Central Grocery we really focus on put them in proof I not so much money improve like before and the user has some control over the strategy approve antibiotic so I'm going to that but that's an additive level when you use the place okay so I've roughly ten minutes to go over course projects good thing is that there aren't that many [Music] druggies from there because here before so if you are is your question that gillnets party and he has this quite rich library of thing that are useful in two locations that is mostly quickly this part one it chains reverse containers utf-8 for sure that were just and a few rappers on area code which rappers there so that they can be cool from Sporto typical also think that we do if they must have been delayed a bit make them another person certify is software for thought for this room for this or a smaller crazy playground between value and source the platform having the 30 fly is the software that runs on top of it to do the stabilization was coded by my colleague Andy replace ReactOS on these by Ravens car for pervaded every time I am the establishing communication code by in this part and the absence of bread after the tiger poop so there is a cool demo feature where you can let it fall and it lands we can do in this programs like that I choose in prototype in teaching research web companies so release who are using Chris apply for the pie thing and the jovem from such as i we use in teaching fully of I talking about Tim is developing this right through the middle world or aerial video architecture of this tutor language there is a tool generates area codes over Carina but of course all the all these things need to talk through this mail over so this mineral was produced me in area and now he's been moved to spark and it tells a bit of this story in in the prepare that you are going to find here that is I think the last you I will promise came from and the cool thing Zoe didn't attend several diverse group of some internal contracts for her this middleware and the coolest thing full of thing is that easily at radically less sterically history on you and they they went through this process of developing the this to adapting this familiar work from era easy to use on one side part and on the other side for the C equally equivalent to Reaper see two more cool absence of retires and possibly one because thing is that he did much faster and is colleague at some point that is not to say that it's impossible but ADA and spark marry make much easier will source so still come studies still the same people here it's true two pilots so there's no distance yet the public code repository but there will be but the end of the year it's still in doing so right now with the TVs in do two pilots is manual stabilized flights and the flight and really cool occupy nice part of the project to achieve really high level of safety for between three so the highest evolved little a Abdi edenic standards so spark is one part of the process to achieve that the reasonable cost and so spark is useful some putting some of the functionalities and also respect to X
glider by Martin Baker researcher from technical invention it's so firm were to control this and my big swing higher model to collect the weather data its launch from the balloon and replies how will you get it go to file and we did that over a very small period of time a few months achieves proof on the target absolutely there are impartial contracts and so you can also see the results and when I show here is that these are all the units of code although the green year has been booked for absence of covers and so fulfill properties the gray ones are the specs export and the black ones and so yeah it's ongoing projects already achieved a lot in the virtual time now it took in year
eventually at the beginning is that was led by Danny points and I'm from these products a few months one year project for the NSA today one face that it was possible to develop very high security software so VAR v is level with formal methods at original cost and so the cool thing is that all the try the artifact statistics on the original code are available from this webpage and you have a version that completed the translation to the spark 2014 the common rule which is part of the test which spoke was probably I which is the part of the examples that we just read with the reading now I'm ganna when is the largest spot open source projects is this a personal offer by again investigator kabuki so these two are researchers at University of scale and the work with sickness which is the CPG company in Germany so you look at the website we need to know all the details of the multiple features that they've been added since 2013 trains on x86 64 and the goal was got these very very small code base of three thousand lines of code with power three and put in the code in assembly it's very very secure software of mystic proof at sorts of containers the cool thing is that the legislation their websites it's unreal a choice of Copperfield so it is really functional I mean on delicate to use men functional supports Mikado and to put the same which is true is that the man is really a milestone in getting this push open source that is proof for absence of for covers X small Y it smell that can be multiplied by the others because of its small size and easy sequencing so if you interested in security look at this one as I said before the code was originally in the previous part and they managed to market it for cleaning and so now it's moving domestically something interesting is that's security is never ended battle you have to defend against the eternal realities of tomorrow and how to how best to illustrates the thing that we had with our approach then to see how well they did with madam and inspector before completely unexpected by the corporate community now that if you look at these emails that were sent and so you learn Mel down is punitive not visually by funded by the way that they selected very very small set of optimizations options to reduce virtualization and aspect is really mitigated and although it could be memorable it's it's much less than multiple possible other jumps so it's both security is not to supporting the system thing and in software is that sir be sure to think that other language but certainly the choice of simplicity and win for strong parties like it's so very fast spontaneity resources so there's a committee release every year make sure it will be bundled with nuts in one load and if you want to get the most part on this part there's a small difference between its policy events purport the number of two days deductions we only ship one with right now with what we call spec discovery so first degree is push on through and version for everyone but who is the one that for people repairs but on on the community version in fact you can install CPC for ng3 easily documented so please look at this to get the most of truth and particular some of the features that context apple will only be now she want to learn sport now there's plenty of online resources a top university and five multi class there's an another five thirty class which is not taking the website which is you can access it from the pepper and all of these will move to a new area and spark learning website from a recording dezer block will move to a decor blog mister I don't have plenty of resources to cover this you will find them the waiting that's some people on the community or producing learning your materials only and they kept using is part by example for teaching nothing better off would you say very nice the total it really think this part so if you produce anything like that let's do we are very happy to a bikini there are community events were we try to gather both open sourced and other community of a provision open in season one part so it wraps and researchers spoken from se days pharmacy has four days but I think everybody's here which show cured for the first time in 37 change little care against this year at National Institutes our sites are technologies in the US 27:28 so we're grateful ground which because anybody tells you happen to be there we have conditions upcoming presentation at conferences so Alexander simiiariy would happen to have presented his work at the embedded mobile intuitive just before me so if you look at security will be net both conferences in Berlin and they will be condition that obviously finally if you have to play this part and you're too lazy to download cool you can play with it this race winner it will be also pop websites your checkup
all stick around so full by clicking yeah so what's your first project no solution is either not impacted real time between