Last Call for Participation: GAMES 2009

                   GAMES 2009

    Annual Workshop of the ESF Networking Programme on
           Games for Design and Verification

             September 14 - 17, 2009
                   Udine, Italy
           http://games2009.dimi.uniud.it/

              LAST CALL FOR PARTICIPATION

GAMES is a European Network pursuing research and 
training on the design and verification of computing 
systems, in a framework that is based on the interplay 
of finite and infinite games, mathematical logic, and 
automata theory. 

For details, see www.games.rwth-aachen.de/

SCOPE:
The scope of the workshop includes the mathematical 
and algorithmic analysis of finite and infinite games, 
the interplay of games with automata theory and  logic, 
and applications of games, automata, and logic for the 
design and verification of computing systems.

PROGRAMME:
As in previous years, GAMES 2009 will be an informal 
workshop, without proceedings. Its programme consists 

[CiE] COMPUTABILITY IN EUROPE 2010: Programs, Proofs, Processes - Ponta Delgada (Azores), Portugal, June 30 to July 5 2010

Preliminary Announcement

----------------------------------------------------------------------------
              COMPUTABILITY IN EUROPE 2010: Programs, Proofs, Processes
                 Ponta Delgada (Azores), Portugal
                     June 30 to July 5 2010
                    http://www.cie2010.uac.pt/
----------------------------------------------------------------------------

CiE 2010 is the sixth in a successful series of conferences organised by
CiE (Computability in Europe), a European association of mathematicians,
logicians, computer scientists, philosophers, physicists and others
interested in new developments in computability and their underlying
significance for the real world. Previous meetings took place in
Amsterdam (2005), Swansea (2006), Siena (2007), Athens (2008), and
Heidelberg (2009). Please mark the conference dates in your agendas for
2010.

CONFIRMED TUTORIALS: Bruno Codenotti (Computational Game Theory).

CONFIRMED INVITED SPEAKERS: Seth Lloyd, Denis Hirschfeldt, Ronald de Wolf, 
Jose L. Balcazar, Eric Allender, Toniann Pitassi, and Sara Negri.

SPECIAL SESSIONS on

* Proof Theory and Computation, organizers: Martin Hyland, Fernando 
Ferreira

* Computational Complexity, organizers: Alan Selman, Elvira Mayordomo

SAC - Security Track: extended deadline 1 week (Sept 14th)

------------------------------------------------------------------------------
Let Crystal Reports handle the reporting - Free Crystal Reports 2008 30-Day 
trial. Simplify your report design, integration and deployment - and focus on 
what you do best, core application coding. Discover what's new with 
Crystal Reports now.  http://p.sf.net/sfu/bobj-july

_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Fwd: SAC - Security Track: extended deadline 1 week (Sept 15th)

------------------------------------------------------------------------------
Let Crystal Reports handle the reporting - Free Crystal Reports 2008 30-Day 
trial. Simplify your report design, integration and deployment - and focus on 
what you do best, core application coding. Discover what's new with 
Crystal Reports now.  http://p.sf.net/sfu/bobj-july

_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

ESSOS - 2nd call for papers

[Apologies if you receive this more than once]

CALL FOR PAPERS
================
International Symposium on Engineering Secure Software and Systems  
(ESSoS)

February 03-04, 2010
Pisa, Italy
http://distrinet.cs.kuleuven.be/events/essos2010

In cooperation with ACM SIGSAC and SIGSOFT (and IEEE CS (TCSE) -  
Pending)

CONTEXT AND MOTIVATION
Trustworthy, secure software is a core ingredient of the modern world.
Unfortunately, the Internet is too. Hostile, networked environments,  
like
the Internet, can allow vulnerabilities in software to be exploited from
anywhere. To address this, high-quality security building blocks (e.g.,
cryptographic components) are necessary, but insufficient. Indeed, the
construction of secure software is challenging because of the  
complexity of
modern applications, the growing sophistication of security  
requirements,
the multitude of available software technologies and the progress of  
attack
vectors. Clearly, a strong need exists for engineering techniques that
scale well and that demonstrably improve the software's security
properties.

GOAL AND SETUP
The goal of this symposium, which will be the second in the series, is  
to
bring together researchers and practitioners to advance the states of  
the
art and practice in secure software engineering. Being one of the few
conference-level events dedicated to this topic, it explicitly aims to
bridge the software engineering and security engineering communities,  
and
promote cross-fertilization. The symposium will feature two days of
technical program as well as one day of tutorials. The technical program
includes an experience track for which the submission of highly  
informative
case studies describing (un)successful secure software project  
experiences
and lessons learned is explicitly encouraged.

TOPICS
The Symposium seeks submissions on subjects related to its goals. This
includes a diversity of topics including (but not limited to):
- scalable techniques for threat modeling and analysis of  
vulnerabilities
- specification and management of security requirements and policies
- security architecture and design for software and systems
- model checking for security
- specification formalisms for security artifacts
- verification techniques for security properties
- systematic support for security best practices
- security testing
- security assurance cases
- programming paradigms, models and DLS's for security
- program rewriting techniques
- processes for the development of secure software and systems
- security-oriented software reconfiguration and evolution
- security measurement
- automated development
- trade-off between security and other non-functional requirements
- support for assurance, certification and accreditation

SUBMISSION AND FORMAT
The proceedings of the symposium are published by Springer-Verlag in the
Lecture Notes in Computer Science Series (http://www.springer.com/lncs).
Submissions should follow the formatting instructions of the Springer  
LNCS
Style.

Submitted papers must present original, non-published work of high  
quality.
The PC will select the papers into three categories:

Full Papers (16 pages plus bibliography)- describe novel original  
research
which is validated by either formal results, experimental analysis or
significant case study validation. The critical bar for acceptance in  
this
category is novelty and validation.

Industrial Reports (12 pagesplus bibliography) - describe the  
application
of existing research techniques or analysis methods to an industry level
case studies. The research results might be already published elsewhere,
here you show that you have applied them to something that is actually  
used
in an industrial setting (eg a real SAP product or a RedHat  
distribution).
A critical issue for acceptance here is applicability to a large scale.

Idea papers (8 pages plus bibliography) - describe an interesting novel
idea whose formal or experimental validation is not at the level of a  
full
paper, but whose potential is promising. An idea paper allows you to
timestamp your research contribution while giving you the chance to  
present
fully validate result at later conferences.

Proposals for tutorials are highly welcome as well. Further guidelines  
will
appear on the website of the symposium.

IMPORTANT DATES
Abstract submission: September 15, 2009
Paper submission: September 30, 2009
Author notification: November 15, 2009
Camera-ready: December 5, 2009
Tutorial submission: October 24, 2009
Tutorial notification: November 21, 2009

STEERING COMMITTEE
Jorge Cuellar (Siemens AG)
Wouter Joosen (Katholieke Universiteit Leuven) - chair
Fabio Massacci (Universita di Trento)
Gary McGraw (Cigital)
Bashar Nuseibeh (The Open University)
Daniel Wallach (Rice University University)

ORGANIZING COMMITTEE
General chair: Fabio Martinelli (C.N.R., IT)
Program co-chairs:
Fabio Massacci (Universita di Trento, IT) and
Dan Wallach (Rice University, USA)
Publication chair: N. Zannone (Eindhoven Technical Univ., NL)
Publicity chair: Yves Younan (Katholieke Universiteit Leuven, BE)
Local arrangements chair: Adriana Lazzaroni (C.N.R., IT)

PROGRAM COMMITTEE
Juergen Doser (IMDEA, ES)
Manuel Fahndrich (Microsoft Research, US)
Michael Franz (UC Irvine, US)
Dieter Gollmann (Hamburg University of Technology, DE)
Jan Jurjens (Open University, UK)
Seok-Won Lee (Univ. North Carolina Charlotte, US)
Antonio Mana (University of Malaga, ES)
Robert Martin (MITRE, USA)
Mattia Monga (Milan University, IT)
Fabio Massacci (Univ. of Trento) - Chair
Haris Mouratidis (Univ. of East London, UK)
Gunther Pernul (Universitat Regensburg, DE)
Samuel Redwine (James Madison University, USA)
David Sands (Chalmers Univ., SE)
Riccardo Scandariato (Katholieke Universiteit Leuven, BE)
Ketil Stolen (Sintef, NO)
Jon Whittle (Lancaster University, UK)
Mohammad Zulkernine (Queen's University, CA)
Neeraj Suri (Tech. Univ. Darmstadt, DE)
Yingjiu Li (Singapore Management Univ., SG)
Hao Chen (UC Davis, US)
Richard Clayton (Cambridge University, UK)
Eduardo Fernandez-Medina (University of Castilla-La Mancha, ES)
Yucel Karabulut (Office of CTO, SAP)
Vijay Varadharajan (Maquarie Univ, AU)
Jungfeng Yang (Columbia University, US)
Dan Wallach (Rice University) - Chair

------------------------------------------------------------------------------
Let Crystal Reports handle the reporting - Free Crystal Reports 2008 30-Day 
trial. Simplify your report design, integration and deployment - and focus on 
what you do best, core application coding. Discover what's new with 
Crystal Reports now.  http://p.sf.net/sfu/bobj-july

Deadline extended: Software Verification and Testing at ACM SAC 2010

Deadline for paper submission to the Software Verification and Testing 
Track ACM SAC 2010 has been extended:

Paper submission (new date): September 15, 2009

                  Call for papers

   ==============================================
   25th Annual ACM Symposium on Applied Computing
      Software Verification and Testing Track
     March 22 - 26, 2010, Sierre, Switzerland

    http://www.acm.org/conferences/sac/sac2010/

Important dates

* Sep 8th 2009: Submission deadline (extended to Sep 15)
* Oct 19th 2009: Notification of acceptance/rejection
* Nov 2nd 2009: Camera-ready versions due

ACM Symposium on Applied Computing

The ACM Symposium on Applied Computing (SAC) has gathered scientists
from different areas of computing over the past twenty-four years. The
forum represents an opportunity to interact with different communities
sharing an interest in applied computing.

SAC 2010 is sponsored by SIGAPP and will be hosted by the University of
Applied Sciences, Western Switzerland in Sierre, and École Polytechnique
Fédérale de Lausanne in Lausanne.

Software Verification and Testing Track

We invite authors to submit new results in formal verification and
testing, as well as development of technologies to improve the usability
of formal methods in software engineering. Also welcome are detailed
descriptions of applications of mechanical verification to large scale
software. Possible topics include, but are not limited to:

- tools and techniques for verification of large scale software systems
- real world applications and case studies applying software verification
- static and run-time analysis
- abstract interpretation
- model checking
- theorem proving
- correct by construction development
- model-based testing
- verification-based testing
- symbolic execution
- analysis methods for dependable systems
- software certification and proof carrying code

Submissions guidelines

Paper submissions must be original, unpublished work. Submissions should
be in electronic format, via the eCMS site:
http://sac.cs.iupui.edu/SAC2010/. Author(s) name(s) and address(es) must
not appear in the body of the paper, and self-reference should be
avoided and made in the third person. Submitted paper will undergo a
blind review process. Authors of accepted papers should submit an
editorial revision of their papers that fits within five two-column
pages (an extra three pages, to a total of eight pages, may be available
at a charge) following the ACM proceedings format reported here:
http://www.acm.org/conferences/sac/sac2010/2010_SAC_Word_Template.pdf.
Please comply to this page limitation already at submission time.
Publication of accepted articles requires the commitment of one of the
authors to register for the conference and present the paper. Accepted
papers will be published in the ACM SAC 2010 proceedings.

Program committee

Wolfgang Ahrendt, Chalmers University of Technology, Sweden
Ana Almeida-Matos, Instituto Superior Técnico, Portugal
Moritz Becker, Microsoft Research, UK
Laura Brandan-Briones, Universidad Nacional de Córdoba, Argentina
Jan Cederquist (track chair), Instituto Superior Técnico, Portugal
Carla Ferreira, Universidade Nova de Lisboa, Portugal
Joshua Guttman, Worcester Polytechnic Institute and The MITRE
Corporation, USA
Chris Hankin, Imperial College, UK
Daniel Kröning, Oxford University, UK
Jay Ligatti, University of South Florida, USA
MohammadReza Mousavi, Eindhoven University of Technology, The Netherlands
Jun Pang, University of Luxembourg, Luxembourg
Tamara Rezk, INRIA Sophia Antipolis Mediterranee, France
Mariëlle Stoelinga, University of Twente, The Netherlands
Mohammad Torabi Dashti, ETH Zürich, Switzerland
Nicolas Wolovick, Universidad Nacional de Córdoba, Argentina

------------------------------------------------------------------------------
Let Crystal Reports handle the reporting - Free Crystal Reports 2008 30-Day 
trial. Simplify your report design, integration and deployment - and focus on 
what you do best, core application coding. Discover what's new with 
Crystal Reports now.  http://p.sf.net/sfu/bobj-july

specify an out-of-order universally quantified variables?

Hi,

I have a theorem of the form:

!x1 x2 ... x(i-1) xi x(i+1) ... xn. t

and I'd like to instantiate xi to another term, say y, without touching 
other universally quantified variables, namely, I want to rewrite it to:

!x1 x2 ... x(i-1) x(i+1) ... xn. t[y/xi]

Is there a handy operation for this, any version of SPECL, or I can 
change the order of xs?

Thanks a lot.
Lu

------------------------------------------------------------------------------
Let Crystal Reports handle the reporting - Free Crystal Reports 2008 30-Day 
trial. Simplify your report design, integration and deployment - and focus on 
what you do best, core application coding. Discover what's new with 
Crystal Reports now.  http://p.sf.net/sfu/bobj-july

Re: specify an out-of-order universally quantified variables?

Hi Lu,

   This is easy to code up in HOL. You can strip
the leading foralls, use INST to replace your variable
by a term and then put all the foralls back, except
for the replaced one:

    fun MY_SPEC v tm th =
      let val (vs,body) = strip_forall(concl th)
          val (_,vs') = Lib.pluck (equal v) vs
      in
         GENL vs' (INST [v |-> tm] (SPEC_ALL th))
      end;

Example:

- val th = mk_thm([],``!(x1:num) (x2:'a) (x3:bool list). P x1 x2 x3  
x3``);
 > val th = |- !x1 x2 x3. P x1 x2 x3 x3 : thm

- MY_SPEC ``x2:'a`` ``foo:'a`` th;
 > val it = |- !x1 x3. P x1 foo x3 x3 : thm

You will have to take care that v and tm have the same
type.

Cheers,
Konrad.

On Sep 11, 2009, at 12:15 PM, Lu Zhao wrote:

> Hi,
>
> I have a theorem of the form:
>
> !x1 x2 ... x(i-1) xi x(i+1) ... xn. t
>
> and I'd like to instantiate xi to another term, say y, without  
> touching
> other universally quantified variables, namely, I want to rewrite  
> it to:
>
> !x1 x2 ... x(i-1) x(i+1) ... xn. t[y/xi]
>
> Is there a handy operation for this, any version of SPECL, or I can
> change the order of xs?
>
> Thanks a lot.
> Lu
>
> ---------------------------------------------------------------------- 
> --------
> Let Crystal Reports handle the reporting - Free Crystal Reports  
> 2008 30-Day
> trial. Simplify your report design, integration and deployment -  
> and focus on
> what you do best, core application coding. Discover what's new with
> Crystal Reports now.  http://p.sf.net/sfu/bobj-july
> _______________________________________________
> hol-info mailing list
> hol-info <at> lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info

------------------------------------------------------------------------------
Let Crystal Reports handle the reporting - Free Crystal Reports 2008 30-Day 
trial. Simplify your report design, integration and deployment - and focus on 
what you do best, core application coding. Discover what's new with 
Crystal Reports now.  http://p.sf.net/sfu/bobj-july

STACS 2010 - Last call for papers

------------------------------------------------------------------------------
Come build with us! The BlackBerry® Developer Conference in SF, CA
is the only developer event you need to attend this year. Jumpstart your
developing skills, take BlackBerry mobile applications to market and stay 
ahead of the curve. Join us from November 9-12, 2009. Register now!
http://p.sf.net/sfu/devconf

_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Call for Abstracts -- Designing Correct Circuits 2010

I attach a Call for Abstracts for the "Designing Correct Circuits"
workshop to be held next March in Cyprus as a satellite event of
ETAPS2010.

I would be most grateful if you would bring it to the attention of any
colleagues and friends who might be interested  -- and, please,
consider submitting an abstract yourself!

(Apologies if you accidentally get multiple copies of this.)

Regards

joe stoy

Designing Correct Circuits 2010
A Satellite Workshop of ETAPS'10
Cyprus, 20-21 March 2010

CALL FOR ABSTRACTS

Abstracts due: Monday 23 November 2009
Notification of acceptance: Monday 21 December 2009
Final version: Wednesday 20 January 2010

A two-day workshop on the topic Designing Correct Circuits will be held on
20-21 March 2010 in Cyprus, as part of the ETAPS group of conferences. The
workshop will bring together researchers in formal methods for hardware design
and verification from academia and industry. It will allow participants to
learn about the current state of the art in formally-based hardware design and
verification, and is intended to spark debate about how more effective
verification methods can be developed. Much research in these areas now takes
place in industry, rather than in academia. For the long term survival of our
field, we must ensure that academics and industrial researchers continue to
work together on the real problems in correct circuit design and verification,
including those currently being faced in microprocessor design,
System-on-a-Chip development, and in the automotive and aerospace industries.

A major aim of this workshop is to strengthen the existing communication
channels and to open more of them. The DCC workshops have been held biennially
since 2002 and have always been a great success in creating an informal forum
where these issues could be discussed. We hope for something similar in 2010.

This call invites you to submit a one page description of a talk that you
would like to give at this workshop. One page abstracts of your talks can be
submitted to Joe Stoy (stoy <at> bluespec.com) by 23 November 2009. The
abstract should describe original work, and should indicate what distinguishes
your work from other research on languages for and approaches to the design
and verification of hardware. Describe the status of your work such as, for
example, industrial experience with conclusions, new idea with prototype
implementation, new theory, comparison of methods, etc. Please indicate
clearly how your talk will contribute to the kind of debate that we are hoping
to generate. Include a list of references on a second page if you
wish. Researchers from both industry and academia are encouraged to submit
talks. Speakers from industry who would be willing to present research
problems that they face (and with which they need help) would also be
welcome. We would like to be able to present a broad view of the current state
of the art in design and verification methods.

The final programme will be agreed by the workshop committee no later than 21
December 2009, and a final version of the material for the participants
proceedings will be due on 20 January 2010. This would preferably be a draft
paper, but could also be slides. The workshop speakers and the workshop
committee will decide after the workshop whether or not to make a more
permanent record, for example by arranging a special issue of a journal.


Workshop Committee

Arvind (MIT)
Per Bjesse (Synopsys)
Wolfgang Kunz (University of Kaiserslautern)
Bob Kurshan (Cadence)
Pete Manolios (Northeastern University)
Andy Martin (IBM)
Tom Melham (University of Oxford)
Gordon Pace (University of Malta)
Marc Pouzet (University of Paris-Sud)
Carl Seger (Intel)
Satnam Singh (Microsoft)
Joe Stoy (Bluespec)

Contact:
Joe Stoy (stoy <at> bluespec.com)

------------------------------------------------------------------------------
Come build with us! The BlackBerry® Developer Conference in SF, CA
is the only developer event you need to attend this year. Jumpstart your
developing skills, take BlackBerry mobile applications to market and stay 
ahead of the curve. Join us from November 9-12, 2009. Register now!
http://p.sf.net/sfu/devconf

_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info