Ανάλυση προγραμμάτων μέσω συμβολικής εκτέλεσής τους
Creators: name: Καραϊσκος, Ζαφείριος Κ.
Publisher: name: Aristotle University of Thessaloniki
Year: 2004
Subjects: Ανάλυση προγράμματος
Συμβολική εκτέλεση
Συλλογή ιδιοτήτων
Δηλωτική σημασιολογία
Σημασία συνέχειας
Αριθμητική διαστημάτων
Program analysis
Symbolic execution
Attribute collection
Demotational semantics
Continuation semantics
Internal arithmetic

description: Στο πεδίο ανάλυσης προγραμμάτων, οι περισσότερες μέθοδοι εφαρμόζονται στη βελτιστοποίηση των μεταγλωττιστών. Πιστεύουμε ότι υπάρχει αρκετή θεωρία, η οπόία θα μπορούσε να υποστηρίξει την εφαρμογή των μεθόδων ανάλυσης προγραμμάτων στην ανάπτυξη λογισμικού. Ενθετα και ασφάλειας-κρίσιμα συστήματα, όπως επίσης, και η ανάπτυξη πολύ μεγάλων και πολύπλοκων εφαρμογών, απαιτούν πιο περίτεχνα εργαλεία για τη σχεδίαση, ανάπτυξη, έλεγχο και συντήρηση λογισμικού. Η συμβολική εκτέλεση είναι μια μέθοδος, η οποία χρησιμοποιείται για την ανασυγκρότηση της λογικής και των υπολογισμών κατά μήκος μιας διαδρομής προγράμματος, εκτελώντας τη διαδρομή με συμβολικές τιμές παρά με πραγματικές τιμές για τις μεταβλητές εισόδου. Τα αποτελέσματα, από την εφαρμογή της μεθόδου, είναι οι συμβολικές παραστάσεις των μεταβλητών του προγράμματος, ως προς τις συμβολικές τιμές των μεταβλητών εισόδου και η συνθήκη-διαδρομής για κάθε διαδρομή που εξετάζεται. Η συμβολική εκτέλεση είναι μια εκ των συνιστωσών ενός εργαλείου, το οποίο υλοποιεί ένα είδος ανάλυσης προγραμμάτων που ονομάζεται συμβολική ανάλυση. Η συμβολική ανάλυση περιλαμβάνει τη μετατροπή ενός πηγαίου προγράμματος χρησιμοποιώντας την ενδιάμεση αναπαράσταση, στον προσδιορισμό της εφικτότητας εκτέλεσης των διαδρομών, στο στατικό έλεγχο σφαλμάτων και σε άλλου είδους επεξεργασία. Ολες οι φάσεις της συμβολικής ανάλυσης βασίστηκαν σε αυστηρές μαθηματικές τεχνικές. Κανονικές εκφράσεις στη λεξική ανάλυση, BNF-κανόνες στη συντακτική ανάλυση, συλλογή-ιδιοτήτων στη στατική-σημασιολογική ανάλυση, δημιουργία της αφαιρετικής σύνταξης με ομορφισμό αλγεβρών και συμβολική εκτέλεση κατευθυνόμενη από τη δηλωτική σημασιολογία
description: Most program analysis methods have been applied to optimising compilers. It is our belief that there is enough theory that could support the application of program analysis methods to software construction. Embedded and safety-critical systems but also large and complex software demand sophisticated tools for design, development, testing and maintenance of software. Symbolic execution is a method used to reconstruct logic and computations along a program path by executing the path with symbolic, rather than actual values of data. The results obtained by symbolic execution are the symbolic formulae, representing the values of the program variables, and the path condition for each path examined. Symbolic execution is a component of a tool which implements a kind of program analysis called symbolic analysis. Symbolic analysis comprises the transformation of a source program to an intemediate representation, the symbolic execution of the program using the intermediate representation, the determination of the feasibility of execution paths, the static error checking and other kinds of processing. All stages of symbolic analysis have been on formal techniques. Regular expressions have been used in lexical analysis, BNF-rules in syntax analysis, attribute-collection in static-semantic analysis, algebra's homomorphism for the creation of the abstract syntax and semantics-directed symbolic execution