Global ETD Search
Search theses and dissertations gathered from participating repositories worldwide. Every result links back to the library that holds it. No account is needed.
Results
Showing 1 to 13 of 13 for “"K framework"”.
-
Rule-based optimization with K-framework
… optimization rules implemented using the K-framework and how much efficiency improvement achieved by use of our optimization rules.
-
A rewriting approach to concurrent programming language design and semantics
… To this aim, this dissertation describes the K framework, an executable semantic framework inspired from rewriting logic but specialized and optimized for programming languages. The K framework consists of three components: (1) a language definitional technique; (2) a specialized notation; and …
-
Closing the gap in the LLVM backend of K
In this thesis, we further develop part of the K framework, a framework for specifying and executing the formal semantics of languages. We dive into the LLVM backend, one of the engines for concrete execution, and implement key functionality that is present in the other concrete execution engine. …
-
Semantics of low-level languages
… utilize the K programming language specification framework to build executable models of the languages discussed: x86 and Tezos Michelson. We extend an existing formalization of x86 to include its most common format - executable binaries by implementing an instruction decoder. We start completely …
-
A language independent debugger semantics based debugging in K
… is a part of the suite of tools that form the K framework. Conventional language dependent debuggers rely on an ad-hoc model of the underlying programming semantics, and may thus be incapable, or inaccurate in their ability to rectify a program’s behavior. The K debugger uses a different approach …
-
A formal semantics of C with applications
… languages can be completely formalized in the K Framework, yielding interpreters and analysis tools for testing and bug detection. This is demonstrated by providing, in K, the first complete formal semantics of the C programming language. With varying degrees of effort, tools such as …
-
Semantics-based program verification
… languages. We implement the algorithm in the K framework, yielding the first language-parametric program equivalence checker. To demonstrate the practical feasibility of the language-parametric formal methods, we instantiate a language-independent deductive program verifier by plugging-in four …
-
A formal semantics of Python 3.3
… complex programming languages in the K Semantic Framework, which provides an interpreter as well as analysis tools for exploring the state space of programs and performing static reasoning about programs. This is demonstrated by means of a partial semantics for the latest version of the popular …
-
A formal semantics of P4 and applications
… formal semantics of the P4 language in the K framework. Based on this semantics, K provides an interpreter and various analysis tools including a symbolic model checker and a deductive program verifier. This thesis overviews our formal K semantics of P4, as well as several P4 language design …
-
A verification framework suitable for proving large language translations
Previously, researchers established some frameworks, such as Morpheus, to specify a compiler translation in a small language and prove the semantic preservation property of the translation in the language under the assumption of sequential consistency. Based on the Morpheus specification language, …
-
J-integral Computations for Linear Elastic Fracture Mechanics in h,p,k Mathematical and Computational Framework
… in h,p,k mathematical and computational framework using finite element formulations based on the Galerkin method with weak form and the least squares process. Since the differential operators in this case are self-adjoint, both the Galerkin method with weak form and the least square …
-
Intelligent Decision-Making for Autonomous Driving in Dynamic and Interactive Environments
… data concerns, a hierarchical decision-making framework is proposed, breaking down the complex decision-making problem into subtasks for improved convergence of driving policies. Third, a robust adaptive game-theoretic decision-making algorithm by utilizing receding horizon optimization and …
-
Translation validation for compilation verification
… to arrive to it. First, we present a formal framework for program equivalence checking that is transformation-agnostic and language-independent. This framework can serve as-is as the proof system for any number of Translation Validation systems targeting different transformation and/or …