The Automation of C Program Verification by Symbolic Method of Loop Invariants Elimination
During deductive verification of programs written in imperative languages, the generation and proof of verification conditions corresponding to loops can cause difficulties, because each one must be provided with an invariant whose construction is often a challenge. As a rule, the methods of invaria...
Kaydedildi:
| Asıl Yazarlar: | , , |
|---|---|
| Materyal Türü: | Artigo |
| Dil: | Inglês |
| Baskı/Yayın Bilgisi: |
Yaroslavl State University
2018-10-01
|
| Seri Bilgileri: | Моделирование и анализ информационных систем |
| Konular: | |
| Online Erişim: | https://www.mais-journal.ru/jour/article/view/745 |
| Etiketler: |
Etiket eklenmemiş, İlk siz ekleyin!
|