Toward a Taxonomy of Typestate Systems: Soundness Without Alias Information

dc.contributor.authorBai, Billy
dc.date.accessioned2025-04-14T13:13:34Z
dc.date.available2025-04-14T13:13:34Z
dc.date.issued2025-04-14
dc.date.submitted2025-04-10
dc.description.abstractExternal third-party APIs are commonly used in real-world programming. Specifications or protocols are given by the designer to direct the usage of those APIs combined. The violation of specifications may crash the program, or weaken or break the guarantees of the framework, which would be vital to some safety-critical systems such as encryption. Typestate system is one of the approaches to check the valid use of APIs based on a given protocol. However, the soundness of the general typestate system relies on the soundness of external alias information. Obtaining whole-program alias information is often expensive and inefficient. One way to remove this dependency is to restrict the protocols. This work tries to examine the class of protocols that can be soundly checked without alias information. We formalize the notion of the protocol and the typestate system, from where we further construct some special classes of protocols. We identify the group of typestate systems called the accumulative typestate system, which is a superset of typestate systems that can be checked soundly without alias information. We also pin down two groups of accumulative typestate systems that are actually sound without alias information.
dc.identifier.urihttps://hdl.handle.net/10012/21581
dc.language.isoen
dc.pendingfalse
dc.publisherUniversity of Waterlooen
dc.subjectprogramming languages
dc.subjecttypestate systems
dc.subjecttype systems
dc.subjectregular languages
dc.titleToward a Taxonomy of Typestate Systems: Soundness Without Alias Information
dc.typeMaster Thesis
uws-etd.degreeMaster of Applied Science
uws-etd.degree.departmentElectrical and Computer Engineering
uws-etd.degree.disciplineElectrical and Computer Engineering
uws-etd.degree.grantorUniversity of Waterlooen
uws-etd.embargo.terms0
uws.contributor.advisorGurfinkel, Arie
uws.contributor.affiliation1Faculty of Engineering
uws.peerReviewStatusUnrevieweden
uws.published.cityWaterlooen
uws.published.countryCanadaen
uws.published.provinceOntarioen
uws.scholarLevelGraduateen
uws.typeOfResourceTexten

Files

Original bundle

Now showing 1 - 1 of 1
Loading...
Thumbnail Image
Name:
Bai_Billy.pdf
Size:
384.67 KB
Format:
Adobe Portable Document Format

License bundle

Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
6.4 KB
Format:
Item-specific license agreed upon to submission
Description: