LICS on Monday

Detailed program
Monday July 22nd, 2002
See also the unified by-slot program

Sessions take place in auditorium 1 unless otherwise indicated.

FLoC opening

Joint with FME, RTA
Chair: Moshe Vardi

08:45-08:55  Introduction and welcome

08:55-09:55  Natarajan Shankar, SRI International, USA
Invited talk: Little engines of proof
The automated construction of mathematical proof is a basic activity in computing. Since the dawn of the field of automated reasoning, there have been two divergent schools of thought. One school, best represented by Alan Robinson's resolution method, is based on simple uniform proof search procedures guided by heuristics. The other school, pioneered by Hao Wang, argues for problem-specific combinations of decision and semi-decision procedures. While the former school has been dominant in the past, the latter approach has greater promise. In recent years, several high quality inference engines have been developed, including propositional satisfiability solvers, ground decision procedures for equality and arithmetic, quantifier elimination procedures for integers and reals, and abstraction methods for finitely approximating problems over infinite domains. We describe some of these "little engines of proof" and a few of the ways in which they can be combined. We focus in particular on the combination ground decision procedures and their use in automated verification. We conclude by arguing for a modern reinterpretation and reappraisal of Hao Wang's hitherto neglected ideas on inferential analysis.

Session 1

Chair: Gordon Plotkin

10:00-10:05  Welcome to LICS by Samson Abramsky

10:05-10:35  Christopher Lynch, Clarkson U, USA
Barbara Morawska, Clarkson U, USA
Automatic decidability
We give a saturation procedure that takes a theory as input, and returns a decision procedure for that theory when it halts. In addition, it returns a bound on the complexity of that theory: O(nlg(n)) for some theories (such as the theory of lists), polynomial for other theories (including all equational theories that halt), and simply exponential for other theories (such as the theory of arrays).

Session 2

Chair: Leonid Libkin

11:00-11:30  Edmund M. Clarke, Carnegie Mellon U, USA
Somesh Jha, U Wisconsin-Madison, USA
Yuan Lu, Broadcom, USA
Helmut Veith, Vienna U of Techn., Austria
Tree-like counterexamples in model checking
Counterexamples for specification violations provide engineers with important debugging information. Although counterexamples are considered one of the main advantages of model checking, state-of the art model checkers are restricted to relatively simple counterexamples, and surprisingly little research effort has been put into counterexamples. In this paper, we introduce a new general framework for counterexamples. The paper has three main contributions:
(i) We determine the general form of ACTL counterexamples. To this end, we investigate the notion of counterexample and show that a large class of temporal logics beyond ACTL admits counterexamples with a simple tree-like transition relation. We show that the existence of tree-like counterexamples is related to a universal fragment of extended branching time logic based on omega-regular temporal operators.
(ii) We present new symbolic algorithms to generate tree-like counterexamples for ACTL specifications.
(iii) Based on tree-like counterexamples we extend the abstraction refinement methodology developed recently by Clarke et al. (CAV'2000) to full ACTL. This demonstrates the conceptual simplicity and elegance of tree-like counterexamples.

11:30-12:00  Sophie Laplante, U Paris XI (Paris-Sud), France
Richard Lassaigne, U Paris VII, France
Frederic Magniez, U Paris XI (Paris-Sud), France
Sylvain Peyronnet, U Paris XI (Paris-Sud), France
Michel de Rougemont, U Paris II, France
Probabilistic abstraction for model checking: An approach based on property testing
The goal of model checking is to verify the correctness of a given program, on all of its inputs. The main obstacle, in many cases, is the intractably large size of the program's transition system. Property testing is a randomized method to verify whether some fixed property holds on individual inputs. This is done by looking at a small random part of that input. We join the strengths of both approaches by introducing a new notion of probabilistic abstraction, and by extending the framework of model checking to include the use of these abstractions. Our abstractions map transition systems associated with large graphs to small transition systems associated with small random subgraphs. This reduces the original transition system to a family of small, even constant-size, transition systems. We prove that with high probability, "sufficiently" incorrect programs will be rejected (eps-robustness). We also prove that under a certain condition (exactness), correct programs will never be rejected (congruence). Our work applies to programs for graph properties such as bipartiteness, k-colorability, or any ∃∀ first order graph properties. Our main contribution is to show how to apply the ideas of property testing to syntactic programs for such properties. We give a concrete example of an abstraction for a program for bipartiteness. Finally, we show that the relaxation of the test alone does not yield transition systems small enough to use the standard model checking method. More specifically, we prove, using methods from communication complexity, that the OBDD size remains exponential for approximate bipartiteness.

12:00-12:30  Thomas Reps, U Wisconsin-Madison, USA
Alexey Loginov, U Wisconsin-Madison, USA
Mooly Sagiv, Tel Aviv U, Israel
Semantic minimization of 3-valued propositional formulae
This paper presents an algorithm for a non-standard logic-minimization problem that arises in 3-valued propositional logic. The problem is motivated by the potential for obtaining better answers in applications that use 3-valued logic. An answer of 0 or 1 provides precise (definite) information; an answer of 1/2 provides imprecise (indefinite) information. By replacing a formula phi with a "better" formula psi, we may improve the precision of the answers obtained. In this paper, we give an algorithm that always produces a formula that is "best" (in a certain well-defined sense).

Session 3

Chair: Peter O'Hearn

14:00-15:00  John C. Reynolds, Carnegie Mellon U, USA
Invited lecture: Separation Logic: A Logic for Shared Mutable Data Structures
In joint work with Peter O'Hearn and others, based on early ideas of Burstall, we have developed an extension of Hoare logic that permits reasoning about low-level imperative programs that use shared mutable data structure.
The simple imperative programming language is extended with commands (not expressions) for accessing and modifying shared structures, and for explicit allocation and deallocation of storage. Assertions are extended by introducing a "separating conjunction" that asserts that its subformulas hold for disjoint parts of the heap, and a closely related "separating implication". Coupled with the inductive definition of predicates on abstract data structures, this extension permits the concise and flexible description of structures with controlled sharing.
In this paper, we will survey the current development of this program.

15:00-15:30  Amal Ahmed, Princeton U, USA
Andrew W. Appel, Princeton U, USA
Roberto Virga, Princeton U, USA
A stratified semantics of general references embeddable in higher-order logic
We demonstrate a semantic model of general references - that is, mutable memory cells that may contain values of any (statically-checked) closed type, including other references. Our model is in terms of execution sequences on a von Neumann machine; thus, it can be used in a Proof-Carrying Code system where the skeptical consumer checks even the proofs of the typing rules. The model allows us to prove a frame-axiom introduction rule that allows locality of specification and reasoning, even in the event of updates to aliased locations. Our proof is machine-checked in the Twelf metalogic.

Session 4

Chair: Andy Pitts

16:00-16:30  Nadeem A. Hamid, Yale U, USA
Zhong Shao, Yale U, USA
Valery Trifonov, Yale U, USA
Stefan Monnier, Yale U, USA
Zhaozhong Ni, Yale U, USA
A syntactic approach to foundational proof-carrying code
Proof-Carrying Code (PCC) is a general framework for verifying the safety properties of machine-language programs. PCC proofs are usually written in a logic extended with language-specific typing rules. In Foundational Proof-Carrying Code (FPCC), on the other hand, proofs are constructed and verified using strictly the foundations of mathematical logic, with no type-specific axioms. FPCC is more flexible and secure because it is not tied to any particular type system and it has a smaller trusted base.
Foundational proofs, however, are much harder to construct. Previous efforts on FPCC all required building sophisticated semantic models for types. In this paper, we present a syntactic approach to FPCC that avoids the difficulties of previous work. Under our new scheme, the foundational proof for a typed machine program simply consists of the typing derivation plus the formalized syntactic soundness proof for the underlying type system. We give a translation from a typed assembly language into FPCC and demonstrate the advantages of our new system via an implementation in the Coq proof assistant.

16:30-17:00  Alan Jeffrey, DePaul U, USA
Julian Rathke, U Sussex, UK
A fully abstract may testing semantics for concurrent objects
This paper provides a fully abstract semantics for a variant of the concurrent object calculus. We define may testing for concurrent object components and then characterise it using a trace semantics inspired by UML interaction diagrams. The main result of this paper is to show that the trace semantics is fully abstract for may testing. This is the first such result for a concurrent object language.

17:00-17:30  Bernhard Reus, U Sussex, UK
Thomas Streicher, U Darmstadt, Germany
Semantics and logic of object calculi
The main contribution of this paper is a formal characterization of recursive object specifications based on a denotational untyped semantics of Abadi & Cardelli's object calculus and the discussion of existence of those (recursive) specifications. The existence theorem uses domain theoretical machinery known from the work of Freyd and Pitts. The semantics is then applied to prove soundness of a programming logic for the object calculus (by Abadi & Leino) and to suggest possible extensions. For the purposes of this discussion we use an informal logic of predomains in order to avoid any commitment to a special syntax of specification logic.

19:00-21:00  City Hall reception

Joint with FME, RTA
Room: City Hall