FALL 2006
CSc 85200.
Seminar in Computational Logic
Code: 94282
Tuesday, 2pm – 4pm, room 3305 (Graduate Center)
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.