Logo: to the web site of Uppsala University

uu.sePublications from Uppsala University
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
An Active Learning Approach to Synthesizing Program Contracts
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.ORCID iD: 0000-0002-3063-6080
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems.ORCID iD: 0000-0001-7897-601X
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Univ Regensburg, Regensburg, Germany..ORCID iD: 0000-0002-2733-7098
2023 (English)In: Software Engineering and Formal Methods, SEFM 2023 / [ed] Ferreira, C; Willemse, TAC, Springer, 2023, Vol. 14323, p. 126-144Conference paper, Published paper (Refereed)
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.

Place, publisher, year, edition, pages
Springer, 2023. Vol. 14323, p. 126-144
Series
Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349 ; 14323
National Category
Computer Sciences Computer Systems
Identifiers
URN: urn:nbn:se:uu:diva-539620DOI: 10.1007/978-3-031-47115-5_8ISI: 001293530200008ISBN: 9783031471148 (print)ISBN: 9783031471155 (electronic)OAI: oai:DiVA.org:uu-539620DiVA, id: diva2:1902891
Conference
21st International Workshop on Software Engineering and Formal Methods (SEFM), November 06-10, 2023, Eindhoven, Netherlands
Funder
Swedish Foundation for Strategic ResearchSwedish Research CouncilKnut and Alice Wallenberg FoundationAvailable from: 2024-10-02 Created: 2024-10-02 Last updated: 2024-10-02Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full text

Authority records

Ghosal, SandipJonsson, BengtRümmer, Philipp

Search in DiVA

By author/editor
Ghosal, SandipJonsson, BengtRümmer, Philipp
By organisation
Division of Computer SystemsComputer SystemsComputing Science
Computer SciencesComputer Systems

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 124 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf