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: email@example.com
|August 15-22, 2010||Workshop in Nags Head, North Carolina|
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).
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.
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.
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.
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.
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).
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.
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.
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/
|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|
For more information, please contact the organizers