Lin, Yuhui | 3 Aug 12:13 2015
Picon
Picon

AVoCS 2015: Final Call for Research Idea Papers & Participation

======================================================================
              
              The 15th International Workshop on 
          Automated Verification of Critical Systems 
             1-4 September 2015, Edinburgh, UK

          https://sites.google.com/site/avocs15/

                avocs2015 <at> easychair.org
                
-----------------------|*** HIGHLIGHTS ***|---------------------------- 
+ Registration is now open !
+ Special research ideas session: short papers due 10th August
+ Several student grants available: application due 10th August
+ Invited talks by
    Colin O'Halloran (D-RisQ/Oxford) 
    Don Sannella (Contemplate/Edinburgh)
+ AI4FM workshop including invited talk by 
    J Strother Moore (Univerity of Texas at Austin)
+ Proceedings to be published by EASST  
+ Special issues of Science of Computer Programming
=======================================================================

REGISTRATION
  Registration for AVoCS is available from

    https://sites.google.com/site/avocs15/registration

  
  Early registration ends 18 August.

SPONSORS
(Continue reading)

宋丹 | 31 Jul 14:16 2015
Picon

Second CFP: Fourth International Seminar on Program Verification, Automated Debugging and Symbolic Computation

 

             PAS 2015 - Fourth International Seminar on

Program Verification, Automated Debugging and Symbolic Computation

                Beijing, China, October 21-23, 2015

                      http://pas2015.cc4cm.org/

 

Important Dates

  - Submission of abstracts                         August 15, 2015

  - Submission of papers/extended abstracts:        August 20, 2015

  - Notification of acceptance or rejection:     September 20, 2015

  - Final version due:                             October 10, 2015

  - Seminar taking place:                       October 21-23, 2015

 

Overview

 

PAS 2015 will provide a forum for researchers and software developers

actively involved or interested in developing, using, and applying

methods and software tools of symbolic computation for program

verification and automated debugging to exchange ideas and views, to

review the state of the art and discuss prospects, to present research

results and experiments,  and to build up contacts for future

cooperation. The scientific program of the seminar will feature

invited talks and contributed presentations.

 

Specific topics for PAS 2015 include (but are not limited to):

 

  - Theories and methodologies for program verification and testing

  - Model checking, fault locating and program repairing

  - Symbolic computation and automated reasoning for program verification

  - Termination, correctness and complexity analysis of programs

  - Automated program synthesis and transformation

  - Logic and semantics for automated and algorithmic debugging

  - Program debugging paradigms and techniques

  - Symbolic constraint solving for verification and debugging

  - Tools, prototypes, empirical and case studies

 

The previous seminars PAS 2012 and PAS 2013 were held in Beijing, China,

and PAS 2014 was part of the Federated Logic Conference (FLoC) and the

Vienna Summer of Logic.

 

 

Submission guideline

 

Potential participants of PAS 2015 are invited to submit first half-page

abstracts and then full papers or extended abstracts (3-5 pages)

describing their work to be presented at the seminar. The submitted full

papers and extended abstracts will be reviewed by the program committee

for soundness and relevance to the seminar. Submission of original

research papers is encouraged, while published material and work in

progress will also be considered for presentation at the seminar.

Electronic submissions are strongly preferred using EasyChair:

 

https://easychair.org/conferences/?conf=pas20150

 

Accepted full papers and extended abstracts will be distributed at the

seminar. Authors of the full papers and extended abstracts accepted for

presentation at the seminar will be invited to submit their full and/or

revised papers for publication in the post-proceedings volume as a special

issue of the Journal of Symbolic Computation (JSC) after the meeting.

The submitted papers will be formally reviewed by external referees

according to the standard refereeing procedure of JSC.

 

 

Honorary Chair

 

Wei Li (Beihang University, China)

 

 

Steering Committee

 

Hoon Hong (North Carolina State University, USA)

Tudor Jebelean (Johannes Kepler University, Austria)

Jens Knoop (Technical University of Vienna, Austria)

Alexander Letichevsky (Cybernetics National Academy of Sciences, Ukraine)

Wei Li (Beihang University, China)

Dongming Wang (Beihang University, China and CNRS, France)

 

Program Chairs

 

Tudor Jebelean (Johannes Kepler University, Austria)

Dongming Wang (Beihang University, China and CNRS, France)

 

 

Program Committee

 

Sandra Alves (University of Porto, Portugal)

Alessandro Armando (University of Genova, Italy)

Armin Biere (Johannes Kepler University, Austria)

Xiaoyu Chen (Beihang University, China)

Stefan Ciobaca (University A. I. Cuza, Romania)

Isabela Dramnesc (West University of Timisoara, Romania)

Madalina Erascu (West University of Timisoara, Romania)

Mario Florido (University of Porto, Portugal)

Martin Giese (University of Oslo, Norway)

Fairouz Kamareddine (Heriot-Watt University, Scotland)

Jens Knoop (Technical University of Vienna, Austria)

Boris Konev (University of Liverpool, England)

Laura Kovacs (Chalmers University of Technology, Sweden)

Gabor Kusper (Eszterhazy Karoly College, Hungary)

Oleksandr Letychevskyi (Glushkov Institute of Cybernetics, Ukraine)

Dorel Lucanu (University A. I. Cuza, Romania)

Jie Luo (Beihang University, China)

Alexander Maletzky (Johannes Kepler University, Austria)

Mircea Marin (West University of Timisoara, Romania)

Marius Minea (Politehnica University of Timisoara, Romania)

Grant Passmore (University of Cambridge, England)

Vladimir Peschanenko (Kherson State University, Russia)

Judit Robu (Babes-Bolyai University, Romania)

Michael Rusinowitch (LORIA - INRIA Nancy, France)

Vlad Rusu (INRIA, France)

Wolfgang Schreiner (Johannes Kepler University, Austria)

Martina Seidl (Johannes Kepler University, Austria)

Viorica Sofronie-Stokkermans (University of Koblenz, Germany)

Kaile Su (Griffith University, Australia)

Wolfgang Windsteiger (Johannes Kepler University, Austria)

Naijun Zhan (Chinese Academy of Sciences, China)

 

 

Local Arrangements

 

Xiaoyu Chen (Beihang University, China)

Aishan Liu (Beihang University, China)

Dan Song (Beihang University, China)

-------------------------------------------------------------
If you do not wish to receive announcements from the
Research Institute for Symbolic Computation (RISC),
please send an e-mail to the following address:
secretary <at> risc.jku.at

------------------------------------------------------------------------------
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
rim.abid | 30 Jul 17:50 2015
Picon
Picon

Software Verification and Testing Track, ACM SAC 2016 (Pisa, Italy) - Second CFP

==================================================
31st Annual ACM Symposium on Applied Computing
Software Verification and Testing Track
April 3 - 8, 2016, Pisa, Italy

More information:
http://antares.sip.ucm.es/svt16/ and
http://www.acm.org/conferences/sac/sac2016/
===================================================

Important dates
---------------

* September 11, 2015: Paper submission
* November 13, 2015: Paper notification
* December 11, 2015: Camera-Ready Copies

ACM Symposium on Applied Computing
----------------------------------

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

SAC 2016 is sponsored by the ACM Special Interest Group on Applied
Computing (SIGAPP), and will be hosted by the University of Pisa and
Scuola Superiore Sant'Anna University, Italy

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:

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

Submissions Guidelines
----------------------

Paper submissions must be original, unpublished work. Submissions
should be in electronic format, via the START site:
http://www.acm.org/conferences/sac/sac2016/Paper-SubmissionUploadPage.htm

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 six two-column pages (an extra two pages, to a total
of eight pages, may be available at a charge). Please comply to this
page limitation already at submission time. Accepted papers will be
published in the ACM SAC 2016 proceedings.

Paper registration is required, allowing the inclusion of papers,
posters, or SRC abstracts in the conference proceedings. An author or
a proxy attending SAC MUST present the work. This is a requirement for
the presented work to be included in the ACM/IEEE digital
library. No-show of registered papers, posters, and SRC abstracts will
result in excluding them from the ACM/IEEE digital library.

A special issue of Journal of Systems and Software has been
confirmed. Selected papers will be invited for submission, and will be
peer-reviewed according to the standard policy of Journal of Systems
and Software.

Student Research Competition
----------------------------

As before, SAC 2016 organises a Student Research Competition (SRC)
Program to provide graduate students the opportunity to meet and
exchange ideas with researchers and practitioners in their areas of
interest. Guidelines and information about the SRC program can be
found at http://www.acm.org/conferences/sac/sac2016/. Submission to
the SRC program should be in electronic form via the following website
http://www.acm.org/conferences/sac/sac2016/SRC-SubmissionUploadPage.htm

Program Committee 
-----------------

Rui Abreu, University of Porto, Portugal 
Cristiano Braga, Universidade Federal Fluminense, Brazil
Radu Calinescu, University of York, UK 
Ana Cavalli, National Institute of Telecommunications, France 
Byoungju Choi, Ewha Womans University, Republic of Korea 
Maximiliano Cristiá, Universidad Nacional de Rosario, Argentina 
Khaled El-Fakih, American University of Sharjah, UAE 
Ylies Falcone, University of Grenoble Alpes, France 
Maria del mar Gallardo, University of Malaga, Spain 
Arie Gurfinkel, Carnegie Mellon University, USA
Tingting Han, University of London, UK 
Klaus Havelund, Nasa Jet Propulsion Laboratory, USA
Ralf Huuck, UNSW, Australia
Nikolai Kosmatov, CEA, France 
Stefan Leue, University of Konstanz, Germany 
Luis Llana, Universidad Complutense de Madrid, Spain 
Jasen Markovski, R&D group, GN Resound Benelux, The Netherlands 
Mohammad Mousavi, Halmstad University, Sweden 
Madhavan Mukund, Chennai Mathematical Institute, India
Shin Nakajima, National Institute of Informatics, Tokyo, Japan 
Brian Nielsen, Aalborg University, Denmark 
Peter Olveczky, University of Oslo, Norway 
Jun Pang, University of Luxembourg, Luxembourg 
Adenilso Simao, ICMC/USP, Brazil
Marjan Sirjani, Reykjavik University, Iceland 
Marielle Stoelinga, University of Twente, The Netherlands 
Jun Sun, Singapore University of Technology and Design
Tanja Vos, Valencia University, Spain 
Carsten Weise, Imbus AG, Germany 
Anton Wijs, Eindhoven University of Technology, The Netherlands 
Nina Yevtushenko, Tomsk State University, Russia
Cemal Yilmaz, Sabanci University, Turkey 
Fatiha Zaidi, Univ. Paris-Sud, France 
Gianluigi Zavattaro, University of Bologna, Italy 
Lijun Zhang, Chinese Academy of Sciences, China

Program Committee Chairs
-----------------

Mercedes G. Merayo, Universidad Complutense de Madrid, Spain
Gwen Salaün, University of Grenoble Alpes, France

------------------------------------------------------------------------------
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Alwen Tiu | 22 Jul 10:49 2015
Picon

One postdoc and two PhD positions on formal verification of security protocols

[Apologies for multiple postings]

One postdoc and two PhD positions are available at the School of Computer Engineering, Nanyang Technological University (NTU)  Singapore.

The postdocs and the PhDs positions are for a project on verification of security
protocols funded by the Ministry of Education of Singapore. A particular emphasis will be on designing and implementing decision procedures for finding attacks on protocols or producing formal proofs of their security. We will be using a mixture of process algebraic and logical frameworks to express protocols and their properties. 

For the postdoc position: 
=========================
Candidates must possess a PhD degree in Computer Science or related areas. Candidates with strong backgrounds in process calculus, such as the pi-calculus and its variants, and/or formal logic and theorem proving are preferred. For further details, including the salary range, please refer to the job ads at:


The position will be initially offered for one year, but can be extended up to three years, subject to satisfactory performance and availability of funding. 

To apply for the position, please send a cover letter and your latest CV (please indicate names of three referees in your CV) by email to Alwen Tiu (atiu <at> ntu.edu.sg, alwen.tiu <at> gmail.com). Applications will be accepted until the position is filled, but to ensure the full consideration of your application, please send your application by 21 August 2015. Only shortlisted candidates will be notified of the results of their applications. The selected candidate is expected to commence in October 2015.


For the PhD positions: 
======================
please send an email to Alwen Tiu (atiu <at> ntu.edu.sg) to express your interests. Please refer to the following website for application procedures and requirements. 

For the intake of January 2016, applications must be received by 31 August 2015. 
 

If you have any further questions, please contact atiu <at> ntu.edu.sg.


Regards,
Alwen Tiu

------------------------------------------------------------------------------
Don't Limit Your Business. Reach for the Cloud.
GigeNET's Cloud Solutions provide you with the tools and support that
you need to offload your IT needs and focus on growing your business.
Configured For All Businesses. Start Your Cloud Today.
https://www.gigenetcloud.com/
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Martin Fränzle | 14 Jul 09:11 2015
Picon

CfP: 2nd Autumn School on Automatic Analysis and Verification of Complex Systems


                      CALL for PARTICIPATION

                        2nd Autumn School on
       Automatic Verification and Analysis of Complex Systems

         Oldenburg, Germany, September 30 to October 2, 2015

                   http://www.avacs.org/autumn2015

BACKGROUND AND OBJECTIVES

"Automatic Verification and Analysis of Complex Systems" is an autumn
school focussing on automated formal methods in computer science and
their application to the analysis and verification of complex embedded
systems. Targeting primarily PhD students and young researchers with
an interest in safety-critical embedded systems, the technical program
comprises talks from 12 specialists in the field of automated formal
methods, covering the range from hard real-time systems over hybrid
systems to dynamically restructuring systems of systems.

LECTURERS

Overview:
    Werner Damm (Carl von Ossietzky Universität Oldenburg, D)

Hybrid Systems:
    Goran Frehse (Université Joseph Fourier Grenoble, F)
    André Platzer (Carnegie Mellon University, PA, USA)
    Thomas Sturm (Max-Planck-Institut für Informatik, D)

Real-Time:
    Kim G. Larsen (Aalborg Universitet, DK)
    Ernst-Rüdiger Olderog (Carl von Ossietzky Universität Oldenburg, D)
    Andrey Rybalchenko (Microsoft Research, UK)
    Mani Swaminathan (Carl von Ossietzky Universität Oldenburg, D)

Systems of Systems:
    Paolo Marin (Albert-Ludwigs-Universität Freiburg, D)
    David Parker (University of Birmingham, UK)
    Sven Schewe (University of Liverpool, UK)
    Ralf Wimmer (Albert-Ludwigs-Universität Freiburg, D)

VENUE

The autumn school will be held at the Carl von Ossietzky University
Oldenburg.  Please see the autumn school's website
www.avacs.org/autumn2015 for travel information.

REGISTRATION AND COST

Registration to the school is performed electronically via the web
form at www.avacs.org/autumn2015. Early registration is recommended,
as the number of participants is limited. A waiting list will be
opened if the number of enrollees exceeds the number of available
places.

The participation fee is 140 EUR (approx. 156 USD) for early
registration and 180 EUR (approx. 200 USD) for normal registration.
Early registration is possible until August 31. Thereafter, only
normal registration is possible. The registration fee covers the
lectures, course materials, and a social event including a conference
dinner.

ACCOMMODATION

A number of hotels in Oldenburg have reserved rooms at special
rates. For details consult the school's web page
www.avacs.org/autumn2015 .

ORGANIZATION

The autumn school is organized by the large scale transregional
research center "AVACS" (Automatic Verification and Analysis of
Complex Systems, www.avacs.org), funded by the Deutsche
Forschungsgemeinschaft DFG (www.dfg.de/en/index.html).

Inquiries can be addressed to the local organizers Martin Fränzle,
Thomas Scheidsteger, and Jürgen Niehaus via email: autumn2015 <at> avacs.org .

FURTHER INFORMATION

www.avacs.org/autumn2015

------------------------------------------------------------------------------
Don't Limit Your Business. Reach for the Cloud.
GigeNET's Cloud Solutions provide you with the tools and support that
you need to offload your IT needs and focus on growing your business.
Configured For All Businesses. Start Your Cloud Today.
https://www.gigenetcloud.com/
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Makarius | 15 Jul 15:25 2015
Picon

HOL4 build, deps etc.

Dear HOL4 experts,

I am trying to understand HOL4 build management.  After some initial 
struggles, I have managed to make a regular build of everything via 
bin/build.  Now I want to see which sources are used in which canonical 
order.

The file tools/build-sequence appears to specify that abstractly, but I 
want to get the resulting sequences of ML files.  I've looked around 
tools/build.sml and tools/buildutils.sml a bit, and it ultimately seems to 
converge towards Holmake invocations.

The latter is unclear to me.  Which are typical targets, e.g. for the 
kernel or core theories?  Maybe there is even some Holmake command line 
option to ask for used file dependencies of such targets?

 	Makarius

------------------------------------------------------------------------------
Don't Limit Your Business. Reach for the Cloud.
GigeNET's Cloud Solutions provide you with the tools and support that
you need to offload your IT needs and focus on growing your business.
Configured For All Businesses. Start Your Cloud Today.
https://www.gigenetcloud.com/
Ramana Kumar | 15 Jul 10:25 2015
Picon
Picon

Unicode versions

What is the difference between these functions?

Parse.overload_on
Parse.Unicode.uoverload_on
Parse.Unicode.unicode_version

Which ones should be used when? Does more than one need to be used at once? From some of my recent playing around, it seems like unicode_version sometimes but not always requires an additional call to one of the overload functions before the parser recognises the unicode version. That is pretty confusing behaviour.
------------------------------------------------------------------------------
Don't Limit Your Business. Reach for the Cloud.
GigeNET's Cloud Solutions provide you with the tools and support that
you need to offload your IT needs and focus on growing your business.
Configured For All Businesses. Start Your Cloud Today.
https://www.gigenetcloud.com/
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
宋丹 | 9 Jul 16:46 2015
Picon

Call for papers - PAS 2015

              PAS 2015 - Fourth International Seminar on
Program Verification, Automated Debugging and Symbolic Computation
               Beijing, China, October 21-23, 2015
                   http://pas2015.cc4cm.org/
 
Important Dates

 - Submission of abstracts:                        August 15, 2015
 - Submission of papers/extended abstracts:        August 20, 2015
 - Notification of acceptance or rejection:     September 20, 2015
 - Final version due:                             October 10, 2015
 - Seminar taking place:                       October 21-23, 2015

Overview

PAS 2015 will provide a forum for researchers and software developers
actively involved or interested in developing, using, and applying
methods and software tools of symbolic computation for program verification
and automated debugging to exchange ideas and views, to review the state of
the art and discuss prospects, to present research results and experiments,
and to build up contacts for future cooperation. The scientific program of
the seminar will feature invited talks and contributed presentations.

Specific topics for PAS 2015 include (but are not limited to):

 - Theories and methodologies for program verification and testing
 - Model checking, fault locating and program repairing
 - Symbolic computation and automated reasoning for program verification
 - Termination, correctness and complexity analysis of programs
 - Automated program synthesis and transformation
 - Logic and semantics for automated and algorithmic debugging
 - Program debugging paradigms and techniques
 - Symbolic constraint solving for verification and debugging
 - Tools, prototypes, empirical and case studies

The previous seminars PAS 2012 and PAS 2013 were held in Beijing, China,
and PAS 2014 was part of the Federated Logic Conference (FLoC) and the
Vienna Summer of Logic.


Submission

Potential participants of PAS 2015 are invited to submit first half-page
abstracts and then full papers or extended abstracts (3-5 pages) describing
their work to be presented at the seminar. The submitted full papers and
extended abstracts will be reviewed by the program committee for soundness
and relevance to the seminar. Submission of original research papers is
encouraged, while published material and work in progress will also be
considered for presentation at the seminar. Electronic submissions are
strongly preferred using EasyChair:

https://easychair.org/conferences/?conf=pas20150

Accepted full papers and extended abstracts will be distributed at the
seminar. Authors of the full papers and extended abstracts accepted for
presentation at the seminar will be invited to submit their full and/or
revised papers for publication in the post-proceedings volume as a special
issue of the Journal of Symbolic Computation (JSC) after the meeting.
The submitted papers will be formally reviewed by external referees
according to the standard refereeing procedure of JSC.


Honorary Chair

Wei Li (Beihang University, China)


Steering Committee

Hoon Hong (North Carolina State University, USA)
Tudor Jebelean (Johannes Kepler University, Austria)
Jens Knoop (Technical University of Vienna, Austria)
Alexander Letichevsky (Cybernetics National Academy of Sciences, Ukraine)
Wei Li (Beihang University, China)
Dongming Wang (Beihang University, China and CNRS, France)


Program Chairs

Tudor Jebelean (Johannes Kepler University, Austria)
Dongming Wang (Beihang University, China and CNRS, France)


Program Committee

Jens Knoop (Technical University of Vienna, Austria)
Hoon Hong (North Carolina State University, USA)
Alexander Letichevsky (Cybernetics National Academy of Sciences, Ukraine)
Jie Luo (Beihang University, China)
Madalina Erascu (West University of Timisoara, Romania)
Isabela Dramnesc (West University of Timisoara, Romania)
Alexander Maletzky (Johannes Kepler University, Austria)
Svetlana Cojocaru (Institute of Mathematics and Computer Science, Moldova)
Alexander Lyaletski (Kiev National Taras Shevchenko University, Ukraine)
(To be completed)


Local Arrangements

Xiaoyu Chen (Beihang University, China)
Aishan Liu ( Beihang University, China)
Dan Song (Beihang University, China)

 

------------------------------------------------------------------------------
Don't Limit Your Business. Reach for the Cloud.
GigeNET's Cloud Solutions provide you with the tools and support that
you need to offload your IT needs and focus on growing your business.
Configured For All Businesses. Start Your Cloud Today.
https://www.gigenetcloud.com/
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
MUNOZ, CESAR (LARC-D320 | 13 Jul 23:04 2015
Picon

[fm-announcements] Final CFP -- 11th Int. Workshop on Developments in Computational Models

FINAL CALL FOR PAPERS -- DCM 2015

11th International Workshop on Developments in Computational Models

October 28, 2015, Cali, Colombia
http://dcm-workshop.org.uk/2015/


A satellite event of ICTAC 2015 - http://www.ictac2015.co


DEADLINE FOR SUBMISSION OF EXTENDED ABSTRACTS (5 pages): AUGUST 3, 2015
======================================================

Several new models of computation have emerged in the last few years, and
many developments of traditional computational models have been proposed
with the aim of taking into account the new demands of computer systems
users and the new capabilities of computation engines. A new computational
model, or a new feature in a traditional one, usually is reflected in a
new family of programming languages, and new paradigms of software
development.

DCM 2015 is the eleventh in a series of international workshops focusing
on new computational models. The aim of this workshop is to bring together
researchers who are currently developing new computational models or new
features for traditional computational models, in order to foster their
interaction, to provide a forum for presenting new ideas and work in
progress, and to enable newcomers to learn about current activities in
this area.

DCM 2015 will be a one-day satellite event of ICTAC 2015, the Twelfth
International Colloquium on Theoretical Aspects of Computing.

== TOPICS OF INTEREST
Topics of interest include all abstract models of computation and their
properties, and their applications to the development of programming
languages and systems:

- functional calculi: lambda-calculus, rho-calculus, term and graph
rewriting;
- quantum computation, including implementations and formal methods in
quantum protocols;
- probabilistic computation and verification in modeling situations;
- chemical, biological and bio-inspired computation, including spatial
models, self-assembly, growth models;
- models of concurrency, including the treatment of mobility, trust, and
security;
- infinitary models of computation;
- information-theoretic ideas in computing.

== IMPORTANT DATES
- Submission Deadline for Extended Abstracts: August 3
- Notification: 13 September
- Pre-proceedings version due: 5 October
- Workshop: 28 October
- Submission Deadline for EPTCS Proceedings: 7 December

== INVITED SPEAKERS
Mauricio Ayala Rincón, Universidade de Brasilia (Brazil).
Gilles Dowek, INRIA (France).

== SUBMISSIONS
Submit your paper in PDF format via the conference EasyChair submission
page:
https://www.easychair.org/conferences/?conf=dcm2015


Submissions should be an abstract of at most 5 pages, written in English.
Simultaneous submission to journals, conferences or other workshops is not
permitted. Please use the EPTCS macro package and follow the instructions
of EPTCS, following the EPTCS style:
http://style.eptcs.org/


A submission may contain an appendix, but reading the appendix should not
be necessary to assess its merits. After the workshop authors are invited
to submit a full paper of their presentation. Accepted contributions will
appear in an issue of EPTCS.

== PROGRAM COMMITTEE:
Mario Benevides (Brazil)
Luís Caires (Portugal)
Ugo Dal Lago (Italy)
Nachum Dershowitz (Israel)
Jérôme Feret (France)
Marcelo Frias (Argentina)
Russ Harmer (France)
Ivan Lanese (Italy)
Radu Mardare (Denmark)
Elvira Mayordomo (Spain)
César A. Muñoz (USA) - chair
Jorge A. Pérez (The Netherlands) - chair
Andrés Sicard-Ramírez (Colombia)
Alexandra Silva (The Netherlands)
Daniele Varacca (France)

---
To opt-out from this mailing list, send an email to

fm-announcements-request <at> lists.nasa.gov

with the word 'unsubscribe' as subject or in the body. You can also make the request by contacting

fm-announcements-owner <at> lists.nasa.gov 
------------------------------------------------------------------------------
Don't Limit Your Business. Reach for the Cloud.
GigeNET's Cloud Solutions provide you with the tools and support that
you need to offload your IT needs and focus on growing your business.
Configured For All Businesses. Start Your Cloud Today.
https://www.gigenetcloud.com/
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Christian Urban | 13 Jul 02:47 2015
Picon

ITP 2015 Call for Participation


Please find the ITP 2015 Call for Participation below.

***************************************************************
The 6th International Conference on Interactive Theorem Proving

          24 - 27 August 2015 in Nanjing, China

    http://www.inf.kcl.ac.uk/staff/urbanc/itp-2015/

Isabelle and Coq tutorials before and after the main conference
***************************************************************  

ITP is the premier international conference for researchers from 
all areas of interactive theorem proving and its applications. 
The pc accepted 30 papers this year

  http://www.inf.kcl.ac.uk/staff/urbanc/itp-2015/accepted.html

There will be invited talks by

  Lars Birkedal
  Michael Norrish

There will be a three-day Isabelle tutorial before the conference
and a three-day Coq tutorial after the conference.

  http://www21.in.tum.de/~nipkow/isa-tut-itp15.html
  http://www.strub.nu/coq-itp-15

ALL RECENT INFO and ON-LINE REGISTRATION can be found at:

   http://www.inf.kcl.ac.uk/staff/urbanc/itp-2015/  

If you need any help with travelling and staying inside
China, we try our best to help.

    Xingyuan Zhang and Christian Urban
    (ITP 2015 co-chairs)

------------------------------------------------------------------------------
Don't Limit Your Business. Reach for the Cloud.
GigeNET's Cloud Solutions provide you with the tools and support that
you need to offload your IT needs and focus on growing your business.
Configured For All Businesses. Start Your Cloud Today.
https://www.gigenetcloud.com/
Andrius Velykis | 12 Jul 15:53 2015
Picon
Picon

AI4FM 2015: Final call for short contributions

AI4FM 2015
The 6th International Workshop on the use of AI in Formal Methods


1st September 2015 in Edinburgh, Scotland.  
In association with AVoCS 2015 (https://sites.google.com/site/avocs15)



Important dates
----------

Submission deadline: 1st August 2015  
Notification of acceptance: 10th August 2015  
Final version due: 21st August 2015  
Workshop: 1st September 2015  



Overview
----------

The 6th International Workshop on the use of AI in Formal Methods (AI4FM 2015) will be held on the 1st of September, 2015 in Edinburgh, Scotland.

The AI4FM workshops bring together researchers from formal methods, automated reasoning and AI; aiming to address the issue of how AI can be used to support the formal software development process, including requirement analysis, modelling and proof. The workshops include a mix of industrial and academic participants and we anticipate attracting a similarly diverse audience in AI4FM 2015.


We invite 3-page short contributions (extended abstracts) presenting work in the areas of automated reasoning, formal methods and artificial intelligence. The authors can submit work in progress, tools under development, and PhD projects to facilitate and benefit from the active dialog between the groups involved in these research areas.


Invited speaker:

J Strother Moore (https://www.cs.utexas.edu/~moore/, University of Texas at Austin, US) will be giving an invited talk at AI4FM 2015.



Topics of interest
----------

The main aim for the workshop is discussion, thus submissions do not need to be original. Extended versions of submissions may have been published previously, or submitted concurrently with or after AI4FM 2015 to another workshop, conference or a journal. Presentations of work in progress, tools under development, and PhD projects are also encouraged.

The scope of the workshop covers the research in automated reasoning, formal methods and artificial intelligence. Particular topics of interest include, but are not limited to:

 - The use of AI and automated reasoning to support and guide the formal modelling process.
 - The use of AI and automated reasoning in the requirement capture process.
 - The use of AI to reuse formal models, programs and proofs.
 - The use of machine learning to support interactive theorem proving.
 - The use of machine learning to enhance automated theorem proving.
 - The development of search heuristics.
 - The use of AI for term synthesis, invariant generation, lemma discovery and concept invention.
 - The use of AI for counter-example generation.
 - The use of constraint solvers in formal methods.
 - The role of AI planning for formal systems developments, from requirements to the end product (including software and hardware).
 - The interplay between reasoning and modelling and the role of AI in this framework.
 - Ontologies in the formal engineering process.
 - Novel ideas on how to use AI (e.g. machine learning, pattern recognition) in proof automation.
 - Use of cloud elasticity for: scalability on large scale developments, proof/lemma exploration.
 - Techniques for bridging the development to maintenance gap.



Submission
----------

Submission is by email to:


Please submit an abstract up to 3 pages in a PDF format. The extended abstracts will be handed out to all participants, and will be made into a technical report prior to the workshop.

Acceptance for presentation at the workshop will be made by the organisers based on relevance to the workshop.



Student grants
----------

Thanks to sponsorships from Altran, FME, and SICSA we can offer financial support for a limited number of students registering for AVoCS in the form of a registration fee waiver (full or partial, registration covers the AI4FM workshop in addition to AVoCS). As this is limited, we ask the students that would like to take the advantage of this support to submit a short application.

The details on how to apply are available on the AVoCS website:



Organisers
----------

 - Leo Freitas (Newcastle University, UK)
 - Andrius Velykis (Newcastle University, UK)
 - Gudmund Grov (Heriot-Watt University, UK)


If you have any queries, please email the organisers at the following e-mail address:


------------------------------------------------------------------------------
Don't Limit Your Business. Reach for the Cloud.
GigeNET's Cloud Solutions provide you with the tools and support that
you need to offload your IT needs and focus on growing your business.
Configured For All Businesses. Start Your Cloud Today.
https://www.gigenetcloud.com/
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Gmane