Sökning: "compiler correctness"

Visar resultat 1 - 5 av 9 avhandlingar innehållade orden compiler correctness.

  1. 1. Proving the correctness of a virtual machine by a bisimulation

    Författare :Mikael Rittri; Chalmers tekniska högskola; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; stack machine; snapshot; one-step reduction; interpreter correctness; verification mapping; bisimulation; operational semantics; compiler correctness; SECD--machine; context; McGowan mapping; state-trace; debugging;

    Sammanfattning : .... LÄS MER

  3. 2. Programming Language Primitives and Tools for Integrated Real-Time Systems Development

    Författare :Saranya Natarajan; David Broman; Haibo Zeng; KTH; []
    Nyckelord :TEKNIK OCH TEKNOLOGIER; ENGINEERING AND TECHNOLOGY; TEKNIK OCH TEKNOLOGIER; ENGINEERING AND TECHNOLOGY; Real-Time System; Programming Language; Compiler; Informations- och kommunikationsteknik; Information and Communication Technology;

    Sammanfattning : The correctness of real-time systems depends on both its logical and temporal correctness. Typically, real-time systems are developed in several steps. First, the application is divided into a number of recurrent tasks and implemented using a programming language. LÄS MER

  4. 3. A Verified Theorem Prover for Higher-Order Logic

    Författare :Oskar Abrahamsson; Chalmers tekniska högskola; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; NATURVETENSKAP; NATURAL SCIENCES; formal verification; higher-order logic; interactive theorem provers;

    Sammanfattning : This thesis is about mechanically establishing the correctness of computer programs. In particular, we are interested in establishing the correctness of tools used in computer-aided mathematics. We build on tools for proof-producing program synthesis, and verified compilation, and a verified theorem proving kernel. LÄS MER

  5. 4. Verified proof checking for higher-order logic

    Författare :Oskar Abrahamsson; Chalmers tekniska högskola; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES;

    Sammanfattning : This thesis is about verified computer-aided checking of mathematical proofs. We build on tools for proof-producing program synthesis, and verified compilation, and a verified theorem proving kernel. Using these tools, we have produced a mechanized proof checker for higher-order logic that is verified to only accept valid proofs. LÄS MER

  7. 5. Random Structured Test Data Generation for Black-Box Testing

    Författare :Michal Palka; Chalmers tekniska högskola; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES;

    Sammanfattning : We show how automated random testing can be used to effectively find bugs in complex software, such as an optimising compiler. To test the GHC Haskell compiler we created a generator of simple random programs, used GHC to compile them with different optimisation levels, and thencompared the results of running them. LÄS MER