 | |
Sessions
take place in auditorium 1 unless otherwise indicated.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. |
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). |
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). |
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. |
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. |
Joint
with FME, RTA
Room:
City Hall | |
![[previous]](../img/prev.gif){kind=small}
![[up]](../img/up.gif){kind=small}
![[next]](../img/next.gif){kind=small}
