Η Haskell ως εργαλείο τυπικής επαλήθευσης με LiquidHaskell
Περίληψη
Οι ελλείψεις στον κώδικα και τα σφάλματα αποτελούν αναπόφευκτο μέρος των λογισμικών συστημάτων. Σε συστήματα κρίσιμα για την ασφάλεια, όπως αυτά των αεροσκαφών ή του ιατρικού εξοπλισμού, ακόμα και ένα μόνο σφάλμα μπορεί να οδηγήσει σε καταστροφικές συνέπειες, όπως τραυματισμούς ή θάνατο. Η τυπική επαλήθευση μπορεί να χρησιμοποιηθεί για τον στατικό εντοπισμό ελλείψεων στον κώδικα, αποδεικνύοντας ή διαψεύδοντας ιδιότητες ορθότητας ενός συστήματος. Ωστόσο, στην παρούσα της μορφή, η τυπική επαλήθευση είναι μια περίπλοκη διαδικασία που σπάνια χρησιμοποιείται από προγραμματιστές του ευρύτερου χώρου, κυρίως επειδή αφορά γλώσσες που δεν είναι γενικού σκοπού (π.χ. Coq, Agda, Dafny). Παρουσιάζουμε το LIQUID HASKELL, έναν πρακτικό επαληθευτή προγραμμάτων που στοχεύει στην καθιέρωση της τυπικής επαλήθευσης ως αναπόσπαστο μέρος της διαδικασίας ανάπτυξης λογισμικού. Το LIQUID HASKELL ενσωματώνει φυσικά τον καθορισμό ιδιοτήτων ορθότητας ως λογικές εξειδικεύσεις στους τύπους της Haskell. Επιπλέον, χρη ...
περισσότερα
Περίληψη σε άλλη γλώσσα
Code deficiencies and bugs constitute an unavoidable part of software systems. In safety critical systems, like aircrafts or medical equipment, even a single bug can lead to catastrophic impacts such as injuries or death. Formal verification can be used to statically track code deficiencies by proving or disproving correctness properties of a system. However, at its current state formal verification is a cumbersome process that is rarely used by mainstream developers, mostly because it targets non general purpose languages (e.g., Coq, Agda, Dafny).We present LIQUID HASKELL, a usable program verifier that aims to establish formal verification as an integral part of the development process. LIQUID HASKELL naturally integrates the specification of correctness properties as logical refinements of Haskell’s types. Moreover, it uses the abstract interpretation framework of liquid types to automatically check correctness of specifications via Satisfiability Modulo Theories (SMT) solvers requi ...
περισσότερα
![]() | |
![]() | Κατεβάστε τη διατριβή σε μορφή PDF (1.04 MB)
(Η υπηρεσία είναι διαθέσιμη μετά από δωρεάν εγγραφή)
|
Όλα τα τεκμήρια στο ΕΑΔΔ προστατεύονται από πνευματικά δικαιώματα.
|
Στατιστικά χρήσης

ΠΡΟΒΟΛΕΣ
Αφορά στις μοναδικές επισκέψεις της διδακτορικής διατριβής για την χρονική περίοδο 07/2018 - 07/2023.
Πηγή: Google Analytics.
Πηγή: Google Analytics.

ΞΕΦΥΛΛΙΣΜΑΤΑ
Αφορά στο άνοιγμα του online αναγνώστη για την χρονική περίοδο 07/2018 - 07/2023.
Πηγή: Google Analytics.
Πηγή: Google Analytics.

ΜΕΤΑΦΟΡΤΩΣΕΙΣ
Αφορά στο σύνολο των μεταφορτώσων του αρχείου της διδακτορικής διατριβής.
Πηγή: Εθνικό Αρχείο Διδακτορικών Διατριβών.
Πηγή: Εθνικό Αρχείο Διδακτορικών Διατριβών.

ΧΡΗΣΤΕΣ
Αφορά στους συνδεδεμένους στο σύστημα χρήστες οι οποίοι έχουν αλληλεπιδράσει με τη διδακτορική διατριβή. Ως επί το πλείστον, αφορά τις μεταφορτώσεις.
Πηγή: Εθνικό Αρχείο Διδακτορικών Διατριβών.
Πηγή: Εθνικό Αρχείο Διδακτορικών Διατριβών.