Logo: to the web site of Uppsala University

uu.sePublikasjoner fra Uppsala universitet
Endre søk
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet 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 (engelsk)Inngår i: Software Engineering and Formal Methods, SEFM 2023 / [ed] Ferreira, C; Willemse, TAC, Springer, 2023, Vol. 14323, s. 126-144Konferansepaper, Publicerat paper (Fagfellevurdert)
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.

sted, utgiver, år, opplag, sider
Springer, 2023. Vol. 14323, s. 126-144
Serie
Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349 ; 14323
HSV kategori
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
Konferanse
21st International Workshop on Software Engineering and Formal Methods (SEFM), November 06-10, 2023, Eindhoven, Netherlands
Forskningsfinansiär
Swedish Foundation for Strategic ResearchSwedish Research CouncilKnut and Alice Wallenberg FoundationTilgjengelig fra: 2024-10-02 Laget: 2024-10-02 Sist oppdatert: 2024-10-02bibliografisk kontrollert

Open Access i DiVA

Fulltekst mangler i DiVA

Andre lenker

Forlagets fulltekst

Person

Ghosal, SandipJonsson, BengtRümmer, Philipp

Søk i DiVA

Av forfatter/redaktør
Ghosal, SandipJonsson, BengtRümmer, Philipp
Av organisasjonen

Søk utenfor DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric

doi
isbn
urn-nbn
Totalt: 125 treff
RefereraExporteraLink to record
Permanent link

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