[TYPES/announce] International School on Tool-based Rigorous Engineering of Software Systems

Claude Marche Claude.Marche at inria.fr
Fri Aug 29 05:42:02 EDT 2014




==========================================================================================


                           2014 International School on
         Tool-based Rigorous Engineering of Software Systems (STRESS 2014)
           (Associated with ISoLA 2014 -- 6th International Symposium on
                   Leveraging Applications of Formal Methods)

                              October 3 - 7, 2012
                                Corfu, Greece

   "STRESSING rigorous, tool-based, development approaches to software 
engineering"

                   http://santos.cis.ksu.edu/STRESS/2014/


The International School on Tool-based Rigorous Engineering of Software 
Systems (STRESS)
series aims to provide top-quality lectures and innovative pedagogical 
material that
provide young researchers with:

* instruction in existing and emerging formal methods and software 
engineering techniques
that are tool-supported and process-oriented,

* insights into how software is developed in the real world, including 
emphasis on domains
such as safety/mission-critical software and embedded systems where the 
development
effort associated with tool-based formal methods promises greatest returns,

* case-studies and example domains in which formal methods have been 
successfully
transitioned into actual development along with insights in how to 
bridge the gap
between research tools and actual development processes, and

* additional pedagogical resources and personal contacts that they can 
explore for the
purpose of increasing the impact of their research.

The theme of the 2014 International School is on Software Specification, 
Verification, and
Variation. It features lecturers from academic and industry with 
significant experience in
software contract, software analysis and certification, and software 
product lines.
Lectures will emphasize the use of program analyzers and verifiers,
model-driven development and software architecture tools, and 
industry-relevant challenge
problems.


--------
Lectures
--------

Introduction to Verification with Spark 2014
Lecturer: Yannick Moy (AdaCore)

SPARK 2014 is the latest evolution of the SPARK programming language. 
Based on Ada 2012,
it encompasses a rich subset of the language and augments it with 
further language
contracts designed to support advanced static verification techniques.

This lecture will provide a broad overview of the SPARK 2014 language: 
the subset of Ada
2012 which it includes and the additional constructs which it adds to 
support
verification. The morning session will cover basic features and static 
analysis
techniques. This will be followed by an introduction to one of the most 
novel features of
the language - the dual nature of the contracts as both executable and 
mathematical
statements and how these can be verified by testing, proof, or a 
combination of the two.

In the afternoon, the tutorial will look at more advanced language 
features that are
essential for industrial-scale specification, such as abstraction and 
refinement.
We will also look at more advanced verification techniques supported by 
the language
such as information flow analysis and proving the absence of run-time 
exceptions
(divide-by-zero, numeric overflow). Finally, we will touch on some of 
the more advanced
proof techniques that may be required.


Bakar Kiasan – A Certifying Program Verifier for High-Integrity Systems
Lecturers: Robby (Kansas State University) and John Hatcliff (Kansas 
State University)

Software-dependent critical systems that impact daily life are rapidly 
increasing in
number, size, and complexity. Unfortunately, inadequate software and 
systems engineering
can lead to accidents that cause economic disaster, injuries or death. 
There is a growing
reliance on development and verification tools to reduce costs, better 
manage complexity,
and to increase confidence in these systems. Recent standards for 
critical systems have
an increased emphasis on characterizing the requirements of tools used 
in the
certification context and the particular certification obligations that 
these tools can
discharge. In the case of avionics, DO-333 explicitly addresses the 
role/use of formal
methods tools, e.g., allowing formal verification of code compliance to 
procedure
contracts to replace unit testing.

This lecture presents the next generation Bakar Kiasan verifier in the 
Sireum platform
(sireum.org). Bakar Kiasan is a certifying symbolic execution-based 
program verifier for
high-integrity critical systems written using the Spark 2014 safe subset 
of Ada 2012.
It checks conformance of Spark programs against their contracts and 
produce evidence for
its analysis results. For example, it produces counter-examples and test 
cases for
contract violations. In addition, Bakar Kiasan produces test cases to 
illustrate contract
satisfactions as well as machine-checkable proofs for its contract 
verifications.
The lecture will present foundations of symbolic execution, discuss how 
evidence can be
generated from symbolic execution-based analysis, and will provide 
hands-on exercises
using Bakar Kiasan to verify Spark 2014 program units.


SCCE: Variability and Evolution through Integrated Domain, Data and 
Process Modeling
Lecturers: Bernhard Steffen (TU Dortmund), Tiziana Margaria (University 
of Potsdam),
          Stefan Naujokat (TU Dortmund), and Johannes Neubauer (TU Dortmund)

Domain-specific tool support is the key towards opening development 
responsibility for
a wider public without dedicated programming knowledge. This is, for 
example, important in
areas like business process modelling or scientific workflows. The 
intention behind the
tools and methods presented in this lecture lies in providing domain 
experts with
appropriate (non-programming) tools, so that they can solve problems 
within their domain
in a non-technical way and even construct domain-specific software 
products without
dedicated programming knowledge.

In the first session of this lecture we will introduce the Dynamic Web 
Application (DyWA)
framework that supports the prototype-driven development of 
process-oriented web
applications. It is a generic, fully functional prototype that 
accompanies the development
right from the beginning, offering a web-based definition facility for 
application domains
in terms of type schemata that captures the data types and their 
associations. The session
will provide hands-on experience on domain modeling with DyWA which 
automatically
generates the (complex) modeled data structures together with their 
fully executable
access functionality.

The second session focuses on ‘breathing life’ into the DyWA domain 
models via the process
modeling environment jABC4. In particular, it will illustrate the power of
prototype-driven process development throughout the whole system 
lifecylce, with a focus
on system evolution and system migration.

The third session presents Cinco, a particularly powerful application of 
our process
modeling framework based on the Eclipse ecosystem. Cinco is a meta 
tooling suite for
generating domain-specific graphical development tools in terms of fully 
operative
Eclipse products. It can be regarded as a domain-specific instance of 
generic meta
modeling frameworks such as Eclipse EMF/Graphiti which radically eases 
their use through
its domain-specific focus. Cinco is an application of our process 
modeling and design
framework jABC4 as all the required transformations, be they 
model-to-model or
model-to-code, are modeled with jABC4 so that they can also be developed 
without
specific programming knowledge. Please note that Cinco is a prime 
example for
bootstrapping. It is a tool for delevoping domain-specific development 
tools that is build
with a domain-specific development tool (jABC4). Indeed, the next 
version of jABC4,
jABC5 will be constructed in this very fashion. In the hands-on tutorial 
part of this
session the participants will use Cinco to create a full graphical DSL 
modeling tool of
their choice (e.g., for State Charts, Petri Nets, BPMN, Timed Automata, 
or even
architectural models or industrial plant layouts) consisting of an 
abstract specification
describing its structure and appearance, accompanied by a code generator 
that is modeled
in jABC4 using modeling components generated from the very same 
specification.


SMT-LIB and Kind
Lecturer: Cesare Tinelli (University of Iowa)

Many problems in computer science, in particular in formal methods, can 
be reduced to
checking the satisfiability of a formula in some logic. Several of these 
problems can be
naturally formulated as Satisfiability Modulo Theories (SMT) problems 
which are about
checking the satisfiability of first-order formulas with respect to some 
logical theory T
of interest. SMT differs from general automated deduction in that the 
background theory T
need not be finitely or even first-order axiomatizable, and specialized 
inference methods
are used for each theory. By being theory-specific and restricting their 
language to
certain classes of formulas, these specialized methods can be 
implemented in solvers that
are more efficient in practice than general-purpose theorem provers. SMT 
solvers have been
used successfully in several application ares including hardware 
verification, equivalence
checking, bounded and unbounded model checking, predicate abstraction, 
static analysis,
automated test case generation, extended static checking, and type checking.

The first session of this lecture will start with an overview of SMT and 
its applications,
followed by exercises using SMT solvers supporting the standard SMT-LIB 
input format, with
a focus on the CVC4 solver. CVC4 is a widely-used open-source SMT solver 
supporting a rich
set of logical theories including the theory of arrays, bit vectors, 
linear integer and
real arithmetic, algebraic data types and strings.

The second session will give a brief overview of model checking 
techniques relying on SMT
solvers, and show how to use the SMT-based Kind 2 model checker to prove 
invariant
properties of transition systems. Kind 2 checks multiple properties 
simultaneously by
running in parallel several model checking engines based on such 
techniques as bounded
model checking (BMC), k-induction, IC3/PDR, and automatic invariant 
generation.
The engines cooperate by exchanging information about the proven or 
disproven properties
as well as auxiliary invariants. Examples and exercises will use 
transition systems and
properties specified in the synchronous data flow language Lustre.


---------------
Important Dates
---------------

Early Registration Deadline: Sept. 1, 2014.
STRESS 2014: October 3-7, 2014.


-----
Venue
-----

STRESS is associated with the International Symposium on Leveraging 
Applications
of Formal Methods (ISoLA 2014). It will be held at the Grecotel Corfu 
Imperial
(http://www.corfuimperial.com/).

More information is available from the ISoLA 2014 general information page
(http://www.cs.uni-potsdam.de/isola/isola2014/general_information.html).


------------------------------
Registration and Accommodation
------------------------------

Please register and view accommodation information via ISoLA 2014 site
(http://www.cs.uni-potsdam.de/isola/isola2014/registration.html).


--------------------
Organizing Committee
--------------------

* John Hatcliff (Kansas State Univerisity)
* Tiziana Margaria (University of Potsdam)
* Robby (Kansas State Univerisity)
* Bernhard Steffen (TU Dortmund)






More information about the Types-announce mailing list