Rob Arthan | 28 May 17:08 2016

Google is not always your friend

I was trying to find a reference for the introduction of conversions in LCF.
The link below is interesting, but not what I was looking for :-).


Regards,

Rob.
------------------------------------------------------------------------------
What NetFlow Analyzer can do for you? Monitors network bandwidth and traffic
patterns at an interface-level. Reveals which users, apps, and protocols are 
consuming the most bandwidth. Provides multi-vendor support for NetFlow, 
J-Flow, sFlow and other flows. Make informed decisions using capacity 
planning reports. https://ad.doubleclick.net/ddm/clk/305295220;132659582;e
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Abid Rauf | 28 May 09:19 2016
Picon

Overload Resolution

Dear All,

Good day!

I am trying to overload resolution for matrices. But it is giving error. Can anyone tell me what exactly is the cause of error?

This states that if we have two matrices of order mxn and pxq, the resulting matrix after operation has order mpxnp.

overload_interface ("%%%",`(Kron_prod):real^N^M->real^Q^P->real^(N*Q)^(M*P)`);;

error is:

Exception: Failure "type expected"


Best Regards,
Abid Rauf
Ph.D Scholar (CS) & RA SAVe Labs,
School of Electrical Engineering and Computer Science (SEECS),
National University of Science and Technology (NUST), H-12, Islamabad, Pakistan
------------------------------------------------------------------------------
What NetFlow Analyzer can do for you? Monitors network bandwidth and traffic
patterns at an interface-level. Reveals which users, apps, and protocols are 
consuming the most bandwidth. Provides multi-vendor support for NetFlow, 
J-Flow, sFlow and other flows. Make informed decisions using capacity 
planning reports. https://ad.doubleclick.net/ddm/clk/305295220;132659582;e
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Waqar Ahmad | 27 May 07:14 2016
Picon

Translating HOL4 function to SML

Hi all,

I am trying to translate some defined HOL4 functions to their equivalent functions in SML. For instance, there is a function "exp ": real->real in a HOL4 'transcTheory' and I want to compute it using a similar SML function `Math.exp`.

So, I have written a translator function as follows:

fun sml_of_hol_real_exp t =
    let val failstring = "Symbolic expression could not be translated in a number" in
    if fst (dest_comb t) = ``exp:real->real`` then
          Math.exp <TERM TO REAL> (snd (dest_comb t))
       else failwith failstring
  end;

A possible usage of above function can be  sml_of_hol_real_exp ``exp 0.4``;

Now, I need a kind of operator in place of <TERM TO REAL>  that can give an argument to Math.exp function for computation... Can anybody have an idea about this?

--
Thanks and best regards,

Waqar Ahmed


------------------------------------------------------------------------------
What NetFlow Analyzer can do for you? Monitors network bandwidth and traffic
patterns at an interface-level. Reveals which users, apps, and protocols are 
consuming the most bandwidth. Provides multi-vendor support for NetFlow, 
J-Flow, sFlow and other flows. Make informed decisions using capacity 
planning reports. https://ad.doubleclick.net/ddm/clk/305295220;132659582;e
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Abid Rauf | 27 May 03:23 2016
Picon

(no subject)



Best Regards,
Abid Rauf
Ph.D Scholar (CS) & RA SAVe Labs,
School of Electrical Engineering and Computer Science (SEECS),
National University of Science and Technology (NUST), H-12, Islamabad, Pakistan
------------------------------------------------------------------------------
What NetFlow Analyzer can do for you? Monitors network bandwidth and traffic
patterns at an interface-level. Reveals which users, apps, and protocols are 
consuming the most bandwidth. Provides multi-vendor support for NetFlow, 
J-Flow, sFlow and other flows. Make informed decisions using capacity 
planning reports. https://ad.doubleclick.net/ddm/clk/305295220;132659582;e
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Abid Rauf | 27 May 03:30 2016
Picon

help needed.

Dear All,

Good day. I want to solve the problem below. I am trying  e(SIMP_TAC[REAL_MUL_AC]);; but its not working here. Please help.


 0 [`1 <= (i:num) /\ (i:num) <= dimindex (:?576605)`]
  1 [`1 <= (i':num) /\ (i':num) <= dimindex (:?576604)`]

`(A:real^N^M)$
 (((i:num) - 1) DIV dimindex (:?576596) + 1)$
 (((i':num) - 1) DIV dimindex (:?576597) + 1) *
 (lambda (i:num) (j:num).
      (B:real^Q^P)$
      (((i:num) - 1) DIV dimindex (:V) + 1)$
      (((j:num) - 1) DIV dimindex (:U) + 1) *
      (C:real^V^U)$
      (((i:num) - 1) MOD dimindex (:V) + 1)$
      (((j:num) - 1) MOD dimindex (:U) + 1))$
 (((i:num) - 1) MOD dimindex (:?576596) + 1)$
 (((i':num) - 1) MOD dimindex (:?576597) + 1) =
 (A:real^N^M)$
 (((i:num) - 1) DIV dimindex (:?576612) + 1)$
 (((i':num) - 1) DIV dimindex (:?576613) + 1) *
 (lambda (i:num) (j:num).
      (B:real^Q^P)$
      (((i:num) - 1) DIV dimindex (:V) + 1)$
      (((j:num) - 1) DIV dimindex (:U) + 1) *
      (C:real^V^U)$
      (((i:num) - 1) MOD dimindex (:V) + 1)$
      (((j:num) - 1) MOD dimindex (:U) + 1))$
 (((i:num) - 1) MOD dimindex (:?576612) + 1)$
 (((i':num) - 1) MOD dimindex (:?576613) + 1)`

Thanks in advance. Cheers!.

Best Regards,
Abid Rauf
Ph.D Scholar (CS) & RA SAVe Labs,
School of Electrical Engineering and Computer Science (SEECS),
National University of Science and Technology (NUST), H-12, Islamabad, Pakistan
------------------------------------------------------------------------------
What NetFlow Analyzer can do for you? Monitors network bandwidth and traffic
patterns at an interface-level. Reveals which users, apps, and protocols are 
consuming the most bandwidth. Provides multi-vendor support for NetFlow, 
J-Flow, sFlow and other flows. Make informed decisions using capacity 
planning reports. https://ad.doubleclick.net/ddm/clk/305295220;132659582;e
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Barbara Kordy | 26 May 09:27 2016
Picon

GraMSec'16 CALL FOR PARTICIPATION

******************************************************************
GraMSec 2016
The Third International Workshop on Graphical Models for Security
Co-located with CSF 2016

Lisbon, Portugal - June 27, 2016
http://gramsec.uni.lu/
******************************************************************

GraMSec REGISTRATION IS NOW OPEN

To register please follow the instructions given at
http://www.gramsec.uni.lu/registration.php

ABOUT GraMSec

Graphical security models provide an intuitive but systematic
methodology to analyze security weaknesses of systems and to evaluate
potential protection measures. Such models have been subject of
academic research and they have also been widely accepted by the
industrial sector, as a means to support and facilitate threat
analysis and risk assessment processes. The objective of GraMSec is to
contribute to the development of well-founded graphical security
models, efficient algorithms for their analysis, as well as
methodologies and tools for their practical usage.

INVITED TALK

Xinming Ou, University of South Florida, USA
A Bottom-up Approach to Applying Graphical Models in Security Analysis

ACCEPTED REGULAR PAPERS

* Maxime Audinot and Sophie Pinchinat.
   On the Soundness of Attack Trees

* Xinshu Dong, Sumeet Jauhar, William G. Temple, Binbin Chen, Zbigniew 
Kalbarczyk, William H. Sanders, Nils Ole Tippenhauer and David M. Nicol.
   The Right Tool for the Job: a Case for Common Input Scenarios for 
Security Assessment

* Marlon Dumas, Luciano García-Bañuelos and Peeter Laud.
   Differential Privacy Analysis of Data Processing Workflows

* Eric Li, Jeroen Barendse, Frederic Brodbeck and Axel Tanner.
   From A to Z: Developing a Visual Vocabulary for Information Security 
Threat Visualisation

* Nihal Pekergin, Sovanna Tan and Jean-Michel Fourneau.
   Quantitative Attack Tree Analysis: Stochastic Bounds and Numerical 
Analysis

* Ricardo J. Rodríguez, Xiaolin Chang, Xiaodan Li and Kishor S. Trivedi.
   Survivability Analysis of a Computer System under an Advanced 
Persistent Threat Attack

* Paul Rowe.
   Confining Adversary Actions via Measurement

ACCEPTED SHORT PAPERS

* Olga Gadyatskaya, Carlo Harpes, Sjouke Mauw, Cedric Muller and Steve 
Muller.
   Bridging Two Worlds: Reconciling Practical Risk Assessment 
Methodologies with Theory of Attack Trees

* Henk Jonkers and Dick Quartel.
   Enterprise Architecture-Based Risk and Security Modelling and Analysis

GENERAL CHAIR
Barbara Kordy, INSA Rennes, IRISA, France

PROGRAM COMMITTEE CO-CHAIRS
Mathias Ekstedt, KTH Royal Institute of Technology, Sweden
DongSeong Kim, University of Canterbury, New Zealand

CONTACT
For inquiries please send an e-mail to gramsec16 <at> easychair.org

------------------------------------------------------------------------------
What NetFlow Analyzer can do for you? Monitors network bandwidth and traffic
patterns at an interface-level. Reveals which users, apps, and protocols are 
consuming the most bandwidth. Provides multi-vendor support for NetFlow, 
J-Flow, sFlow and other flows. Make informed decisions using capacity 
planning reports. https://ad.doubleclick.net/ddm/clk/305295220;132659582;e
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Havelund, Klaus (348B | 10 May 00:42 2016
Picon
Picon

[fm-announcements] RV 2016, Deadlines Extended - Abstract: May 20, Paper/Tutorial: May 27


Following several requests, the deadlines have been extended as follows:

- Abstract deadline: Friday May 20 (AoE).
- Paper and tutorial deadline: Friday May 27 (AoE).

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


RV 2016

16th International Conference on Runtime Verification

September 23-30, Madrid, Spain


Scope

Runtime verification is concerned with monitoring and analysis of software and hardware system executions. Runtime verification techniques are crucial for system correctness, reliability, and robustness; they are significantly more powerful and versatile than conventional testing, and more practical than exhaustive formal verification. Runtime verification can be used prior to deployment, for testing, verification, and debugging purposes, and after deployment for ensuring reliability, safety, and security and for providing fault containment and recovery as well as online system repair. Topics of interest to the conference include:

- specification languages
- specification mining
- program instrumentation
- monitor construction techniques
- logging, recording, and replay
- runtime enforcement, fault detection, localization, containment, recovery and repair
- program steering and adaptation
- metrics and statistical information gathering
- combination of static and dynamic analyses
- program execution visualization
- monitoring techniques for safety/mission-critical systems
- monitoring distributed systems, cloud services, and big data applications
- monitoring security and privacy policies

Application areas of runtime verification include cyber-physical systems, safety/mission-critical systems, enterprise and systems software, autonomous and reactive control systems, health management and diagnosis systems, and system security and privacy.

Invited Speakers

The program of RV 2016 will feature invited talks from:

  • Gul Agha (University of Illinois at Urbana-Champaign, USA)
  • Oded Maler (CNRS and University of Grenoble-Alpes, France)
  • Fred B. Schneider (Cornell University, USA)

Overview

RV 2016 will be held September 23-30 in Madrid, Spain. RV 2016 will feature the first summer school on Runtime Verification (September 23-25), two workshop/tutorial days (September 26-25), and three conference days (September 28-30).

General Information on Submissions

All papers and tutorials will appear in the conference proceedings in an LNCS volume. Submitted papers and tutorials must use the LNCS/Springer style. At least one author of each accepted paper and tutorial must attend RV 2016 to present the paper. Papers must be written in English and submitted electronically (in PDF format) using the EasyChair system. The below page limitations include all text and figures, but exclude references. Additional details omitted due to space limitations may be included in a clearly marked appendix that will be reviewed at the discretion of reviewers.

Research Papers Track

Research papers can be submitted in two categories: regular and short papers. Papers in both categories will be reviewed by at least 3 members of the Program Committee.
  • Regular Papers (up to 15 pages) should present original unpublished results. Theoretical papers, system and application papers as well as case studies on runtime verification are all welcome.
    The Program Committee will give a best paper award. A selection of accepted regular papers will be invited to appear in a special issue of the Springer Journal on Formal Methods in System Design.
  • Short Papers (up to 6 pages) may present novel but not necessarily thoroughly worked out ideas, for example emerging runtime verification techniques and applications, or techniques and applications that establish relationships between runtime verification and other domains. Accepted short papers will be presented in special talk (15 minutes) and poster sessions.

Tool Papers Track

The aim of the RV 2016 tool track is to provide an opportunity for researchers and practitioners to show and to discuss the latest advances, experiences and challenges in devising and developing reliable software tools for runtime verification. All tool papers will be reviewed by at least 3 members of the Tool Committee. An author of each accepted tool paper should give a 15-20 minutes demonstration during the conference.

All tool papers must include information on tool availability, maturity, selected experimental results and it should provide a link to a website containing the theoretical background and user guide. Furthermore, we strongly encourage authors to make their tools and benchmarks available with their submission.
We encourage tool papers to include a script in an appendix (not included in the page count) describing how the demo will be conducted during the conference presentation with screenshots presenting step-by-step the tool’s capabilities, highlighting the main characteristics and the usage.

Tool papers can be submitted into two categories:

  • Regular Tool Papers (up to 8 pages). A tool paper in this category should present a new tool, a new tool component or significant and novel extensions to existing tools supporting runtime verification. Each submission should be original and not published previously in a tool paper form.
  • Tool Exhibition Papers (up to 4 pages). A tool paper in this category can have been previously published. A tool paper in this category should be oriented towards the tool usage and is an opportunity for the developers to present them at RV 2016.

Tutorial Track

Tutorials are two-to-three-hour presentations on a selected topic. Additionally, tutorial presenters will be offered to publish a paper of up to 20 pages in the LNCS conference proceedings.

A proposal for a tutorial must contain the subject of the tutorial, a proposed timeline, a note on previous similar tutorials (if applicable) and the differences to this incarnation, and a biography of the presenter. The proposal must not exceed 2 pages. Tutorial proposals will be reviewed by the Program Committee.

(new) Important Dates

Research and tool papers as well as tutorials will follow the following timeline:

  • Abstract deadline: May 20, 2016 (AoE)
  • Paper and tutorial deadline: May 27, 2016 (AoE)
  • Tutorial notification: June 15, 2016
  • Paper notification: July 18, 2016
  • Camera ready deadline: August 8, 2016
  • Summer school: September 23-25, 2016
  • Workshops and tutorials: September 26-27, 2016
  • Conference: September 28-30, 2016

Committees

Program Committee Chairs


  • Yliès Falcone, Univ. Grenoble-Alpes and Inria, France
  • Cesar Sanchez, IMDEA Software, Madrid, Spain

Tool Committee Chair


  • Klaus Havelund, NASA Jet Propulsion Laboratory, USA

Local Organization Chair


  • Juan E. Tapiador, Universidad Carlos III de Madrid, Spain

Program Committee


  • Erika Abraham, RWTH Aachen University, Germany
  • Howard Barringer, The University of Manchester, UK
  • Ezio Bartocci, TU Wien, Austria
  • Andreas Bauer, NICTA & Australian National University, Australia
  • Saddek Bensalem, Univ. Grenoble Alpes, France
  • Eric Bodden, Fraunhofer SIT and Technische University Darmstadt, Germany
  • Borzoo Bonakdarpour, McMaster University, Canada
  • Laura Bozzelli, Technical University of Madrid (UPM), Spain
  • Juan Caballero, IMDEA Software Institute, Spain
  • Wei-Ngan Chin, National University of Singapore, Singapore
  • Christian Colombo, University of Malta, Malta
  • Jyotirmoy Deshmukh, Toyota Technical Center, USA
  • Alexandre Donzé, UC Berkeley EECS Department, USA
  • Yliès Falcone, Univ. Grenoble Alpes and Inria, France
  • Bernd Finkbeiner, Saarland University, Germany
  • Adrian Francalanza, University of Malta, Malta
  • Vijay Garg, The University of Texas at Austin, USA
  • Patrice Godefroid, Microsoft Research, USA
  • Susanne Graf, Univ. Grenoble Alpes and CNRS, France
  • Radu Grosu, Vienna University of Technology, Austria
  • Sylvain Hallé, Université du Québec à Chicoutimi, Canada
  • Klaus Havelund, NASA Jet Propulsion Laboratory, USA
  • Johan Jaffar, National University of Singapore, Singapore
  • Thierry Jéron, Inria Rennes – Bretagne Atlantique, France
  • Johannes Kinder, Royal Holloway University of London, UK
  • Felix Klaedtke, NEC Europe Ltd., Germany
  • Kim G. Larsen, Aalborg University, Denmark
  • Axel Legay, Inria Rennes – Bretagne Atlantique, France
  • Martin Leucker, University of Lübeck, Germany
  • Benjamin Livshits, Microsoft Research, USA
  • Joao Lourenço, Universidade Nova de Lisboa, Portugal
  • Rupak Majumdar, MPI-SWS, Germany
  • Leonardo Mariani, University of Milano Bicocca, Italy
  • David Naumann, Stevens Institute of Technology, USA
  • Dejan Nickovic, Austrian Institute of Technology, Austria
  • Gordon Pace, University of Malta, Malta
  • Doron Peled, Bar Ilan University, Israel
  • Lee Pike, Galois, Inc., USA
  • Grigore Rosu, University of Illinois at Urbana-Champaign, USA
  • Gwen Salaün, Univ. Grenoble Alpes and Inria, France
  • Cesar Sanchez, IMDEA Software Institute, Spain
  • Sriram Sankaranarayanan, University of Colorado Boulder, USA
  • Gerardo Schneider, University of Gothenburg, Sweden
  • Scott Smolka, Stony Brook University, USA
  • Oleg Sokolsky, University of Pennsylvania, USA
  • Bernhard Steffen, University of Dortmund, Germany
  • Scott Stoller, Stony Brook University, USA
  • Volker Stolz, University of Oslo, Norway
  • Jun Sun, Singapore University of Technology and Design, Singapore
  • Juan Tapiador, Universidad Carlos III de Madrid, Spain
  • Serdar Tasiran, Koc Univ., Turkey
  • Michael Whalen, University of Minnesota, USA
  • Eugen Zalinescu, ETH Zurich, Switzerland
  • Lenore Zuck, University of Illinois at Chicago, USA

Tool Committee


  • Steven Arzt, EC Spride, Germany
  • Howard Barringer, The University of Manchester, UK
  • Ezio Bartocci, TU Wien, Austria
  • Martin Leucker, University of Luebeck, Germany
  • Gordon Pace, University of Malta, Malta
  • Giles Reger, The University of Manchester, UK
  • Julien Signoles, CEA, France
  • Oleg Sokolsky, University of Pennsylvania, USA
  • Bernhard Steffen, University of Dortmund, Germany
  • Nikolai Tillmann, Microsoft Research, USA
  • Eugen Zalinescu, ETH Zurich, Switzerland

---
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 
------------------------------------------------------------------------------
Mobile security can be enabling, not merely restricting. Employees who
bring their own devices (BYOD) to work are irked by the imposition of MDM
restrictions. Mobile Device Manager Plus allows you to control only the
apps on BYO-devices by containerizing them, leaving personal data untouched!
https://ad.doubleclick.net/ddm/clk/304595813;131938128;j
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Isabela Dramnesc | 21 May 19:04 2016
Picon

CFP Synasc 2016, Timisoara, Romania

---
Final Call for Papers
--------------------------

                       SYNASC 2016

              18th International Symposium on
   Symbolic and Numeric Algorithms for Scientific Computing
         September 24-27, 2016, Timisoara, Romania
               http://synasc.ro/2016

Aim
---

SYNASC aims to stimulate the interaction between the two scientific communities of symbolic and numeric computing and to exhibit interesting applications of the areas both in theory and in practice. The choice of the topic is motivated by the belief of the organizers that the dialogue between the two communities is very necessary for accelerating the progress in making the computer a truly intelligent aid for mathematicians and engineers.

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

10 June 2016          :  Abstract submission
22 June 2016          :  Paper submission (HARD DEADLINE)
27 July 2016          :  Notification of acceptance
15 August 2016        :  Registration
01 September 2016     :  Revised papers according to the reviews
24-27 September 2016  :  Symposium
30 November 2016      :  Final papers for post-proceedings


Invited Speakers
---------------

Erika Abraham, RWTH Aachen University, Germany
Chris Brown, U.S. Naval Academy
Dan Cristea, Alexandru Ioan Cuza University, Iasi, Romania
Tetsuo Ida, University of Tsukuba, Japan
Sorin Stratulat, University of Lorraine, France


Tracks
------

    * Symbolic Computation
        + computer algebra
        + symbolic techniques applied to numerics
        + hybrid symbolic and numeric algorithms
        + numerics and symbolics for geometry
        + programming with constraints, narrowing

    * Numerical Computing
        + iterative approximation of fixed points
        + solving systems of nonlinear equations
        + numerical and symbolic algorithms for differential equations
        + numerical and symbolic algorithms for optimization
        + parallel algorithms for numerical computing
        + scientific visualization and image processing

    * Logic and Programming
        + automatic reasoning
        + formal system verification
        + formal verification and synthesis
        + software quality assessment
        + static analysis
        + timing analysis

    * Artificial Intelligence
        + intelligent systems for scientific computing
        + recommender and expert systems for scientific computing
        + scientific knowledge management
        + agent-based complex systems modeling and development
        + uncertain reasoning in scientific computing    
        + computational intelligence
        + machine learning
        + data mining, text mining and web mining
        + natural language processing
        + computer vision
        + intelligent hybrid systems

    * Distributed Computing
        + parallel and distributed algorithms for clouds, GPUs, HPC, P2P systems, autonomous systems. Work should focus on scheduling, scaling, load balancing, networks, fault-tolerance, gossip algorithms, energy saving
        + applications for parallel and distributed systems, including work on cross disciplinary (scientific) applications for grids/clouds, web applications, workflow platforms, network measurement tools, programming environments
        + architectures for parallel and distributed systems, including self-managing and autonomous systems, negotiation protocols, HPC on clouds, GPU processing, PaaS for (inter)cloud, brokering platforms, mobile computing
        + modelling of parallel and distributed systems including models on resources and networks, semantic representation, negotiation, social networks, trace management, simulators
        + any other topic deemed relevant to the field

    * Advances in the Theory of Computing
       + Data Structures and algorithms
       + Combinatorial Optimization
       + Formal languages and Combinatorics on Words
       + Graph-theoretic and Combinatorial methods in Computer Science
       + Algorithmic paradigms, including distributed, online,
         approximation, probabilistic, game-theoretic algorithms
       + Computational Complexity Theory, including structural complexity, boolean complexity, communication complexity, average-case complexity, derandomization and property testing
       + Logical approaches to complexity, including finite model theory
       + Algorithmic and computational learning theory
       + Aspects of computability theory, including computability in
         analysis and algorithmic information theory
       + Proof complexity
       + Computational social choice and game theory
       + New computational paradigms: CNN computing, quantum,
         holographic and other non-standard approaches to Computability
       + Randomized methods, random graphs, threshold phenomena and
         typical-case complexity
       + Automata theory and other formal models, particularly in
         relation to formal verification methods such as model
         checking and runtime verification
       + Applications of theory, including wireless and sensor networks,
         computational biology and computational economics
       + Experimental algorithmics

This list is not intended to be exhaustive.   

Publication
--------------
Research papers that are accepted and presented at the symposium will be collected as post-proceedings published by Conference Publishing Service (CPS) (included in IEEE Xplore) and will be submitted for indexing in ISI Web of Science, DBLP, SCOPUS.

Extended versions of the selected papers published in post-proceedings will be considered to be published as special issues in international journals (e.g. Soft Computing Journal, Scalable Computing: Practice and Experience etc.)
 
Honorary Chairs
---------------
    * Bruno Buchberger, Johannes Kepler University, Austria
    * Stefan Maruster, West University of Timisoara, Romania

Steering Committee
------------------
    * Tetsuo Ida, University of Tsukuba, Japan
    * Tudor Jebelean, Johannes Kepler University, Austria
    * Viorel Negru, West University of Timisoara, Romania
    * Dana Petcu, West University of Timisoara, Romania
    * Stephen Watt, University of Western Ontario, Canada
    * Daniela Zaharie, West University of Timisoara, Romania

General Chairs
-------------
    * Viorel Negru, West University of Timisoara, Romania
    * Dana Petcu, West University of Timisoara, Romania

Program Chairs
-------------
    * James Davenport, University of Bath, UK
    * Daniela Zaharie, West University of Timisoara, Romania

Track Chairs
------------
    * Symbolic Computation
        + Tetsuo Ida, University of Tsukuba, Japan
        + Stephen Watt, University of Western Ontario, Canada
        + Manuel Kauers, Johannes Kepler University, Linz, Austria
        + Alin Bostan, INRIA, France

    * Numerical Computing
        + Stephen Takacs, Johannes Kepler University Linz, Austria
        + Eva Kaslik, West University of Timisoara, Romania

    * Logic and Programming
        + Nikolaj Bjorner, Microsoft Research, USA
        + Laura Kovacs, Chalmers University of Technology, Sweden
        + Tudor Jebelean, Johannes Kepler University Linz, Austria
     
    * Artificial Intelligence
        + Andrei Petrovski, Robert Gordon University, UK 
        + Daniela Zaharie, West University of Timisoara, Romania
 
    * Distributed Computing
        + Marc Frincu, West University of Timisoara, Romania
        + Karoly Bosa, Johannes Kepler University Linz, Austria
       
    * Advances in the Theory of Computing
        + Mircea Marin, West University of Timisoara, Romania
        + Gabriel Istrate, Institute e-Austria Timisoara, Romania
             
Special sessions and workshops chair
------------------------------------
    * Daniel Pop, West University of Timisoara, Romania

Tutorial chair
--------------
    * Florin Fortis, West University of Timisoara, Romania
           
Proceedings Chairs
------------------
    * James Davenport, University of Bath, UK 
    * Daniela Zaharie, West University of Timisoara, Romania
 
Local Committee Chairs
----------------------
    * Isabela Dramnesc, West University of Timisoara, Romania
    * Silviu Panica, Institute e-Austria Timisoara, Romania
    * Monica Tirea, West University of Timisoara, Romania
    * Mihail Gaianu, West University of Timisoara, Romania   

Submission
-----------
Submissions of research papers are invited. The papers must contain original research results not submitted and not published elsewhere.

The submission process consists of two steps.

    * In the first step the authors are invited to express their intention to participate at the conference by registering the title and a tentative abstract (1/2 page, at maximum) of their paper.

    * In the second step the authors should submit the full paper.

There are four categories of submissions:
    * Regular papers describing fully completed research results (up to 8 pages in the two-columns paper style).
    * System descriptions and experimental papers describing implementation results of experimental data, with a link to the reported results (up to 4 pages in the two-columns paper style).
    * Short papers, describing work in progress and/or preliminary results (up to 4 pages in the two-columns paper style).
    * Posters, describing ongoing work and research challenges of PhD students (up to 2 pages in the two-columns paper style).
 
Both the abstract and the full paper should be submitted electronically through http://www.easychair.org/conferences/?conf=synasc2016.


Workshops
---------

* Workshop on Agents for Complex Systems (ACSys)

* Workshop on Geoinformatics (GeoInfo)

* Workshop on HPC for Science and Technology (HPC-ST)

* Workshop on Iterative Approximation of Fixed Points (IAFP)

* Workshop on Management of resources and services in Cloud and Sky computing (MICAS)

* Workshop on Natural Computing and Applications (NCA)

The papers for workshops should be submitted through https://easychair.org/conferences/?conf=synasc2016workshops


* Workshop on Satisfiability Checking and Symbolic Computation (SC²)

The papers for this workshop should be submitted through https://easychair.org/conferences/?conf=scsquare2016


All papers accepted at workshops will be included in the local electronic proceedings and the best presented papers will be included in the post proceedings published by Conference Publishing Services.

Tutorials and trainings
-----------------------

* Tutorial in Monitoring of Big Data Applications

* Tutorial on HPC Cloud Services

* Training in HPC for Industrial Innovation

[the list is still open]


-----------
SYNASC 2016
West University of Timisoara
Department of Computer Science
Bd. V. Parvan 4, 300223 Timisoara, Romania
tel: + (40) 256 592195, +(40) 256 592389
fax: + (40) 256 592316, +(40) 256 592380
e-mail: synasc16 <at> info.uvt.ro
------------------------------------------------------------------------------
Mobile security can be enabling, not merely restricting. Employees who
bring their own devices (BYOD) to work are irked by the imposition of MDM
restrictions. Mobile Device Manager Plus allows you to control only the
apps on BYO-devices by containerizing them, leaving personal data untouched!
https://ad.doubleclick.net/ddm/clk/304595813;131938128;j
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Alexander Romanovsky | 19 May 07:38 2016
Picon
Picon

Call for papers: SERENE 2016, 5-6th September 2016, Gothenburg, Sweden

Call for papers
================================================================================
SERENE 2016
8th International Workshop on Software Engineering for Resilient Systems
5-6th September 2016, Gothenburg, Sweden
http://serene.disim.univaq.it/2016


Co-located with EDCC, the European Dependable Computing Conference
(http://www.cse.chalmers.se/edcc2016/)

================================================================================
Important Dates

Submission due: June 3rd, 2016
Authors notification: July 1th, 2016
Camera ready papers: July 15th, 2016
Workshop: September 5-6, 2016
================================================================================
Resilience is an ability of a system to persistently deliver trustworthy services despite changes. Modern
software systems continuously change in response to evolving requirements, customer feedback, new
business needs, platform upgrades etc. Despite frequent changes software is expected to function
correctly and reliably especially while providing services that are critical to society, e.g.,  in such
areas as
transportation, healthcare, energy production etc. Since modern software should be developed to
Efficiently cope with changes, unforeseen failures and intrusions,  design for resilience is becoming an
Increasingly important area of software engineering.

SERENE workshop has a long tradition of bringing together researchers and industry practitioners to
discuss advances in engineering resilient systems. Since 2015 SERENE has become a part of a major
European dependability forum –  EDCC, the European Dependable Computing Conference
(http://www.cse.chalmers.se/edcc2016/)


The SERENE 2016 workshop provides a forum for researchers and practitioners to exchange ideas on
advances in all areas relevant to software engineering for resilient systems, including, but not limited to:

Development of resilient systems
- Incremental development processes for resilient systems;
- Requirements engineering & re-engineering for resilience;
- Frameworks, patterns and software architectures for resilience;
- Engineering of self-healing autonomic systems;
- Design of trustworthy and intrusion-safe systems;
- Resilience at run-time (mechanisms, reasoning and adaptation);
- Resilience & dependability (resilience vs. robustness, dependable vs. adaptive systems).

Verification, validation and evaluation of resilience
  Modelling and model based analysis of resilience properties;
- Formal and semi-formal techniques for verification and validation;
- Experimental evaluations of resilient systems;    Quantitative approaches to ensuring resilience;
- Resilience prediction.

Case studies & applications
- Empirical studies in the domain of resilient systems;
- Methodologies adopted in industrial contexts;    Cloud computing and resilient service provisioning;
- Resilience for data-driven systems (e.g., big data-based adaption and resilience);
- Resilient cyber-physical systems and infrastructures;
- Global aspects of resilience engineering: education, training and cooperation.

================================================================================
Contributions

We welcome relevant contributions in the following forms:
- Technical papers describing original theoretical or practical work;
- Experience/Industry papers describing practitioner experience or field study, addressing an application
domain and the lessons learned;
- PhD Forum papers describing objectives, methodology, and results at an early stage in research;
- Project papers describing goals and results of ongoing projects;
- Tool papers presenting tools that support the development of resilient systems.

Submission
Papers can be submitted via EasyChair: https://www.easychair.org/conferences/?conf=serene2016

Each paper must be submitted in PDF and be formatted according to the Springer LNCS Guidelines:
http://www.springer.com/computer/lncs?SGWID=0-164-6-793341-0 be no longer than 15 pages for
technical and experience/industry papers, and 8 pages for all others.

Submitted papers must describe novel work and not be published elsewhere. All papers will be
peer-reviewed and assessed for relevance to the workshop topics, technical soundness, innovation,
scientific and presentation quality. Accepted papers must be presented by (one of) the author(s).

The Proceedings of SERENE 2016 will be published as a volume in Springer Lecture Notes in Computer
Science (LNCS).

================================================================================
Info

SERENE website: htttp://serene.disim.univaq.it
LinkedIn group: https://www.linkedin.com/groups?home=&gid=4365850&trk=my_groups-tile-grp

Slideshare: www.slideshare.net/SERENEWorkshop/


Program Chairs:
* Ivica Crnkovic , Chalmers U. of Technology and U. of Gothenburg, Sweden
* Elena A. Troubitsyna, Abo Akademi University

Program Committee
* Paris Avgeriou, U. Groningen, The Netherlands
* Marco Autili, University of L’Aquila, Italy
* Iain Bate, University of York, UK
* Didier Buchs, U. Geneva, Switzerland
* Barbora Buhnova, Masaryk University, Czech Republic
* Tomas Bures, Charles University, Czech Republic
* Andrea Ceccarelli, U. Firenze, Italy
* Vincenzo De Florio, U. Antwerp, Belgium
* Nikolaos Georgantas, INRIA, France
* Anatoliy Gorbenko, KhAI, Ukraine
* David De Andres, Universidad Politecnica de Valencia
* Felicita Di Giandomenico, CNR-ISTI, Italy
* Holger Giese, U. Potsdam, U. Potsdam, Germany
* Nicolas Guelfi, U. Luxembourg, Luxembourg
* Alexei Iliasov, Newcastle U., UK
* Kaustubh Joshi, At&T, USA
* Mohamed Kaaniche, LAAS-CNRS, France
* Zsolt Kocsis , IBM, Hungary
* Linas Laibinis, bo Akademi U., Finland
* Nuno Laranjeiro, U. Coimbra, Portugal
* Istvan Majzik, Budapest University of Technology and Economics, Hungary
* Paolo Masci, Queen Mary U., UK
* Marina Mongiello, Technical University of Bari, Italy
* Henry Muccini, U. L’Aquila, Italy
* Sadaf Mustafiz, McGill U., Canada
* Andras Pataricza, Budapest University of Technology and Economics, Hungary
* Patrizio Pelliccione,  Chalmers University of Technology, Sweden
* Nadia Polikarpova
* Markus Roggenbach, Swansea University, UK
* Alexander Romanovsky, Newcastle U., UK
* Stefano Russo, U. Naples Federico II, Italy
* Peter Schneider-Kamp, U. Southern Denmark, Denmark
* Marco Vieira, University of Coimbra, Portugal
* Katinka Wolter, Freie U. Berlin, Germany
* Apostolos Zarras, U. Ioannina, Greece

================================================================================
Info
SERENE website: htttp://serene.disim.univaq.it
LinkedIn group: https://www.linkedin.com/groups?home=&gid=4365850&trk=my_groups-tile-grp

Slideshare: www.slideshare.net/SERENEWorkshop/

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


************************************************************************

To remove your name from laas-dependability-announce email list, simply
send a message to sympa <at> laas.fr with the words 
"UNSubscribe laas-dependability-announce" 
in the subject line. If you encounter a problem, please contact laas-dependability-announce-owner <at> laas.fr

************************************************************************
------------------------------------------------------------------------------
Mobile security can be enabling, not merely restricting. Employees who
bring their own devices (BYOD) to work are irked by the imposition of MDM
restrictions. Mobile Device Manager Plus allows you to control only the
apps on BYO-devices by containerizing them, leaving personal data untouched!
https://ad.doubleclick.net/ddm/clk/304595813;131938128;j
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Alexander Romanovsky | 10 May 15:22 2016
Picon
Picon

CfPart: Int. Conference on Reliability, Safety and Security of Railway Systems

International Conference on 
Reliability, Safety and Security of Railway Systems: 
Modelling, Analysis, Verification and Certification
http://conferences.ncl.ac.uk/rssrail/ 

28-30 June 2016
Espace du Centenaire, Maison de la RATP, Paris, France

Call for Participation

Conference Aims:
* to bring together researchers and developers
* to ensure that advances in research are driven by the real needs of the railway
* to help develop technology that is usable, scalable and deployable
* to support the provision and utilisation of advanced methods and tools
* to present novel methods for modelling, analysis, verification and validation
* to identify mechanisms and procedures which support evidence cases 
that standards are being met

Challenges:
* to improve railway system safety, security and reliability
* to reduce production cost, time to market and running costs
* to increase system capacity and reduce carbon emissions

Context:
* integration of railway systems into larger multi-mode transport networks
* dramatic increases in the complexity of railway applications
* ever higher degree of automation

The conference will feature three invited keynote talks, from eminent 
and experienced investigators:

Robin Bloomfield, Adelard LLP and City University London (UK)
The risk assessment of ERTMS based railway systems from a cyber perspective:
methodology and lessons learnt

Denis Sabatier, ClearSy (France)
Using formal proof and B method at system level for industrial projects

Jan Peleska, University of Bremen and Verified Systems (Germany)
A novel approach to HW/SW integration testing of route-based interlocking 
system controllers

And the invited presentation by Claude Andlauer, Head of Rail Transport for RATP (France)
Formal methods as part of RATP’s DNA

Specific topics to be presented at RSSRail 2016 will include:
* failure analysis, 
* interlocking verification, 
* formal system specification and refinement, 
* security analysis of ERTMS, 
* safety verification,  
* formalisation of requirements, 
* proof automation,
* operational security, 
* railway system reliability, 
* risk assessment for ERTMS, 
* verification of EN-50128 safety requirements.

For more details on the keynote talks, the individual papers and the posters to be 
presented, please visit the website: http://conferences.ncl.ac.uk/rssrail/programme/

The proceedings are published by Springer.

Registration: http://conferences.ncl.ac.uk/rssrail/registration/

------------------------------------------------------------------------------
Mobile security can be enabling, not merely restricting. Employees who
bring their own devices (BYOD) to work are irked by the imposition of MDM
restrictions. Mobile Device Manager Plus allows you to control only the
apps on BYO-devices by containerizing them, leaving personal data untouched!
https://ad.doubleclick.net/ddm/clk/304595813;131938128;j
Walther Neuper | 25 May 08:28 2016
Picon

ThEdu at CICM'16 deadline approaching

Te deadline for extended abstracts is approaching ...
=======================================================================
                            ThEdu'16
         Theorem Prover Components for Educational Software
            http://www.uc.pt/en/congressos/thedu/thedu16
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
                          at CICM 2016
          Conferences on Intelligent Computer Mathematics
               July 25-29, 2016, Bialystok, Poland
               http://www.cicm-conference.org/2016
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

Scope:

 Educational software tools have technologies integrated from CAS, from
DGS, from Spreadsheets and others, but not from (Computer) Theorem
Provers (TPs) with few exceptions: the latter have been developed to
model mathematical reasoning in software -- rigorous reasoning as a
companion of calculating, which guarantees the unsurpassed reliability
of mathematics. Providing students with insight in and experience with
this kind of reliability is considered an essential aim of mathematics
education.

 TPs intrude into science as well as into industry: They are used to
tackle difficult proofs in the science of mathematics, like the Four
Color Theorem or the Kepler Conjecture. In industry TPs are successfully
used to verify safety critical software. This workshop addresses a
window of opportunity during the still open development of TPs.

 The workshop provides a meeting place for educators and developers of
educational mathematics software and experts in TP. The discussions
shall clarify the requirements of education, identify advantages and
promises of TP for learning and motivate development of such a novel
kind of educational mathematical tools.

Important Dates

    * Extended Abstracts:    4. June 2016
    * Author Notification:  18. June 2016
    * Final Version:         2. July 2016
    * Workshop Day:         25-29. July 2016

Points of interest include:

  * Adaption of TP -- concepts and technologies for education: knowledge
    representation, simplifiers, reasoners; undefinednes, level of
    abstraction, etc.
  * Requirements on software support for reasoning -- reasoning appears
    as the most advanced method of human thought, so at which age
    which kind of support TP should be provided?
  * Automated TP in geometry -- relating intuitive evidence with logical
    rigor: specific provers, adaption of axioms and theorems, visual
    proofs, etc.
  * Application of TP components in SW for engineers -- Formal Methods
    increasingly advance into engineering practice, so educational
    software based on TP components could anticipate that advancement.
  * Levels of authoring -- in order to cope with generality of TP:
    experts adapt to specifics of countries or levels, teachers adapt
    to courses and students.
  * Adaptive modules, students modeling and learning paths -- services
    for user guidance provided by TP technology: which interfaces
    enable flexible generation of adaptive user guidance?
  * Next-step-guidance -- suggesting a next step when a student gets
    stuck in problem solving: which computational methods can extend
    TP for that purpose?
  * TP as unifying foundation -- for the integration of technologies
    like CAS, DGS, Spreadsheets etc: interfaces for unified support of
    reasoning?
  * Continuous tool chains -- for mathematics education from high-school
    to university, from algebra and geometry to graph theory etc.

Submission

  We welcome submission of extended abstracts and demonstration
  proposals presenting original unpublished work which is not been
  submitted for publication elsewhere.
    All accepted extended abstracts and demonstrations will be presented
  at the workshop. The extended abstracts will be made available
  online.
    Contributions should be submitted via THedu'16 easychair
  https://www.easychair.org/conferences/?conf=thedu16.
    Extended abstracts and demonstration proposals should be no more
  than 4 pages in length and are to be submitted in PDF format. They
  must conform to the EPTCS style guidelines (http://style.eptcs.org/).
    At least one author of each accepted extended abstract/demonstration
  proposal is expected to attend THedu'15 and presents his/her extended
  abstract/demonstration. Joint publication in companion with other CICM
  events is under consideration (e.g. http://ceur-ws.org/).

Program Committee

  Francisco Botana, University of Vigo at Pontevedra, Spain
  Roman Hašek, University of South Bohemia, Czech Republic
  Filip Maric, University of Belgrade, Serbia
  Walther Neuper, TUG University of Technology, Austria (co-chair)
  Pavel Pech, University of South Bohemia, Czech Republic
  Pedro Quaresma, University of Coimbra, Portugal (co-chair)
  Vanda Santos, CISUC, Portugal
  Wolfgang Schreiner, Johannes Kepler University, Austria
  Burkhart Wolff, University Paris-Sud, France

------------------------------------------------------------------------------
Mobile security can be enabling, not merely restricting. Employees who
bring their own devices (BYOD) to work are irked by the imposition of MDM
restrictions. Mobile Device Manager Plus allows you to control only the
apps on BYO-devices by containerizing them, leaving personal data untouched!
https://ad.doubleclick.net/ddm/clk/304595813;131938128;j
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Gmane