Please use this identifier to cite or link to this item:
http://artemis.cslab.ece.ntua.gr:8080/jspui/handle/123456789/13625
Title: | Δυναμικός Συμβολικός Έλεγχος Με Χρήση Πολλαπλών Smt Επιλυτών |
Authors: | Κωνσταντίνος Ρακτιβάν Σαγώνας Κωστής |
Keywords: | έλεγχος δυναμικός συμβολικός έλεγχος smt επιλυτές smtlib cuter |
Issue Date: | 6-Nov-2017 |
Abstract: | Ο concolic έλεγχος είναι μία πολλά υποσχόμενη τεχνική για τον έλεγχο προγραμμάτων. Λαμβάνει υπόψη τόσο συμβολικές (symbolic) όσο και σταθερές (concrete) τιμές των μεταβλητών, μεγιστοποιώντας το πλήθος των μονοπατιών εκτέλεσης (execution paths) που καταφέρνει εξετάσει. Χρησιμοποιούμε έναν SMT επιλυτή για να υπολογίσουμε τιμές των παραμέτρων εισόδου που οδηγούν την εκτέλεση του ελεγχόμενου κώδικα σε επιλεγμένο μονοπάτι. Αντικείμενο της παρούσας εργασίας είναι η δημιουργία ενός πλαισίου που επιτρέπει την αξιοποίηση πολλαπλών επιλυτών για τον έλεγχο ενός προγράμματος, επικοινωνώντας με αυτούς μέσω της γλώσσας SMTLIB. Επίσης, αναφέρουμε τα προβλήματα που προκύπτουν κατά την προσθήκη των επιλυτών, τον τρόπο αντιμετώπισής τους και τελικά αναδεικνύουμε τα πλεονεκτήματα της συγκεκριμένης προσέγγισης. Η εργασία αναπτύχθηκε στο εργαλείο CutEr, το οποίο εφαρμόζει concolic testing σε προγράμματα γραμμένα σε γλώσσα Erlang. Η υλοποίησή της παρέχει τη δυνατότητα στο εργαλείο να ελέγχει επιτυχημένα ένα ευρύτερο σύνολο προγραμμάτων, το οποίο δε μπορούσε να διαχειριστεί προηγουμένως. |
URI: | http://artemis-new.cslab.ece.ntua.gr:8080/jspui/handle/123456789/13625 |
Appears in Collections: | Διπλωματικές Εργασίες - Theses |
Files in This Item:
File | Size | Format | |
---|---|---|---|
DT2017-0285.pdf | 1.14 MB | Adobe PDF | View/Open |
Items in Artemis are protected by copyright, with all rights reserved, unless otherwise indicated.