Sökning: "Hoare Logic"

Hittade 5 uppsatser innehållade orden Hoare Logic.

1. 1. Automated inference of ACSL function contracts using TriCera

   Master-uppsats, KTH/Skolan för elektroteknik och datavetenskap (EECS)

   Författare :Jesper Amilon; [2021]
   Nyckelord :Formal Verification; Contract inference; Hoare Logic; Model Checking; Horn clauses; Formell verifikation; Kontraktgenerering; Formell semantik; Hoare logik; Modellprovning; Horn clauses;

   Sammanfattning : This thesis explores synergies between deductive verification and model checking, by using the existing model checker TriCera to automatically infer specifications for the deductive verifier Frama-C. To accomplish this, a formal semantics is defined for a subset of ANSI C, extended with assume statements, called Csmall. LÄS MER

3. 2. Extracting scalable program models for TLA model checking

   Kandidat-uppsats, KTH/Skolan för elektroteknik och datavetenskap (EECS)

   Författare :Anders Ågren Thuné; Theo Puranen Åhfeldt; [2020]
   Nyckelord :;

   Sammanfattning : Program verification has long been of interest to researchers and practitioners for its role in asserting reliability in critical systems. Many such systems feature reactive behavior, where temporal properties are of interest. Consequently, a number of systems and program verification tools for dealing with temporal logic have been developed. LÄS MER

4. 3. A contract language for modular specification and verification of temporal properties

   Master-uppsats, KTH/Skolan för elektroteknik och datavetenskap (EECS)

   Författare :Lars Hummelgren; [2020]
   Nyckelord :;

   Sammanfattning : Deductive software verification is used to prove correctness of programs with respect to contracts. Contracts are commonly expressed on procedures of a program using Hoare logic. LÄS MER

5. 4. Verifying Temporal Properties Using Deductive Verifiers

   Kandidat-uppsats, KTH/Skolan för elektroteknik och datavetenskap (EECS)

   Författare :Jesper Amilon; Axel Lindeberg; [2019]
   Nyckelord :;

   Sammanfattning : Formal verification is an area of theoretical computer science where mathematical logic is used to prove that a program behaves in a certain way. With the methods in formal verification, you can prove that the program follows some given specification and thereby behaves in the desired way. The area is largely split up into two distinct parts. LÄS MER

7. 5. Provably Sound and Secure Automatic Proving and Generation of Verification Conditions

   Master-uppsats, KTH/Teoretisk datalogi, TCS

   Författare :Didrik Lundberg; [2018]
   Nyckelord :HOL4; HOL; Higher-order logic; SML; Poly ML; Formal methods; Axiomatic semantics; Formal verification; Static verification; Program verification; Hoare logic; Floyd-Hoare logic; ITP; Interactive theorem prover; Theorem prover; Proof assistant; BIR; Automated theorem proving; ATP; Automated deduction; Computer-assisted proof; Automated reasoning;

   Sammanfattning : Formal verification of programs can be done with the aid of an interactive theorem prover. The program to be verified is represented in an intermediate language representation inside the interactive theorem prover, after which statements and their proofs can be constructed. This is a process that can be automated to a high degree. LÄS MER