Παρακαλώ χρησιμοποιήστε αυτό το αναγνωριστικό για να παραπέμψετε ή να δημιουργήσετε σύνδεσμο προς αυτό το τεκμήριο:
http://artemis.cslab.ece.ntua.gr:8080/jspui/handle/123456789/13625
Τίτλος: | Δυναμικός Συμβολικός Έλεγχος Με Χρήση Πολλαπλών Smt Επιλυτών |
Συγγραφείς: | Κωνσταντίνος Ρακτιβάν Σαγώνας Κωστής |
Λέξεις κλειδιά: | έλεγχος δυναμικός συμβολικός έλεγχος smt επιλυτές smtlib cuter |
Ημερομηνία έκδοσης: | 6-Νοε-2017 |
Περίληψη: | Ο concolic έλεγχος είναι μία πολλά υποσχόμενη τεχνική για τον έλεγχο προγραμμάτων. Λαμβάνει υπόψη τόσο συμβολικές (symbolic) όσο και σταθερές (concrete) τιμές των μεταβλητών, μεγιστοποιώντας το πλήθος των μονοπατιών εκτέλεσης (execution paths) που καταφέρνει εξετάσει. Χρησιμοποιούμε έναν SMT επιλυτή για να υπολογίσουμε τιμές των παραμέτρων εισόδου που οδηγούν την εκτέλεση του ελεγχόμενου κώδικα σε επιλεγμένο μονοπάτι. Αντικείμενο της παρούσας εργασίας είναι η δημιουργία ενός πλαισίου που επιτρέπει την αξιοποίηση πολλαπλών επιλυτών για τον έλεγχο ενός προγράμματος, επικοινωνώντας με αυτούς μέσω της γλώσσας SMTLIB. Επίσης, αναφέρουμε τα προβλήματα που προκύπτουν κατά την προσθήκη των επιλυτών, τον τρόπο αντιμετώπισής τους και τελικά αναδεικνύουμε τα πλεονεκτήματα της συγκεκριμένης προσέγγισης. Η εργασία αναπτύχθηκε στο εργαλείο CutEr, το οποίο εφαρμόζει concolic testing σε προγράμματα γραμμένα σε γλώσσα Erlang. Η υλοποίησή της παρέχει τη δυνατότητα στο εργαλείο να ελέγχει επιτυχημένα ένα ευρύτερο σύνολο προγραμμάτων, το οποίο δε μπορούσε να διαχειριστεί προηγουμένως. |
URI: | http://artemis-new.cslab.ece.ntua.gr:8080/jspui/handle/123456789/13625 |
Εμφανίζεται στις συλλογές: | Διπλωματικές Εργασίες - Theses |
Αρχεία σε αυτό το τεκμήριο:
Αρχείο | Μέγεθος | Μορφότυπος | |
---|---|---|---|
DT2017-0285.pdf | 1.14 MB | Adobe PDF | Εμφάνιση/Άνοιγμα |
Όλα τα τεκμήρια του δικτυακού τόπου προστατεύονται από πνευματικά δικαιώματα.