DocumentCode :
3030208
Title :
A memetic algorithm for program verification
Author :
Aleb, Nassima ; Tamen, Zahia
Author_Institution :
Comput. Sci. Dept., USTHB, Algiers, Algeria
fYear :
2011
fDate :
16-18 Nov. 2011
Firstpage :
30
Lastpage :
35
Abstract :
We present a memetic algorithm for program safety properties verification. This problem is expressed by means of Reach ability of some erroneous location L in the program. We use a new method for program modeling: A Separation Modeling Approach: ASMA, in which programs are represented by two components: Data Model DM, and Control Model CM. The erroneous location is represented by its "Location Access Chain", LAC: a string where each position represents the required value of CM elements guards to reach L. The memetic algorithm generates each time a new population attempting to provide an execution which is " conform" to the location access chain. An individual of the population is a set of intervals each one representing an input variable. At each generation, two local search operators are used to improve some chosen solutions.
Keywords :
program verification; a separation modeling approach; control model; data model; location access chain; memetic algorithm; program modeling; program safety properties verification; Analytical models; Computational modeling; Data models; Delta modulation; Input variables; Memetics; Silicon; memetic algorithms; program modeling; program verification; reachability analysis;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Computer Modeling and Simulation (EMS), 2011 Fifth UKSim European Symposium on
Conference_Location :
Madrid
Print_ISBN :
978-1-4673-0060-5
Type :
conf
DOI :
10.1109/EMS.2011.92
Filename :
6131212
Link To Document :
بازگشت