Δυναμικός Συμβολικός Έλεγχος Με Χρήση Πολλαπλών Smt Επιλυτών

Abstract

Ο concolic έλεγχος είναι μία πολλά υποσχόμενη τεχνική για τον έλεγχο προγραμμάτων. Λαμβάνει υπόψη τόσο συμβολικές (symbolic) όσο και σταθερές (concrete) τιμές των μεταβλητών, μεγιστοποιώντας το πλήθος των μονοπατιών εκτέλεσης (execution paths) που καταφέρνει εξετάσει. Χρησιμοποιούμε έναν SMT επιλυτή για να υπολογίσουμε τιμές των παραμέτρων εισόδου που οδηγούν την εκτέλεση του ελεγχόμενου κώδικα σε επιλεγμένο μονοπάτι. Αντικείμενο της παρούσας εργασίας είναι η δημιουργία ενός πλαισίου που επιτρέπει την αξιοποίηση πολλαπλών επιλυτών για τον έλεγχο ενός προγράμματος, επικοινωνώντας με αυτούς μέσω της γλώσσας SMTLIB. Επίσης, αναφέρουμε τα προβλήματα που προκύπτουν κατά την προσθήκη των επιλυτών, τον τρόπο αντιμετώπισής τους και τελικά αναδεικνύουμε τα πλεονεκτήματα της συγκεκριμένης προσέγγισης. Η εργασία αναπτύχθηκε στο εργαλείο CutEr, το οποίο εφαρμόζει concolic testing σε προγράμματα γραμμένα σε γλώσσα Erlang. Η υλοποίησή της παρέχει τη δυνατότητα στο εργαλείο να ελέγχει επιτυχημένα ένα ευρύτερο σύνολο προγραμμάτων, το οποίο δε μπορούσε να διαχειριστεί προηγουμένως.