• Refine Query
  • Source
  • Publication year
  • to
  • Language
  • No language data
  • Tagged with
  • 2
  • 2
  • 2
  • 2
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • About
  • The Global ETD Search service is a free service for researchers to find electronic theses and dissertations. This service is provided by the Networked Digital Library of Theses and Dissertations.
    Our metadata is collected from universities around the world. If you manage a university/consortium/country archive and want to be added, details can be found on the NDLTD website.
1

Drop-in Concurrent API Replacement for Exploration, Test, and Debug

Morse, Everett Allen 09 December 2010 (has links) (PDF)
Complex concurrent APIs are difficult to reason about annually due to the exponential growth in the number of feasible schedules. Testing against reference solutions of these APIs is equally difficult as reference solutions implement an unknown set of allowed behaviors, and programmers have no way to directly control schedules or API internals to expose or reproduce errors. The work in this paper mechanically generates a drop-in replacement for a concurrent API from a formal specification. The specification is a guarded command system with first-order logic that is compiled into a core calculus. The term rewriting system is connected to actual C programs written against the API through lightweight wrappers in a role-based relationship with the rewriting system. The drop-in replacement supports putative what-if queries over API scenarios for behavior exploration, reproducibility for test and debug, full exhaustive search and other advanced model checking analysis methods for C programs using the API. We provide a Racket instantiation of the rewriting system with a C/Racket implementation of the role-based architecture and validate the process with an API from the Multicore Association.
2

Javalite - An Operational Semantics for Modeling Java Programs

Wesonga, Saint Oming'o 04 November 2012 (has links) (PDF)
Java is currently a widely used programming language. However, there is no formal definition of Java's semantics. Consequently, Java code does not have a universal meaning. This work discusses recent attempts to formalize Java and presents a new formalism of Java called Javalite. In contrast to common approaches to formalization, Javalite is purely syntactic in its definition. Syntactic operational semantics use the structure of the language to define its behavior. Javalite models most Java features with notable exceptions being threads, reflection, and interfaces. This work presents an executable semi-formal model of Javalite in PLT Redex. Being executable means that Javalite programs can be run using this model. We then render the semi-formal model in the Coq theorem prover and present theorems stating that the operational semantics are decidable and deterministic. This formal model can then be used to facilitate research in areas such as proving properties of algorithms that perform various analyses on Java code, e.g. verification, optimization, and refactoring.

Page generated in 0.0262 seconds