Unit:
Κατεύθυνση / ειδίκευση Υπολογιστικά Συστήματα: Λογισμικό και Υλικό (ΣΥΣ)Πληροφορική
Supervisors info:
Σμαραγδάκης Γιάννης, Καθηγητής, Πληροφορικής και Τηλεπικοινωνιών, Εθνικό και Καποδιστριακό Πανεπιστήμιο Αθηνών
Original Title:
Datalog Based Symbolic Program Reasoning for Java
Translated title:
Datalog Based Symbolic Program Reasoning for Java
Summary:
Motivated by the success of theorem provers as aiding tools in symbolic execution and the
convenience that declarative programming languages provide, in this thesis we attempt
to introduce a strictly declarative implementation of a theorem prover in Datalog. Our
approach, namely static declarative symbolic reasoning is implemented within the Doop
framework for Java Pointer Analysis, and it mainly seeks to answer ”Which expressions
are implied by another expression within a program”. The main motivation behind that
decision was to leverage Doop’s powerful infrastructure, and at the same time make it
possible for Doop to utilize the reasoner in the future for any of its analyses.
Main subject category:
Technology - Computer science
Keywords:
flow-sensitivity, path-sensitivity, inference rules and logic proofs
