Logotyp: till Uppsala universitets webbplats

uu.sePublikationer från Uppsala universitet
Driftstörningar
Det förekommer återkommande driftstörningar på några av sök-portalerna på grund av hög belastning. Vi arbetar på att lösa problemet, ni kan tillfälligt mötas av ett felmeddelande.
Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
An Active Learning Approach to Synthesizing Program Contracts
Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Avdelningen för datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.ORCID-id: 0000-0002-3063-6080
Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Avdelningen för datorteknik.ORCID-id: 0000-0001-7897-601X
Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Avdelningen för datorteknik. Univ Regensburg, Regensburg, Germany..ORCID-id: 0000-0002-2733-7098
2023 (Engelska)Ingår i: Software Engineering and Formal Methods, SEFM 2023 / [ed] Ferreira, C; Willemse, TAC, Springer, 2023, Vol. 14323, s. 126-144Konferensbidrag, Publicerat paper (Refereegranskat)
Abstract [en]

Contracts capture assumptions (preconditions) and guarantees (postconditions) of functions in a software program, and are an important paradigm for documenting program code, for program understanding, and to enable modular program verification. In this paper, we focus on contracts for stateful software modules, for instance modules implementing data-structures like queues. Such modules offer different kinds of functions to their environment: observers, which are pure functions used to query the state of the module; and mutators, which can change the module state. We present a novel technique to synthesize contracts for the mutators of a module, in which pre- and postconditions are expressed as Boolean combinations of the observers. Our method builds on existing algorithms for active learning of register automata to model the possible behaviours of the stateful module. We then present techniques for synthesizing contracts from a learned register automaton. The entire method is fully black-box and automated. Based on our proposed approach, we develop a tool called CoGent that generates a set of contracts for a mutator from a given register automaton of a module. Finally, we evaluate our tool using the APIs for various data structures.

Ort, förlag, år, upplaga, sidor
Springer, 2023. Vol. 14323, s. 126-144
Serie
Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349 ; 14323
Nationell ämneskategori
Datavetenskap (datalogi) Datorsystem
Identifikatorer
URN: urn:nbn:se:uu:diva-539620DOI: 10.1007/978-3-031-47115-5_8ISI: 001293530200008ISBN: 9783031471148 (tryckt)ISBN: 9783031471155 (digital)OAI: oai:DiVA.org:uu-539620DiVA, id: diva2:1902891
Konferens
21st International Workshop on Software Engineering and Formal Methods (SEFM), November 06-10, 2023, Eindhoven, Netherlands
Forskningsfinansiär
Stiftelsen för strategisk forskning (SSF)VetenskapsrådetKnut och Alice Wallenbergs StiftelseTillgänglig från: 2024-10-02 Skapad: 2024-10-02 Senast uppdaterad: 2024-10-02Bibliografiskt granskad

Open Access i DiVA

Fulltext saknas i DiVA

Övriga länkar

Förlagets fulltext

Person

Ghosal, SandipJonsson, BengtRümmer, Philipp

Sök vidare i DiVA

Av författaren/redaktören
Ghosal, SandipJonsson, BengtRümmer, Philipp
Av organisationen
Avdelningen för datorteknikDatorteknikDatalogi
Datavetenskap (datalogi)Datorsystem

Sök vidare utanför DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetricpoäng

doi
isbn
urn-nbn
Totalt: 125 träffar
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf