Essays about: "ACSL"
Found 3 essays containing the word ACSL.
-
1. Automated Inference of ACSL Contracts for Programs with Heaps
University essay from KTH/Skolan för elektroteknik och datavetenskap (EECS)Abstract : Contract inference consists in automatically computing contracts that formally describe the behaviour of program functions. Contracts are used in deductive verification, which is a method for verifying whether a system behaves according to a provided specification. The Saida plugin in Frama-C is a contract inference tool for C code. READ MORE
-
2. Automated inference of ACSL function contracts using TriCera
University essay from KTH/Skolan för elektroteknik och datavetenskap (EECS)Abstract : 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. READ MORE
-
3. Automatic Verification of Embedded Systems Using Horn Clause Solvers
University essay from Uppsala universitet/Institutionen för informationsteknologiAbstract : Recently, an increase in the use of safety-critical embedded systems in the automotive industry has led to a drastic up-tick in vehicle software and code complexity. Failure in safety-critical applications can cost lives and money. READ MORE