Program logics

Researchers

Ph.D. Students

Alumni

Mika Cohen, Ph.D. June 2007

Short Description

Program logics use various forms of logic to specify interesting and useful properties of computer systems and software, and to prove or disprove these properties, either algorithmically, or by some form of machine-assisted, but essentially manual, proof search. Model checking, for instance, concerns the problem of checking a logical specification on a model of some concrete piece of hardware or software. Many varieties of logic, some quite exotic, have found use in this branch of computer science:

Modal and temporal logics typically express time- and choice-dependent properties. An example temporal property of a scheduler may be that it cannot forever deny service to a client that continually requests it.
Logics of knowledge and belief are often used to express properties of distributed systems. For instance the purpose of a distributed agreement protocol might be to establish common knowledge among the processes in a system of some agreed-upon value.
Linear, relevant, and other substructural logics may be used to compose and decompose properties according to the structure of an underlying model. As an example a model may be composed of a number of threads executing in parallel, and it is of interest to find ways in which a property of such a model can be reduced to properties of the individual threads.

The main research questions are:

Expressiveness: Does the logic express an interesting/useful class of properties? Can we quantify this statement? An example is Hennessy and Milner's now classical characterization of bisimulation equivalence, an equivalence of behavioral identity among communicating processes, in terms of labelled modal logic.
Proof systems: Proof systems should certainly be sound such that only valid statements can be derived. But, it is also interesting to ask if it is complete in the sense that all valid statements can be derived, or, if this is impossible, complete relative to some other formal system.
Decision procedures: An important task is to chip off logical verification problems that can be solved, fully or partially, by machine. Most interesting cases, as we know from undecidability of the halting problem, cannot in fact be solved algorithmically, and so one key problem is to come up with abstraction techniques that allow hard problems to be approximated by less hard ones.

Epistemic logics and cryptography

Epistemic logic is the logic of knowledge. Cryptographic communication is about the establishment or prevention of knowledge in the presence of attackers, and a typical goal of a cryptographic protocol is to establish common knowledge of some secret not known to a potential intruder. The use of epistemic logic in this area has, however, run into the problem that there is a mismatch between the logical interpretation of knowledge, and the use of cryptography for information hiding. Our main achievement has been to propose a new type of model that overcomes this mismatch and to examine its implications in terms of expressiveness and axiomatizations.

Modal and first-order mu-calculus

In the context of the Verification of Control-Flow Properties of Programs with Procedures (CVPP) project the modal mu-calculus is used to specify control-flow temporal properties of programs. These specifications are used by the framework for modular verification.

Projects and Funding

TBD

Publications

A Completeness result for BAN logic: M. Cohen, M. Dam; In Journal of Logic, Language, and Information
A Complete Axiomatization of Knowledge and Cryptography: M. Cohen, M. Dam; Proc. LICS'07, pp. 77-86
Logical Omniscience in the Semantics of BAN Logics: M. Cohen, M. Dam; Proc. FCS'05, Chicago, 2005, pp. 121-132.
A Completeness result for BAN logic: M. Cohen, M. Dam; Proc. Methods for Modalities 4, Berlin, Dec. 2005
On the Structure of Inductive Reasoning: Circular and Tree-shaped Proofs in the mu-Calculus: C. Sprenger, M. Dam; In Proc. FOSSACS’03, Warsaw, Poland, LNCS vol. 2620, pp. 425-440.
A note on global induction mechanisms in a µ-calculus with explicit approximations: C. Sprenger, M. Dam; Theoretical Informatics and Applications 37 (2003) pp. 365-399.
Proof Systems for Pi-Calculus Logics: M. Dam; In R. de Queiroz (ed.), "Logic for Concurrency and Synchronisation", Trends in Logic, Logica Library, Kluwer, 2003, pp. 145--212.
M. Dam and D. Gurov: Mu-Calculus with Explicit Points and Approximations: M. Dam, D. Gurov; Journal of Logic and Computation, vol. 12, issue 2, April 2002, pp. 255-269.
A note on global induction in a mu-calculus with explicit approximations: C. Sprenger and M. Dam; Proc. FICS 2002: pp. 22-24, 2002
Mu-Calculus with Explicit Points and Approximations (Abstract).: M. Dam, D. Gurov; In Proc. FICS'00, 2000
Compositional Verification of CCS Processes: M. Dam, D. Gurov; Proc. PSI'99, LNCS vol. 1755, pp. 247-256, 1999
Proving Properties of Dynamic Process Networks: M. Dam; Information and Computation 140, 1998, pp. 95-114.
Model Checking Mobile Processes: M. Dam; Information and Computation 129(1), 1996, pp. 35-51
Toward a Modal Theory of Types for the pi-Calculus: R. Amadio, M. Dam; Proc. FTRTFT'96, Springer Lecture Notes in Computer Science.
Reasoning about Higher-Order Processes: R. Amadio, M. Dam; Proc. CAAP'95, pp. 202-217.
M. Dam. CTL* and ECTL* as Fragments of the Modal mu-Calculus.: M. Dam; Theoretical Computer Science 126 (1994) pp. 77-96.
Temporal Logics, Automata, and Classical Theories - An Introduction.: M. Dam; Lecture Notes for the 6th European Summer School on Logic, Language and Information, 1994.
Fixed Points of Buchi Automata.: M. Dam; In Proceedings of 12th Conference on Foundations of Software Technology and Theoretical Computer Science, Lecture Notes in Computer Science 652 (1992) pp. 39-50.
R-Generability, and Definability in Branching Time Logics: M. Dam; Information Processing Letters 41 (1992) pp. 281-287.