Cape Hatteras Lighthouse

K 2010

1st International Workshop on the K Framework and its Applications

Nags Head, North Carolina, United States, August 15-22, 2010

9409 S. Old Oregon Inlet Road, Nags Head

Home page: http://fsl.cs.uiuc.edu/K10/, Contact e-mail: grosu@illinois.edu


PICTURE GALLERY


IMPORTANT DATES

August 15-22, 2010 Workshop in Nags Head, North Carolina

PRELIMINARY PROGRAM


Irina Mariuca Asavoae

Title: CEGAR in K : Past, Present, Future

Abstract: CEGAR is an well established abstraction refinement technique. The presentation will cover some background for this technique (for the Past section), the K specification of CEGAR with predicate abstraction (for the Present section), and CEGAR with predicate transition abstraction (for the Future section).


Mihail Asavoae

Title: WCET Estimation in K

Abstract: The presentation aims to investigate how K can be used in the specification and verification of non-functional requirements for embedded systems. A non-functional requirement, such as worst-case execution time (WCET) or power consumption, defines a quality of the execution. An estimation-based tool for non-functional requirements relies on the specification of both the program and the underlying architecture. The presentation includes the K definition of a low level programming language for the purpose of WCET estimation, the survey the state of the art WCET analysis techniques and how the K framework could help to tackle this problem.


Andrei Arusoaie

Title: On Compiling K Definitions

Abstract: TBD


Chucky Ellison

Title: A Formal Semantics of C with Applications

Abstract: This presentation describes an executable formal semantics for C expressed using K, a formalism based on rewriting logic. Being executable, the semantics has been thoroughly tested against the GCC torture test suite and successfully passes over 85% of the nearly 800 test programs. It is the most complete and thoroughly tested formal definition of C to date.

The semantics yields an interpreter, debugger, and state space search and model checker "for free". The semantics is shown capable of automatically finding program errors, both statically and at runtime. It is also used to enumerate nondeterministic behavior, and with an extension of simple concurrency primitives, Dekker's algorithm and the dining philosopher's problem are investigated.

Title: Formalizing Experimental Languages

Abstract: This talk describes a number of esoteric programming languages being given formal semantics using the K framework. Being quite different in both syntax and semantics from traditional programming languages, as well as being quite small, these case studies offer insight into what the definition of a language is and what it could be. The languages described will include at least Thue, Befunge, BrainF****, and possibly ReMorse.


Dorel Lucanu, Gheorghe Grigoras

Title: An overview on CIRC

Abstract: CIRC is a theorem prover able to prove coinductive and inductive properties using Circularity Principle. In this talk I will present the current status of CIRC and I will discuss in which way CIRC could be used in the context of K-framework.


Dorel Lucanu

Title: Modular defintions in K

Abstract: In this talk I will discus sevaral ways to define programming languages in K using a modular approach. In particular, I will focus on how to define a OO programming language starting from the definition of an imperative program languages (similar how C++ is built on top of C).


Grigore Rosu

Title: The K Framework: Overview and Current Status

Abstract: K is an executable semantic framework in which programming languages, calculi, as well as type systems or formal analysis tools can be defined, making use of configurations, computations and rules. Configurations organize the system/program state in units called cells, which are labeled and can be nested. Computations carry ``computational meaning'' as special nested list structures sequentializing computational tasks, such as fragments of program; in particular, computations extend the original language or calculus syntax.

K (rewrite) rules generalize conventional rewrite rules by making explicit which parts of the term they read, write, or do not care about. This distinction makes K a suitable framework for defining truly concurrent languages or calculi, even in the presence of sharing. Since computations can be handled like any other terms in a rewriting environment, that is, they can be matched, moved from one place to another in the original term, modified, or even deleted, K is particularly suitable for defining control-intensive language features such as abrupt termination, exceptions, or call/cc.

In this talk I will give an overview of the K framework: what it is, how it can be used, and where it has been used so far. I will also discuss several K definitions, both of conventional calculi and of paradigmatic languages.


Traian Florin Serbanuta

Title: K-Maude: Overview and Current Status

Abstract: TBD


AIMS AND SCOPE

K is an executable semantic framework in which programming languages, calculi, as well as type systems or formal analysis tools can be defined making use of configurations, computations and rules.

Since computations can be handled like any other terms in a rewriting environment, that is, they can be matched, moved from one place to another in the original term, modified, or even deleted, K is particularly suitable for defining control-intensive language features such as abrupt termination, exceptions or call/cc.

The topics of the workshop comprise, but are not limited to,

LOCATION

K 2010 will be held in Nags Head, on the Outer Banks of North Carolina, on August 15-22, 2010.

Located in Nags Head is the largest sand dune on the East Coast, Jockey's Ridge. The sand dune has migrated over the years from wind and erosion, and has buried a miniature golf course along the way. A castle is still visible and is a major landmark. Also buried is The Old Nags Head Hotel. The area surrounding Jockey's Ridge is good for biking, or hiking. Jockey's Ridge has been popular with Hang-gliders since the advent of the sport, as well as kite flyers and sand gliders. The Ridge includes an informative museum with exhibits on sand, weather, and area animals. The creatures outside are numerous and includes bird species, foxes, mice, squirels, occasional deer and friendly wild rabbits. One of the most exciting features of the Ridge is its capriciousness. Annual visitors find that lagoons can spring up, the sand can shift making for a fresh experience every time. From the top of the Ridge, the ocean as well as the sound can be seen. Jockey's Ridge has a sound beach on the Roanoke Sound side that visitors can swim in.

The Nags Head Woods Ecological Preserve is 1,092 acres (4.42 km2) and lies North of Jockey's Ridge and east of Roanoke Sound. It was designated a National Natural Landmark in 1974.

As in any other beach town, the ocean and shoreline are the major attractions, providing beaches for swimming, sunbathing, and a variety of water sports. A series of historic cottages overlook the beach in sections. There are three piers, Nags Head Pier, Jennette's Pier, and Outer Banks Pier which are popular for fishing.

A useful link for Nags Head is http://www.townofnagshead.net/. A live webcam of the ocean can be seen at http://beachcam.kdhnc.com/view/


PROGRAM COMMITTEE

Mihail Asavoae Alexandru Ioan Cuza University
Mariuca Asavoae Alexandru Ioan Cuza University
Chucky Ellison University of Illinois
Gheorghe Grigoras Alexandru Ioan Cuza University
Dorel Lucanu Alexandru Ioan Cuza University
Patrick Meredith University of Illinois
Elena Naum Alexandru Ioan Cuza University
Grigore Rosu University of Illinois
Traian Florin Șerbănuță University of Illinois
Andrei Ștefănescu University of Illinois


CONTACT INFORMATION

For more information, please contact the organizers

grosu@illinois.edu

or visit the workshop web page
http://fsl.cs.uiuc.edu/K10/


Cape Hatteras Lighthouse image reproduced above:
http://www.flickr.com/photos/razvanorendovici/ / CC BY 2.0
Information about Nags Head from Wikipedia: http://en.wikipedia.org/wiki/Nags_Head,_North_Carolina