Sökning: "Jesper Amilon"
Hittade 2 uppsatser innehållade orden Jesper Amilon.
1. Automated inference of ACSL function contracts using TriCera
Master-uppsats, KTH/Skolan för elektroteknik och datavetenskap (EECS)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
2. Verifying Temporal Properties Using Deductive Verifiers
Kandidat-uppsats, KTH/Skolan för elektroteknik och datavetenskap (EECS)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