View Item 
        •   Utrecht University Student Theses Repository Home
        • UU Theses Repository
        • Theses
        • View Item
        •   Utrecht University Student Theses Repository Home
        • UU Theses Repository
        • Theses
        • View Item
        JavaScript is disabled for your browser. Some features of this site may not work without it.

        Browse

        All of UU Student Theses RepositoryBy Issue DateAuthorsTitlesSubjectsThis CollectionBy Issue DateAuthorsTitlesSubjects

        Partial Order Reduction in Symbolic Execution for Object-Oriented Languages

        Thumbnail
        View/Open
        Thesis.pdf (666.9Kb)
        Publication date
        2024
        Author
        Vrooman, Jesse
        Metadata
        Show full item record
        Summary
        The path explosion problem is a significant issue for verification tools that use symbolic execution. Monotonic partial order reduction introduces a sound and complete method of pruning paths irrelevant to the verification process. It does this by finding dependencies within transitions, chaining them, and determining if a computation can be considered quasi-monotonic; if not, the path can be pruned. The algorithm does not clarify possible dependencies between symbolic or concrete references to objects and arrays that must be considered when pruning paths in a concurrent object-oriented language. The contributions made by this research are the extension of the original monotonic partial order reduction method, as well as a performance study of the algorithm when implemented in a symbolic execution verification tool. After a comprehensive, in-depth look at the monotonic partial order reduction algorithm, it was implemented in a verification tool for an intermediate object-oriented language called OOX. When testing the verification tool using many benchmark programs, it is shown that the algorithm remained sound in the pruning of paths and is complete over most scenarios (does not allow for pruning paths using assumptions made over symbolic references). The testing also showed that the algorithm caused a significant increase in performance when compared to not having any form of path reduction, and a simplistic reduction method.
        URI
        https://studenttheses.uu.nl/handle/20.500.12932/47436
        Collections
        • Theses

        Related items

        Showing items related by title, author, creator and subject.

        • The evaluation of the Conductive Education program and the implementation of a Cognitive Stimulation program in a home for children with developmental disabilities in a rural area of South Africa. 

          Vos, R.V.; Westrhenen, N. van (2010)
          Samenvatting: Introduction: A Conductive Education (CE) program and a Cognitive Stimulation (CS) program were implemented in Sizanani Children’s Home, a residential facility in South Africa for children and young adults ...
        • The evaluation of the Conductive Education program and the Cognitive Stimulation program in a home for children with developmental disabilities in a rural area of South Africa 

          Mathot, A.F.; Velzen, J.M. van (2010)
          Introduction: This research evaluated the effectiveness of two developmental programs given in the Sizanani Children’s Home for disabled children in Bronkhorstspruit, South Africa. The Conductive Education (CE) program ...
        • Serving the Community; What are the individual and programmatic determinants for a corporate social responsibility program developed for high potentials in a talent management program? 

          Miert, I.C.J. van (2012)
          In the ongoing globalization, it becomes difficult to attract the talents that are suited for an organisation as Philips. Previous research shows that organisations need to innovate and listen to the needs of the High ...
        Utrecht university logo