Programming-Testing-Proving
- Domaine
- Programming-Testing-Proving
- Domain - extra
- Random-based test Generation
- Année
- 2011
- Starting
- 1.10.2011
- État
- Open
- Sujet
- Random-Based Methods for Test- Case-Generation of C Programs
- Thesis advisor
- WOLFF Burkhart
- Co-advisors
- Frederic Voisin (LRI)
Marie-Claude Gaudel (LRI)
- Laboratory
- Collaborations
- CEA (Frama C)
- Abstract
- In this Phd, the goal is to explore static testing methods for a realistic subset of C, i.e. test-data are generated according certain criteria and techniques and run against „the real code“. A particular emphasis in this Phd is put on testing data- invariants of pointer structures, but also classical control-flow based test- case coverage criteria are considered, which were represented both by an LTL like assertion language. Such assertions can be compiled to graphs; instead of exploring them exhaustively, uniform random selection methods were applied to statically
generate constraints for object graphs and control-flow-graphs (path- conditions) as well. By finding effective means to approximate feasible paths (by invariant generation, abstract interpretation as well as code-slicing techniques), the effectivity of the overall method should be improved. - Context
- The programming language C is widely used for operating system level code which is both complex
(due to the need for efficiency and the proximity to hardware) and safety critical. Building environments to verify C code has therefore attracted the interest of many research groups, leading to environments such as Frama-C or Visualstudio/VCC.
Besides classical proof-based code analysis methods, there is the possibility to generate tests along control-flow graphs for programs. In the ForTesSE-group, a prototype called Auguste has been developed generates tests for a small fragment of C based on Johan Oudinets Rukia system that generates uniformly distributed random samples for such graphs. - Objectives
- The practical part of this Phd consists in - Integrating pre-existing AUGUSTE/RUKIA into Frama-C
- Developing an assertion language for data-structure consistency based on LTL and the pre-existing ADCL2 (Frama C Jessie Plugin)
- implementing new invariant- construction, abstract interpretation and other techniques (such as Dekkers Algorithm) in order to perform code-slicing before control- flow-graph construction.
- careful statistic exploration of larger program samples. - Work program
- The practical part of this Phd consists in - Integrating pre-existing AUGUSTE/RUKIA into Frama-C
- Developing an assertion language for data-structure consistency based on LTL and the pre-existing ADCL2 (Frama C Jessie Plugin)
- implementing new invariant- construction, abstract interpretation and other techniques (such as Dekkers Algorithm) in order to perform code-slicing before control- flow-graph construction.
- careful statistic exploration of larger program samples. - Extra information
- 1.Sascha Böhme, Michal Moskal, Wolfram Schulte, Burkhart Wolff: HOL- Boogie - An Interactive Prover- Backend for the Verifying C Compiler. J. Autom. Reasoning 44(1-2): 111-144 (2010) 2.G. J. Holzmann. The SPIN Model Checker : Primer and Reference Manual. Addison-Wesley Professional, September 2003. 3.D. Peled. Model checking and testing combined. In ICALP, pages 47–63, 2003 4.The Rukia Home Page: http://www.lri.fr/~oudinet/en/project.html
- Prerequisite
- - Knowledge or interest in functional programming
in OCaml
- Knowledge over elementary logic and program analysis
- Knowledge over Frama-C desirable. - Détails
Random-based Test-Case Generation for C (RTGC).pdf- Expected funding
- Institutional funding
- Status of funding
- Expected
- Candidates
- ROMAIN AISSAT
- Utilisateur
- burkhart.wolff
- Créé
- Jeudi 19 avril 2012 17:21:51 CEST
- dernière modif.
- Mardi 15 mai 2012 14:47:28 CEST
Connexion
Ecole Doctorale Informatique Paris-Sud
Directrice
Nicole Bidoit
Assistante
Stéphanie Druetta
Conseiller aux thèses
Dominique Gouyou-Beauchamps
ED 427 - Université Paris-Sud
UFR Sciences Orsay
Bat 650 - aile nord - 417
Tel : 01 69 15 63 19
Fax : 01 69 15 63 87
courriel: ed-info à lri.fr