Academic Journal
Correct Code Containing Containers
| العنوان: | Correct Code Containing Containers |
|---|---|
| المؤلفون: | Claire Dross, Jean-christophe Filliâtre, Yannick Moy |
| المساهمون: | The Pennsylvania State University CiteSeerX Archives |
| المصدر: | http://proval.lri.fr/publications/dross11tap.pdf. |
| سنة النشر: | 2011 |
| المجموعة: | CiteSeerX |
| مصطلحات موضوعية: | containers, iterators, verification by contracts, annotations, axiomatization, API usage verification, SMT |
| الوصف: | For critical software development, containers such as lists, vectors, sets or maps are an attractive alternative to ad-hoc data structures based on pointers. As standards like DO-178C put formal verification and testing on an equal footing, it is important to give users the ability to apply both to the verification of code using containers. In this paper, we present a definition of containers whose aim is to facilitate their use in certified software, using modern proof technology and novel specification languages. Correct usage of containers and user-provided correctness properties can be checked either by execution during testing or by formal proof with an automatic prover. We present a formal semantics for containers and an axiomatization of this semantics targeted at automatic provers. We have proved in Coq that the formal semantics is consistent and that the axiomatization thereof is correct. |
| نوع الوثيقة: | text |
| وصف الملف: | application/pdf |
| اللغة: | English |
| Relation: | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.384.2650; http://proval.lri.fr/publications/dross11tap.pdf |
| الاتاحة: | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.384.2650 http://proval.lri.fr/publications/dross11tap.pdf |
| Rights: | Metadata may be used without restrictions as long as the oai identifier remains attached to it. |
| رقم الانضمام: | edsbas.5A46A308 |
| قاعدة البيانات: | BASE |
| الوصف غير متاح. |