Program verification with SPARK - When your code must not fail

Video thumbnail (Frame 0) Video thumbnail (Frame 1979) Video thumbnail (Frame 5453) Video thumbnail (Frame 19423) Video thumbnail (Frame 25071) Video thumbnail (Frame 35750) Video thumbnail (Frame 42844) Video thumbnail (Frame 44177) Video thumbnail (Frame 44887) Video thumbnail (Frame 49944) Video thumbnail (Frame 50838) Video thumbnail (Frame 53594)
Video in TIB AV-Portal: Program verification with SPARK - When your code must not fail

Formal Metadata

Title
Program verification with SPARK - When your code must not fail
Title of Series
Author
Contributors
License
CC Attribution - ShareAlike 4.0 International:
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 and the work or content is shared also in adapted form only under the conditions of this license.
Identifiers
Publisher
Release Date
2018
Language
German

Content Metadata

Subject Area
Abstract
An introduction on SPARK, a programming language specifically designed for high reliability and used in safety critical areas such as avionics or railway signaling or in high security applications such as the Muen micro kernel or the WooKey, a secure USB mass storage device.
Keywords Alles

Related Material

The following resource is accompanying material for the video
Video is cited by the following resource
Component-based software engineering Programming language SPARK <Programmiersprache> Component-based software engineering Systems <München> Software Open source EASY <Programm> Information systems Compiler Operating system Compiler
Implementation Mobile app EASY <Programm> Typ Disintegration Function (mathematics) Objektorientierung Programmer (hardware) Windows Presentation Foundation Systems <München> Software Agreeableness Absolute value Buffer overflow
Dataflow Functional (mathematics) Mobile app Run time (program lifecycle phase) Code Mikrokernel USB <Schnittstelle> Cursor (computers) Mathematical analysis Function (mathematics) Atomic nucleus Cryptanalysis Variable (mathematics) Physical quantity Number Evolutionarily stable strategy Attribute grammar Windows Presentation Foundation Agreeableness Software Firmware Default (computer science) SPARK <Programmiersprache> Typ Statische Analyse Data storage device Division (mathematics) Variable (mathematics) Software Apple <Marke> Systems <München> ACCESS <Programm> String (computer science) Normal (geometry) Buffer overflow
Pascal's triangle Print <4-> Implementation Print <4-> Block (periodic table) Interior (topology) Code 3 (number) Cursor (computers) Variable (mathematics) Cursor (computers) IP address Geometrischer Körper MEGA Preprocessor ADELE <Programm> String (computer science) Hard disk drive Length Speicheradresse Default (computer science)
Laptop Flock (web browser) Structural load Block (periodic table) Typ Data storage device Cursor (computers) Propositional formula Cursor (computers) IP address Mach's principle String (computer science) World Wide Web Hard disk drive Length Buffer overflow Default (computer science)
Laptop Point (geometry) Carriageway Moment (mathematics) Cursor (computers) Cursor (computers) IP address Mach's principle Drucker <Datentechnik> String (computer science) World Wide Web Display Hard disk drive Loop (music) Computing platform Social class Default (computer science)
Typ Zielfunktion Codomain
Point (geometry) Software Interior (topology) Code Typ MIKE <Programm> Absolute value
Validation Module (mathematics) Dataflow Software Code Data type
ja Programm Verifikation mit Frage 2 wichtige Sachen es geht nicht um Patties
BAG es geht auch nicht um die Compiler Architektur es das wird gern verwechselt sondern es geht um die Programmiersprache was kurzes zu mir
Informationssystem Techniker Nötigung ich arbeite seit letztem Jahr für die Kommunen kommt Phonolith GmbH hauptsächlich in der Betriebssystem oder Treiberentwicklung mit das BAG und auch C und 7. das Plus wir entwickeln sichere Komponenten basierte Systeme im Mobilbereich im Industriebereich das ist er so weit es möglich ist auf Basis freier Software und es ist frei und den Bürger auch selbst freie Software im wenn in offen Entwicklung das heißt sie können aufgetaucht folgen wenn ihr das wollt und wir uns überlegt für sichere Systeme brauchen eine sichere Programmiersprache und sind an der Stelle zu Arda gekommen da ist ein ISO-Standard existiert schon seit 1987 wärs kontinuierlich erweitert worden so dass wir heutzutage moderne Sprache haben die
Objektorientierung unterstützt die Kinder X unterstützt und was ganz wichtig in dem Bereich ist die unterstützt extensive kommt Landheim checkst es und wir haben sehr sehr sehr starkes Typ Systemen Integrationen in das Ziel von fangt schon dafür ist das heißt wir können einfach mit in C geschriebenen bei ist interagieren und wir haben Konfekt bis vor können in Kontakt besten Programmen heißt ich habe Verträge an einer Software an die ich mich halten muss das ist ein Beispiel aus C ich habe die Funktion Apps die gibt mir den absolut wert ist der Eingabe zurück das steht in dem Kommentar das ist ein Kommentar der wird vom Kompalla von allen Sache ignoriert zum Vergleich dazu aber ich habe die Funktion erst wir jung die tut genau das gleiche und die hat einen so genannten es prägt das heißt dieser Aspekt ist eine in diesem Fall eine so genannte nach Bedingungen die angibt dass der das besser als der Funktion Apps Dallio größer gleich 0 sein darf und für den Fall dass das nicht passiert würde ich einen würde ich ein Fehler bekommen man dass die Implementierung der Funktion Erbsen zählen ist recht einfach Billard größer als 0 ist mehr zurück sonst gehen wir man ja zurück das funktioniert war minus 1 1 frei zum Ziel auf 1 1 freie und 4 0 und es gibt ein Fall für den es nicht funktioniert vielleicht hat jemand eine Idee der China der ist nicht symmetrisch und für den kleinstmöglichen Thatcher wird 2 auf minus 32 gibt es keine positive Darstellung das heißt die größte mögliche Darstellung surfen unter 2 hoch 32 minus 1 das heißt es bei dieser Operation läuft enthält über und wie bekommen den negativ dazu zurück so die gleiche Funktionen aller August okay die Erwartung ist ich bekomme 10 Fehler an dem ich bekomme 10 Fehler dass meine Ausgaben nicht mehr nicht positiv ist ich habe es aber gar nicht bis dahin denn er hat auch Overflow Checks auch in Thatcher werden
und der in Hettche an der Stelle minus J Überläufe diesen wert beendet das Programm bereits an der Stelle jetzt können wir vor auf unsere
Software testen so wird dessen trotzdem wichtig wir brauchen sie für Integration wir müssen validieren dass die den hinter der Software die richtigen Sinn aber wir können niemals alle Werte testen also schon für die einfache Funktion Erbs hätten wir über 4 Milliarden möglich Eingabewerte wenn wir 2 Zahlen addieren wollen dann haben wir 4 Milliarden mal 4 Milliarden möglich Eingabewerte und für jede nichttriviale Software ist einfach so viel dass es nicht mehr testbar ist und selbst die der Kunde das Testen unter besten Bedingungen schafft im besten Fall ein Fehler alle 1 Tausend Zeilen Code und mit formalen betonen können wir bis zu 50 bis 100 x besser werden als das das heißt wir hätten dann ein Fehler auf 100 Tausend Zeilen Code was uns die Möglichkeit gibt auch größere Software Projekte tatsächlich fehlerfrei zu implementieren jetzt komme zum eigentlichen Thema des Vortrags das BAG das BAG S 1 habe seit von da ist untersteht unterstützt uns bei der statischen Analyse und bei der formalen Verifikation der eben gezeigten Verträge das heißt wir können das alles bereits zu kommen Eltern überprüfen und wir haben auch Datenfluss Unabhängigkeit Überprüfungen ein Beispiel ist ich habe eine Verschlüsselungsfunktion die hängt ab von einem Klartext und von O von unseren Kiel und da kam dann Seifert Text raus und ich könnte mir zwar geht's beweisen dass dieses helfe Text tatsächlich eine Abhängigkeit von sowohl den Klartext als auch dem Keith und Dinki hat würde ich jetzt dort ein statischen Kiel in die Funktion einbauen würde der Beweis an der Stelle fehlschlagen und wir haben auch eine variable tiefe unsere Verifikation das heißt wenn ich war etwas wirklich ziehen will muss ich nicht sofort und in gehen ich kann anfangen mit einfachsten Variante Verletzbarkeit das bedeutet ich habe keine EXIST Zeit also für die 10 Menschen dessen Pointer und Funktion dürfen keine zum Beispiel keine Seiteneffekte haben wenn ich die Funktion Ettaler Abt das Bild ansehe darf die keine globale Variable manipulieren zum Beispiel eine weitere Stufe wäre die Abwesenheit von Laufzeitfehlern das heißt ich habe keine Overflows keine ekstatisches in der Software ich kann beweisen diese Software unter den gegebenen Bedingungen niemals abstürzt und die nächste Stufe für die einen erheblichen Mehraufwand auch gefordert ist der Flug ist eine vollständige funktionale eine ein Vorschläge funktionaler Beweis sei ich habe jeder Eigenschaft diese Software bewiesen nicht nur dass sie nicht abstürzen auch das exakt das tut was sie spezifiziert haben wie funktioniert das wir haben unseren Cord C alle Spiele und unser Tool unsere Beweise gehen daraus nicht irgendwelche Beweise sondern sie generieren zu erst einmal Beweise Verpflichtungen wenn die durch B Teile habe ich beide Divisionen keinen oder hat nicht durch 0 teilen also generieren wir die Beweise Verpflichtungen B ist ungleich 0 wenn ich den Code beweisen möchte dann muss ich an in dieser Zeile Code nachweisen dass B nicht den Wert 0 annehmen darf annehmen kann ich mache das Beispiel von vorhin einmal weiter unten setze immer die die Ausgaben des des zu ist es knapp los am angegebenen und an dieser Stelle sagt uns das knapp 5 bereits wir können ein Overflow Check haben wenn wenn der Wert J minus 2 hoch 32 annimmt das können wir wieder um verhindern indem wir unseren Vertrag an unseren Vertrag angeben dass die Eingabe in diese Funktion diesen wird nicht annehmen darf Interceltique für das bedeutet in diesem Fall also das das Zicke ist ein sogenanntes Attributen Ader und Fürst ist der 1. spricht der kleinste der den der in Thatcher kennt in diesem Fall minus 2 hoch 32 und der mehr sagen als Vorbedingung für unsere Funktionen haben wir möchten wir dürfen diesen Wert nicht übergeben da können wir beweisen unser auch auf laut Check den wir eben hatten beweist denn dieses dieser Wert kann ich mehr auftreten und unsere nach Würdigung beweist in der Stille für sich von ganz allein mit den wenn ich alle negativen werden die Tiere werden sie größer 0 jetzt benutze ich diese Funktion in einer ganz normalen plus Dittsche ich versuche das nicht für nötig den Beweis über diese Apple der auch über diese Funktion und an dieser Stelle ich habe keine weiteren Checks und der sagt mir natürlich meine vor Würdigung kann viel kann fehlschlagen wenn der mehr wert von Balliol Dénes die entsprechende sprechen wird angenommen hat das kann ich einerseits ganz einfach lösen ich sage okay ich rufe die Funktion Apps nur dann auf wenn der Wert nicht angegeben worden ist also sagt dass mir die Pflege kandischen also die Vorbedingungen wurde bewiesen aber ich habe von so aber er hat ein sehr sehr stark ist tipps Systemen und ich kann einfach etwas viel eleganteres machen ich sage ich definieren wir ein und hielten das symmetrische in Thatcher der geht von minus 2 hoch 32 plus 1 bis minus 2 2 auf 32 minus 1 heißt es von Plus bis im negativen und im positiven Bereich gleich groß ich verliere dadurch einen wert aber diesen wird kann ich sowieso nicht bearbeiten und sage die Funktion als 2 junge darf an der Stelle nun nach diesen Typen verwenden und hoch und ich brauche die Vorbedingungen nicht mehr denn die Vorbedingung wird implizit durch den Tüten auffällt wenn ich das jetzt beweisen möchte wenn ich sehen dass der ORF lautstark nicht mehr auftritt denn dieser in Thatcher kann bei den Regierungs- Operation nicht überlaufen asymmetrisch ist und an wenn ich das an dieser Stelle kann es kann ich auch in der darüberliegenden Funktion einfach sagen ich verwende einen symmetrischen in Thatcher und kann mir meine manuellen Schecks sparen denn alle diese Checks werden von der Sprache übernommen und die gibt es auch keine Beweise Verpflichtung mehr denn der Typ enthält bereits alle Eigenschaften die wir haben möchten so wurde das Ganze verwendet in vielen Dingen die man täglichen und nicht ganze täglichen Leben sehen kann also ins heftige Bereich ist Fliegen Rolls-Royce-Triebwerke deren Software Essens Bad geschrieben und die hängen so weit ich mich entsinnen kann an dem ein oder anderen Airbus dran mit dem man in Urlaub fliegt im militärischen Bereich Euro da zum Beispiel verwendet Frage aber auch da haben Signalsysteme der Bahn die halt nicht versagen dürfen beziehungsweise auch um in der Raumfahrt kann ich mir nicht leisten kann ich halt einfach ein Techniker im Weltraum schicken Mantel beliebten Mädchen soll die Software muss funktionieren Security Bereich im gibt es denn nur in Mikro Kern als ein Mikro kann der auf die Abwesenheit von Laufzeitfehler also bei dem die Abwesenheit von auf Zeit Wesens das heißt es die Software stürzt nicht ab beziehungsweise von der am französischen IT-Sicherheitsbehörde der ansehen gibt es die sogenannten okay der Konzil USB-Dongle darstellt dessen Firmware ins Bad formale infiziert worden ist und der gegen diverse USB Angriffe damit geschützt ist so einen ich versucht noch ein praktisches Beispiel einzubringen an der Stelle vielleicht irgendjemand nicht ganz folgen kann mich bitte kurz und Handzeichen unterbrechen eine kurze Einführung in ganz Frings in The ins zwingen zerissen Pointer auf das Stück Speicher und am Ende liegt man 0 und wenn die nur dann ich liegt dann glaube ich aus man Speicher raus und das geht alles kaputt ich habe auch keine explizite Längenangabe wenn die nur dann ich liebe weiß nicht wie lange der Speicher hinter dem unter ist und schönsten aber sind aber ist die haben immer an bestimmten Objekttypen der angehörte eingereiht wird in diesem Fall ein Charakter was ist wenn werden soll und alle essen aber haben eine explizite Größe in meinem Beispiel werde ich einmal an der Ostsee darauf aus aufrufen einfach um quasi zu verdeutlichen wie schön das Interface ist ich werde deswegen wenn an die Funktion übergeben und denn wiederum romanischen ein anderes wenn um und für diese Meinung Funktion am möchten wir ist das Ziel zu beweisen dass sie 1. nicht abstürzt und zweitens 1 0 Pointer oder ein lernst schwingt immer mit einem bestimmten die Fort Wert dafür immer bestimmten die vorbeiplätschernd wieso ist hoffen wir dass es klappt aber Wirtz Sorge haben unsere man
period sehe ganz kurz der meine Messer stehe wird 0 initialisiert welche Argument übergebe das heißt sie kann auch nur sein aber in jedem aller feine benötigt um bestimmte Wand Time Eigenschaften von aber zu haben und die Funktion tönt importiere ich aus einer A 1 A der Videothek
dies hier definiert also wie gesagt es unser schönes Interface ich sage ich habe die Frau zu doppeln die nimmt einer als es zum kommt etwas das Pointer und eine maximale Länge und ich exportiere die Nacht sehr und dieser oder Print heißen implementiert es die recht simpel kurze Anmerkung dass wir es oben sind im Prinzip 10 Clouds nur sehr viel schöner also ich habe mich einfach irgenwelchen Präprozessor kaut dran sondern es ist wird es sind tatsächlich semantische Pakete die Funktion brennt es implementiert sie bekommt Ostens Vigneault Testpaket können wird aber was wir beweisen möchten übergibt den Pointer ein die Vorzüge und die Länge und ich erhalte daraus ein anderes schön billig danach einfach ausgeben kann das können wir zum interessanten Teile die Funktion von virtueller die hat eine nach Bedingungen der C ist schön 1 0 Adresse ist dann sollte die Fortzügen zurückgegeben werden kurz zur Einführung noch ich habe noch eine Funktion längst das machen müssen Konzept das schön längst in 10 nun aber implementiert und als nach Bedingungen sagen wir das Ergebnis ist auf maximal so groß sein wie die maximale Länge sonst wäre es keine maximale Länge Implementierung es ganz einfach wir lesen zu als die länger aus lesen dass sie länger aus den wir müssen vorher wissen wie lange es schön wird den Generälen wären Objekt entsprechen länger Insider 40 das im instanzieren das müssen wir irgendwie initialisieren ja ja Schulungen und zwar das ist eine Pascal heutige Syntax und wir haben einen deklarativen und einen Funktionsblock an der Stelle bis der deklarative Block von dem ist und dem Beginn begrenzt wird müssen wir alle deckt alle Variablen die wir verwenden wollen vorher deklarieren somit ist sichergestellt dass Sie nicht dass wir immer explizit wissen was Herrn Spa ein an Variablen zu Verfügung haben und auch nicht irgendwo Unkraut am Objekt auftauchen die ich kennen und dem Beginn Block wird der wird wird der Funktionscode abgehandelt genau wir sagen wenn die Länge größer 0 ist dann bitte reden wir über den Szenen die mir gerade erklärt haben und Gerd Schaar nimmt den Pointer und gibt uns den den Charakter an der Speicheradresse zurück und dann fügen wir diesen Charakter ins Schlingern entsprechen Stelle ein und wir haben noch die Eigenschaft wenn der Cursor klar wenn der Cursor größer gleich dem letzte Element unseres Freundes also der höchstmöglichen Speicheradresse ist brechen wie die Schleife ab und wenn das nicht der Fall das heißt wir noch nicht einer höchste speicherte sind dann können wir implementieren das schützt uns nicht zwangsläufig da vor dass wenn
Speicherfehler erhalten weil der C Pointer kann einfach auf dem Block zeigen die uns gar nicht gehört und wir können das nicht überprüfen aber es sitzen sah vor dass wir am Ende des Speichers sind nicht versehentlich einen Overflow generieren zur jetzt beweisen wir das pro
Laptop und schauen was uns das Programm sagen würde es dauert immer alles ein bisschen also beweisen es keine einfache Sache der Beweise aber hat bestimmte Eigenschaften es nicht determiniert wird aber für alles was uns bewiesen wird gilt die Garantie dass das nicht fehlerhaft ist okay das haben wir hier jetzt kommt das nicht mehr vor genau jetzt haben wir da ein das kann man leider nicht sinngemäß mit Lauben das ist dass dass ist da steht das sagt uns ein Mensch steckt wohl ist bewiesen worden und längst Stärke darin steckende längst checkt kommen durch den Zwängen weil wir haben für für er habe quasi die Mensch das Typen und die Länge dass er es ist schön und den das handelt heißt das was nicht bewiesen wurde eigentlich sollte uns das da unten ach genau das ist die Pflege könnte schon bald versteht dort und zwar wenn der Cursor 0 ist und Gerd Schah das auf Speicher zugreift hat eine Vorbedingungen dass der Cursor niemals 0 sein darf und was wir haben ist diese Bedingungen ist L größer 0 und diese Bedingungen gibt sich aus unserer längst Funktion denn diese längst Funktion läuft und läuft über den Speicher und die wiederum hat selbst initialisiert L mit 0 und sagt wenn der nur der Pointe nicht 0 ist dann laufen über das Ereignis werden wir finden aber wenn es ist dann mitteln wir sofort L das heißt wenn etwas größer als wenn wenn wenn das wird ja unter größer als 0 ist dann gilt die Eigenschaft dass der Pointe den wir da vor der 3 getan haben Groll er nicht nur sein kann und das müssen wir es irgendwie ausdrücken das klingt erst mal recht komplex aber was Sie machen können ist der Film an der längst Funktion eines ein sogar einen sogenannten Konfekt Käs anerkannt verkehr ist spezifiziert für bestimmte Ausgabe wird die möglich sind bestimmte Eigenschaften das heißt kommt Viertklässlers fragen wir längst ich halt das muss ich schicken ach ja meint sie ist schön genau halt Beispiel bestimmt Eingabewerte nicht ausgewählte also unsere C ist schön ist eine 0 Pointer dann gilt unseres zahlt ist kleiner gleich 0 und im zweiten Fall also die müssen noch feuchten ist eine kann ich sagen wenn das Geld geht es an geht das bestimmte müsse es auch ja ja er wird schon an der Stelle in Thatcher wenn wir sagen gleich 0 müssen wir gleichzeitig beweisen dass der Fall kleiner 0 niemals auftritt das heißt wir würden das nicht vollständig beweisen können wir keine Aussagen nur Werte ab 0 dann könnte man sagen gleich 0 soll müssen den zweiten Fall noch betrachten heißt was ist wenn es nicht 0 ist Größe Kölsch ja das heißt im Prinzip besagen größer vergleichen oh ja das wird ein genau das heißt wir können für die nur keine Aussage treffen wenn man eine 0 bekommen das wird an der Stelle nicht ist 0 Pointer oder nicht aber das macht nichts den wenn wir 0 bekommen wenn wir unseren die Forts schönen zurück so wir die Eigenschaft sagte 2. Ich habe noch Zeit versuchen dass es zu beweisen werden gleich sehen ich habe ich mich vertippt das schon mal gut so ist wenn wir so weiß immer noch nicht zwar geplant denn wir haben hier die Funktion zu Pointer und zwar haben haben wir unseren Typen Pointer und diese Funktion zu Pointer macht und unsere System period schönes einen selbstdefinierten Pointer Typen da wir da Geld Schar vor auf diesen poltert schieben vorbei ist und wir gerade in bewiesen haben dass diese das der C ist für ihn nicht nur sein kann kann diese Verknüpfung noch nicht hergestellt werden das heißt Sie müssen die Funktion zur Pointe anschauen stellte unten und die nennt also zum Bund etwas Mütter und einen Pointer und auch für die müssen jetzt Eigenschaften definieren dass wir sagen wenn das Ei 0 Pointer ist dann werden wir eine 0 Adresse bekommen dann bekommt auch eine Pointer und wenn wir keine 0 Adresse bekommen bekommen wir keine 0 Pointer das heißt anschlag nicht oh dann ja ich mach wirklich
gleich so Konflikte ist so was wir
gesagt haben wenn unser Adresse eine 0 Adresse ist dann mit schon der 0 Pointer wenn es keines mit keine jetzt kommt der große Moment habe ich mich vertan habe es beweisen wir das und ich habe mich vor ja das jedenfalls tatsächlich und Lessing semicolon ab nur das Problem das ich sehe auf meinem Laptop nicht ganz alles weil das Display vom meinem Laptop kleiner als ist das Plattform jetzt kompiliertes und ist beweist und das dauert und für könnte schon bald während es begleichen und ist schön gleich aber 0 er jetzt an wir zwar jetzt können wir sagen okay es kann aber ist alles anders machen will und eigentlich müsste es jetzt beweisen das ist wir checken war ob ich ihr sagen können Cursors und gleich 0 falsch nicht da sondern indem er nein und zwar ich kann es Partner hinschreiben und der der Punkt dass wenn ich das packe meine Strategie das ab dieser Stelle und das Pferd beweist dann nicht mehr also das packt man muss auch bewiesen werden ich habe es auch einen Pack meine grüne Markierung das ist bewiesen wurde dass es stimmt das heißt wir haben tatsächlich an der Stelle bewiesen dass unser Cursor dort keine Pointe sein kann warum kann das Schleife sein Schleife auf Schleifer wo wir so eine komplexe Sache müssen zwar geht's erklären dass sich dieser Cursor in der Schleife nicht ändert und dafür gibt es sogar eine Schleife in Varianten die und das Schreiben Prinzip genau das Gleiche rein sagen dieser zwischen gilt in der Schleife für jeden Aufruf und beweisen das und es beweist das heißt ich habe es an der Stelle bewiesen obwohl ich nicht explizit darauf checke das ist dass der Pointe nicht verwendet keine 0 Pointer ist aber nicht die Eigenschaft der Funktion längst und durch die Eigenschaft dass ich quasi die länger an die an die Eigenschaft ist Pointers Koppel der kann ich in der Schleife auch beweisen dass diese Pointe niemals 0 werden kann heißt haben Check gespart und das ist immer noch alles kommt das Programm ist noch niemals gelaufen das heißt ich habe hier eine im Prinzip eine Klasse von Fehlern ohne einen einzigen Programmaufruf bereits eliminiert also das ist auch was was nur schwer zu testen wäre so mir wurde gerade ein Zeitzeichen gegeben deswegen würde ich jetzt in die Fragerunde übergehen ich hoffe es hat Euch was gefragt so von wir fordern bitte nur eine Frage
okay und zwar nächsten Aufruf an solche bei denen sie Metrik in Täter bei C Beispiel Walzer ja ich im gemütlichen gefallen sind bisschen weil es kommt darauf an was wir 2 was wenn in der erpressen ist und was Komplimente einer
Kompliment meine Frage setzt wenn dieses Image mit in jetzt alles in die eigene zwischen 40 Aufrufe zur Verfügung stellst könntest du das werden die können es ist eigentlich nicht mehr dazu kommt Freizeit stecken also hätte sein auch an die Frank B wir genauso wie wenn du nicht mehr und dass wir bei den nicht mal terminierten Svingen passiert auch soll 2 also man muss über wenn man mit 10. agierten muss man die API-Aufrufe so anpassen dass sie Typen stimme ich kann diese mehr Check-ins nach C übergeben das heißt der Wertebereich denn der Zielfunktion ankommt wird immer diesen somit weg
in sein weicher voll bewiesen habe also geprüft habe dass das der Fall ist aber und sie ist diese Eigenschaft weg wenn sie habe ich meine Int des 32 Bit auf die er auf den Sprecher Architektur und damit ist die Eigenschaft weg ich kann die Typen da nicht verwenden in also der der Punkt das Wasser machen würde es ist im Prinzip was ich jetzt gemacht habe das 7. übernimmst was aus C und unsere längst Funktion hat auch keine Vorbedingungen weil ich weiß nicht was kommt es keine 0 Pointer kannst kann irgendwas komme ich kann
überhaupt keine Eigenschaften wird sie beweisen das heißt du musst diesen dafür sie so bauen dass Suche nach C explizite nach mit er wenn du in einer etwas zu begibst für dich selbst solche nach Bedingungen des ist das Ziel damit umgehen kann und gleichzeitig eine was aus C benimmst gar keine anderen triffst weil du weißt nicht was sie alles kaputtgemacht werde vor als eine Frage beantwortet einmal Wortmeldungen der Beweis war jetzt nicht besonders umfangreich wie lange dauert es dann im realistischen Szenario Sinn Beweis wirklich durchzuführen der Beweis den habe ich vorher schon mal gemacht da habe ich mir nicht gerade gerade nicht ausgedacht der Punktes man fängt man also es ist er in der deutlicher mehr Aufwand des dafür zu beweisen dann schreib sie und dann funktioniert dann kann so sie aus wenn sie period die Taschen Asthma an um dann von den Punkt zu kommen lassen Software die es irgendwie funktioniert und das ist auch der über die der formal gezeigt heißt dass sie nicht abstürzt raus so tendenziell noch mal so lange wie dafür dass die so viel geschrieben hast der Vorteil ist das Sicherheitsgarantien die mit testen nicht erreicht so hat 2 Fragen aber noch kaum ist er da geschrieben also bitte genau also es barg ist und die Theater in der Retorte Restaurant Uhren C in der Währung also da muss eigentlich bewiesen werden dass es sich um haben was er da als führt auch zu 100 Prozent korrekt terminiert die Wohnung ist der Interpret äußeren Zweck geschrieben aber es nicht interpretiert der der der spezifischen Prozess aus steckt wo du nur über mehrere 100 Prozentig den Alltag oder ausführen da ist nicht interpretiert aber wird kompiliert direkt nach bald kommt es gibt in der GCC von den Fahrer was im Prinzip in Bad Code kompiliert der springende Punkt ist du vertraust den GCC genauso wie du dann aber kam keiner vertraust an der Stelle muss den Tools Vertrauen nichtsdestotrotz finden diese Tools Fehler für dich diese alleine unter Umständen nicht gefunden oder nur sehr mit sehr viel mehr Aufwand gefunden hättest und der zweite Punkt ist es gibt immer noch die Garantie dieses Tool zeigt ein Beweis nur dann als bewiesen an wenn es Ihnen tatsächlich bewiesen hat und das heißt das Tool kann ihn nicht zwangsläufig beweisen was hat wir um es ist was keine Phosphor das heißt dass keine Akte akzeptierten Beweise die nicht korrekt sind es kann aber passieren es ist wohl nicht meine Lage sind das zu beweisen und dann siehst du wirst du es nicht schaffen das zu beweisen aber das heißt nicht dass es nicht korrekt ist also wenn die Korrektheit nachgewiesen wurde dann ist es korrekt die genauen technischen Details darüber würde ich an der Stelle er Kurt der Firma die das Tooling entwickelt überlassen ich fasse die letzten das Leid
vergessen ja das werde ich jetzt es leid gewesen für die Fragen ja eine Frau wollte immer noch Maria oh je nimm meine Frage war zu ich ich versucht das wäre für mich zu verkaufen sie jetzt nicht 7. plus nehme meine da wir Frage was kann ich jetzt erschlagen Siemens der Legende leiser nur wenn so meine Frage bietet den da zumindest oder das Bagdader im sowieso in die quasi Validierung an weil mir des gehe vorgeschlagene Thema
Beispiel ist der von der Ariane-Rakete war dann auch eher so dass sich in so Modulen die sich dann die Sachen explodiert haben über die in die ei und Kansas irgendwie Beispiel oder bei dem ich Probleme ein die du jetzt das mal nicht so mehr ja genau wo das wäre beziehen kann so zu mir so sogleich Beispiele wurde weiß man Geleise dazu wirklich schwierig und das habe ich bis Ende März BAG quasi verhindern können so weit wir haben dann kommt bei der hat Bush stimmte Namen was die er die eine trifft Nitsche Preußen ich selbst das Problem ich habe was bewiesen es kam auf einmal andere Ergebnisse aus sich eben bewiesen hatte dass rauskommen können springe Punkte sich haben Datentypen verwendet aber kleiner als 8 Bit und mit Datentypen die kleiner als 8 zu nahm sich Kompalla gerne schwer an der Stelle muss man sehr genau wissen was man wie sich da kommt verhält was zu beweisen kann es an der Stelle ist die Semantik eines großen kann es beweisen dass bestimmte Datenflüsse in den Code so stattfinden dass er an aufgrund dieser Daten so nicht abstürzt wenn dann Kompalla auf einer Art bestimmen Architektur aufgrund bestimmter Architektur alle anderen Dinge tut gibt auf die du keinen Einfluss heißt und die dann dazu führen dass Speicherbereiche sich verändern oder du hast kreist auf Sensordaten zu den Sensorfeld aus und gibt der Werte die eigentlich laut so Datenblatt gar nicht erlaubt sind dagegen kannst dich nicht wirklich schützen trotzdem kannst du schon enorm viele Fehler aus der Software halten alle die Fehler die du jetzt noch drin hast hast auch drinnen oder sind Sie wenn Zirkus bloß schreibst ALDI Compal der Tricks allen die Axt im Kompalla da hast du auch und sie also das schützt dichten darf da vor stützt sich auch an an eine andere Sprache nicht
Feedback