Automated inference of ACSL function contracts using TriCera

Automated inference of ACSL function contracts using TriCera

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 state...

Full description

Bibliographic Details
Main Author: Amilon, Jesper
Format: Others
Language:English
Published: KTH, Skolan för elektroteknik och datavetenskap (EECS) 2021
Subjects:
Formal Verification
Contract inference
Hoare Logic
Model Checking
Horn clauses
Formell verifikation
Kontraktgenerering
Formell semantik
Hoare logik
Modellprovning
Computer Sciences
Datavetenskap (datalogi)
Online Access:http://urn.kb.se/resolve?urn=urn:nbn:se:kth:diva-303867

Internet

http://urn.kb.se/resolve?urn=urn:nbn:se:kth:diva-303867

Similar Items