September 19 meeting
Speaker:
Sergei Artemov (Graduate Center CUNY)
Topic:
Gettier examples revisited: toward a formal analysis of justification
In this talk we try to apply the emerging formal theory of justification (Logic of Proofs, Fitting epistemic semantics, Justification Logic)
to the studies of justification initiated by Gettier's well-known paper of 1963. Rather than advocating any specific solution to Gettier
Problem, we try to show that there are formal logical methods available for analyzing epistemic justification.
A brief introduction to Justification Logic will be offered.
September 12 meeting
Speaker:
Greta Yorsh (Tel Aviv University)
Topic:
A Logic of Reachable Patterns in Linked Data-Structures
Greta Yorsh, Alexander Rabinovich, Mooly Sagiv, Antoine Meyer, Ahmed Bouajjani
To appear in
Proc. Foundations of Software Science and Computation Structures, 2006
(
FOSSACS 2006)
We define a new decidable logic for expressing and checking invariants of programs that manipulate
dynamically-allocated objects via pointers and destructive pointer updates. The main feature of this
logic is the ability to limit the neighborhood of a node that is reachable via a regular expression
from a designated node. The logic is closed under boolean operations (entailment, negation) and has
a finite model property. The key technical result is the proof of decidability. We show how to
express precondition, postconditions, and loop invariants for some interesting programs. It is also
possible to express properties such as disjointness of data-structures, and low-level heap mutations.
Moreover, our logic can express properties of arbitrary data-structures and of an arbitrary number
of pointer fields. The latter provides a way to naturally specify postconditions that relate the
fields on entry to a procedure to the fields on exit. Therefore, it is possible to use the logic
to automatically prove partial correctness of programs performing low-level heap mutations.
Click here to access the full version of the paper (including proofs):
PostScript;
PDF
September 5 meeting
This will be a town meeting. All the participants are invited to tell
about research progress made during the summer. Newcomers are expected
to say a few worlds about their areas of interest. We will sketch a
seminar program for a semester.
