We're sorry but this page doesn't work properly without JavaScript enabled. Please enable it to continue.
Feedback

Concise Read-Only Specifications for Better Synthesis of Programs with Pointers

00:00

Formale Metadaten

Titel
Concise Read-Only Specifications for Better Synthesis of Programs with Pointers
Serientitel
Anzahl der Teile
13
Autor
Mitwirkende
Lizenz
CC-Namensnennung 3.0 Deutschland:
Sie dürfen das Werk bzw. den Inhalt zu jedem legalen Zweck nutzen, verändern und in unveränderter oder veränderter Form vervielfältigen, verbreiten und öffentlich zugänglich machen, sofern Sie den Namen des Autors/Rechteinhabers in der von ihm festgelegten Weise nennen.
Identifikatoren
Herausgeber
Erscheinungsjahr
Sprache

Inhaltliche Metadaten

Fachgebiet
Genre
Abstract
In program synthesis there is a well-known trade-off between concise and strong specifications: if a specification is too verbose, it might be harder to write than the program; if it is too weak, the synthesised program might not match the user's intent. In this work we explore the use of annotations for restricting memory access permissions in program synthesis, and show that they can make specifications much stronger while remaining surprisingly concise. Specifically, we enhance Synthetic Separation Logic (SSL), a framework for synthesis of heap-manipulating programs, with the logical mechanism of read-only borrows. We observe that this minimalistic and conservative SSL extension benefits the synthesis in several ways, making it more (a) expressive (stronger correctness guarantees are achieved with a modest annotation overhead), (b) ffective (it produces more concise and easier-to-read programs), (c) efficient (faster synthesis), and (d) robust (synthesis efficiency is less affected by the choice of the search heuristic). We explain the intuition and provide formal treatment for read-only borrows. We substantiate the claims (a){(d) by describing our quantitative evaluation of the borrowing-aware synthesis implementation on a series of standard benchmark specifications for various heap-manipulating programs.
Schlagwörter
Prädikat <Logik>GrenzschichtablösungMathematische LogikROM <Informatik>Lesen <Datenverarbeitung>Mailing-ListeUmwandlungsenthalpieÄußere Algebra eines ModulsAdditionHeuristikInhalt <Mathematik>Schreib-Lese-KopfResultanteProgrammierungZeiger <Informatik>SchlussregelBefehl <Informatik>ProgrammfehlerLogiksyntheseElement <Gruppentheorie>Mechanismus-Design-TheorieZellularer AutomatFestspeicherMultifunktionAggregatzustandInformationsspeicherungPunktMinkowski-MetrikKategorie <Mathematik>SystemaufrufMathematische LogikPrädikat <Logik>SchnittmengeBeweistheorieDerivation <Algebra>StandardabweichungParametersystemBenchmarkLesen <Datenverarbeitung>PräkonditionierungStrategisches SpielZahlenbereichHalbleiterspeicherGrenzschichtablösungDifferenteTVD-VerfahrenPlotterNebenbedingungQuaderProzess <Informatik>GrößenordnungMultiplikationsoperatorBitSubstitutionOrdnung <Mathematik>ExistenzsatzKonfigurationsraumCodeKartesische KoordinatenKollaboration <Informatik>InstantiierungEindeutigkeitSchaltnetzProgrammcodeRahmenproblemStörungstheorieBildschirmmaskeStrömungsrichtungSpeicherabzugCASE <Informatik>ClientSpeicheradresseSuite <Programmpaket>Wurzel <Mathematik>Konstruktor <Informatik>TopologieSpeicherverwaltungSoundverarbeitungKonditionszahlVollständigkeitKomplex <Algebra>Ein-AusgabeBruchrechnungKlassische PhysikProgrammverifikationWort <Informatik>Arithmetisches MittelFehlermeldungPhysikalisches SystemDatenparallelitätFramework <Informatik>Shape <Informatik>TermFunktion <Mathematik>Algorithmische ProgrammierspracheAbstraktionsebeneComputeranimation
Transkript: Englisch(automatisch erzeugt)