Paper Info
Title
Synthesis Of Parametric Programs Using Genetic Programming And Model Checking
Abstract
Formal methods apply algorithms based on mathematical principles to enhance the reliability of systems. It would only be natural to try to progress from verification, model checking or testing a system against its formal specification into constructing it automatically. Classical algorithmic synthesis theory provides interesting algorithms but also alarming high complexity and undecidability results. The use of genetic programming, in combination of model checking and testing, provides a powerful heuristic to synthesize programs. The method is not completely automatic, as it is fine tuned by a user that sets up the specification and parameters. It also does not guarantee to always succeed and converge towards a solution that satisfies all the required properties. However, we applied it successfully on quite nontrivial examples and managed to find solutions to hard programming challenges, as well as to improve and to correct code. We describe here several versions of our method for synthesizing sequential and concurrent systems.
Year
DOI
Venue
2014
10.4204/EPTCS.140.5
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE
Field
DocType
Issue
Discrete mathematics,Heuristic,Model checking,Programming language,Computer science,Information technology,Formal specification,Genetic programming,Theoretical computer science,Parametric statistics,Formal methods
Journal
140
ISSN
Citations 
PageRank 
2075-2180
2
0.39
References 
Authors
20
2
Name
Order
Citations
PageRank
Gal Katz11346.80
Doron Peled23357273.18