-
First International Workshop on
Rewriting Techniques for Program Transformations and Evaluation (WPTE 14)i
Vienna, Austria, 13th July 2014, proceedings
-
Rewriting Techniques and Applications (RTA)
joint with the
12th International Conference on
Typed Lambda Calculi and Applications (TLCA),
part of FLoC 2014. Vienna, Austria, 14. July - 17.July 2014.
-
Im Rahmen der Kolloquiumsveranstaltung
des Instituts für Informatik
der Goethe-Universität hat am
Dienstag, den 19. Juli um 10.15 Uhr
im Seminarraum 307 (Robert-Mayer-Str. 11-15)
Prof. Dr. Deepak Kapur
(University of New Mexico, USA)
einen Vortrag gehalten zum Thema
Inductive Theorem Proving, Invariants, and Abstraction
Abstract
Invariants play a key role in verifying properties of imperative programs. Inductive theorem proving is essential to verifying properties of recursive programs. Relationship between derivation of loop invariants and speculation of lemmas needed to do proofs by induction is explored. Abstraction is an effective heuristic for approximating program behavior in order to derive invariants. Interaction among developing abstractions, induction theorem proving, and generating invariants is investigated.
Kurzbiografie
Deepak Kapur is a distinguished professor of computer science at the University of New Mexico at Albuquerque. From 1998 until 2006, he served as the chair of the computer science department there. He has conducted research in areas of automated deduction, induction theorem proving, term rewriting, unification theory, formal methods, algebraic and geometric reasoning and their applications. His group built one of the first rewrite-based theorem provers, called Rewrite Rule Laboratory. He served as the editor-in-chief of the Journal of Automated Reasoning from 1993-2007. He is on the editorial board of Journal of Symbolic Computation and other journals. He received the Herbrand Award for distinguished contributions to automated reasoning in 2009.
- RTA 2011 - 22nd International Conference on Rewriting Techniques and Applications
Novi Sad (Serbia), May 30, 2011 - June 1, 2011
-
Im Rahmen des Instituskolloquims fand am
Montag, den 04. Oktober 2010
der Vortrag
"A Step-indexed Kripke Model of Hidden State"
von
Herrn Dr. Jan Schwinghammer (Universität des Saarlandes, Saarbrücken)
statt
Abstract
A Step-indexed Kripke Model of Hidden State
Frame and anti-frame rules have been proposed as proof rules for modular reasoning about programs. Frame rules allow one to hide irrelevant parts of the state during verification, whereas the anti-frame rule allows one to hide local state from the context.
I present frame and anti-frame rules in the setting of Chargueraud and Pottier's type and capability system for an ML-like language, and argue soundness of this system by describing a possible worlds model that is based on the operational semantics and step-indexed heap relations.
- 16. Jahrestagung der GI-Fachgruppe "Logik in der Informatik", November 6-7, 2009, Frankfurt am Main
-
Im Rahmen des Instituskolloquims fand am
Dienstag, den 16. Oktober 2007
der Vortrag
"Methods of Proving Correctness of Program Transformations Using Calculi"
von
Frau Prof. Elena Machkasova (University of Minnesota, Morris, USA)
statt
Abstract
Modern compilers not only convert programs to a lower-level representation, such as machine code, but also optimize programs to make them more efficient. Proving that such optimizations do not affect the results of a program is a challenging task. One of the methods that addresses such proofs is modeling a programming language in a formal system, often called a calculus, and using operational semantics to represent a program's evaluation.
In this talk I will introduce two systems for modeling programs and their transformations: the lambda calculus, a well known system for modeling functions, and its extension - a calculus of records which is used to model program modules. I will discuss properties of the calculi that allow us to prove that a certain class of program transformations preserve the behavior of a program. I will present two approaches to such proof: a method based on properties called confluence and standardization, which is suitable for the lambda calculus, and a method based on properties called lift and project that we developed for the calculus of records which lacks the confluence property.
This is joint work with Franklyn Turbak, Wellesley College, USA.
-
Im Rahmen des Instituskolloquims fand am
Mittwoch, den 28. Februar 2007
der Vortrag
"Separation Logic for General Storage"
von
Herrn Dr. Jan Schwinghammer (Universität des Saarlandes, Saarbrücken)
statt
Abstract
Logic is a substructural logic that supports local
reasoning about imperative programs, in the sense that for the
verification of program fragments only the
reachable part of the heap must be taken into account.
In past work, Separation Logic has been developed for heaps
containing records of basic data types.
Yet, languages like C or ML also allow procedures to be stored on
the heap. The corresponding heap model is commonly
referred to as "general storage" (or "higher-order store").
this talk I will address the problem of lifting Separation Logic
from first-order to higher-order store. To this end, we develop a
Hoare-style logic featuring Separation Logic connectives for a simple
imperative language with dynamic memory management and storable
commands. To prove soundness, the language is endowed with a
denotational semantics. As a benefit, we can reuse further powerful
proof rules for programs using general storage.
This is
joint work with Bernhard Reus, University of Sussex.
-
Im Rahmen des Instituskolloquims fand am
Mittwoch, den 27. Januar 2006
der Vortrag
"Node Selection Queries in XML documents by Tree Automata"
von
Herrn Dr. Joachim Niehren (INRIA Futurs, LIFL, Lille, France)
statt
Abstract
Motivated by an application in Web information extraction, we investigate n-ary node selection queries in HTML or XML trees. In the first part, we discuss the application and present the SQUIRREL system that we developed during the last 2 years in Lille. In the second part, we turn to the formal foundations, which belong to the domain of database theory, logic and automata. We study n-ary node selection queries in trees that are represented by successful runs of tree automata. We show that run-based n-ary queries capture MSO, contribute algorithms for enumerating answers of n-ary queries, and study the complexity of the problem. We investigate the subclass of run-based n-ary queries by unambiguous tree automata.
-
Im Rahmen des Instituskolloquims fand am
Freitag, den 23. Juli 2006
der Vortrag
"The Quest for Correct Programming Languages"
von
Herrn Christian Urban, Ph.D. (TU München)
statt
Abstract
No matter how much one probes the specification of a programming language for errors, to ensure that a programming language is correct one needs to give a mathematical proof. For small idealised programming languages proofs with "pencil and paper" are enough, but for non-trivial languages one needs to have computer support and correctness proofs that can be checked by machine.
In this talk a technique will be described for implementing with ease machine checkable proofs about the lambda-calculus. This work is based on the nominal approach to binders where terms have names in abstractions. A nominal datatype package, currently under development in the theorem prover Isabelle/HOL, is designed to help establishing the correctness of programming languages. The talk will describe some of the mathematical ideas behind this datatype package.
-
Im Rahmen des Instituskolloquims fand am
Mittwoch, den 17. August 2005
der Vortrag
"Beyond Secure Information Flow: A Classification of Declassifications."
von
Herrn Prof. David Sands, Ph.D. (Chalmers University of Technology and University of Göteborg)
statt
Abstract
Computing systems often deliberately release (or declassify) sensitive information. A principal security concern for systems permitting information release is whether this release is safe: is it possible that the attacker compromises the information release mechanism and extracts more secret information than intended?
While the security community has recognized the importance of the problem, the state-of-the-art in information release is, unfortunately, a number of approaches with somewhat unconnected semantic goals. We provide a road map
of the main directions of current research, by classifying the basic goals according to what information is released, who releases information, where in the system information is released, and when information can be released.
With a general declassification framework as a long-term goal, we identify some prudent principles of declassification. These principles shed light on existing definitions and may also serve as useful sanity checks for emerging models.
-
UNIF'99 (13th International Workshop on Unification)