Andreas Lochbihler | 15 Apr 15:57 2014
Picon

Two PhD positions in Information Security at ETH Zurich, Switzerland

The Information Security group headed by Prof. David Basin at ETH
Zurich has two open PhD positions in two projects:

(1) Formalizing computational soundness for protocol implementations
(2) Testing access control systems

We are looking for enthusiastic outstanding researchers with a strong
background and interest in one or more of the following areas:

- formal methods or mathematical logic,
- information security or cryptography,
- (project 1) interactive theorem proving
   (project 2) software testing.

Candidates with a strong theoretical background in related areas are
also encouraged to apply. ETH Zurich regulations require PhD
candidates to hold a Masters or equivalent degree (e.g. Diplom). The
preferred starting date for both positions is as soon as possible, at
the latest by the end of 2014.

Description of the projects:

(1) Formalizing computational soundness for protocol implementations,
     funded by the Swiss National Science Foundation

The project aims at a better understanding of, and more confidence in,
the security guarantees offered by symbolic analysis methods for
security protocols, e.g. TLS and IPsec. To this end, symbolic and
computational models of security protocols and security properties
will be formalized in the proof assistant Isabelle/HOL and linked with
(Continue reading)

Ramana Kumar | 15 Apr 08:30 2014
Picon
Picon

INT_OF_NUM conversion

I'm about to write a conversion to reduce terms of the form Num(&n) where n is a ground non-negative integer. But I would expect such a thing to already exist somewhere - does anyone know where?

I notice that EVAL does not reduce Num(&1) - is there something I can load that will make it do so?
------------------------------------------------------------------------------
Learn Graph Databases - Download FREE O'Reilly Book
"Graph Databases" is the definitive new guide to graph databases and their
applications. Written by three acclaimed leaders in the field,
this first edition is now available. Download your free book today!
http://p.sf.net/sfu/NeoTech
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Wendelin Serwe | 14 Apr 11:47 2014
Picon
Picon

FMICS 2014: submission still open

############################################################################
LAST CALL FOR PAPERS

FMICS 2014
19th International Workshop on
Formal Methods for Industrial Critical Systems
(http://fmics2014.unifi.it)

11-12 September 2014, Florence, Italy

In co-location with EPEW, FORMATS, QEST, and SAFECOMP
(http://florence2014.org/conferences.html)

############################################################################

The aim of the FMICS workshop series is to provide a forum for researchers who 
are interested in the development and application of formal methods in 
industry. In particular, FMICS brings together scientists and engineers that 
are active in the area of formal methods and interested in exchanging their 
experiences in the industrial usage of these methods. The FMICS workshop 
series also strives to promote research and development for the improvement of 
formal methods and tools for industrial applications.

Important Dates

     Paper submission: April 18th
     Notification: June 10th
     Final version due: June 27th
     Workshop: September 11th-12th

Topics of interest include (but are not limited to):

     Design, specification, code generation and testing based on formal methods.
     Methods, techniques and tools to support automated analysis, 
certification, debugging, learning, optimization and transformation of 
complex, distributed, real-time systems and embedded systems.
     Verification and validation methods that address shortcomings of existing 
methods with respect to their industrial applicability (e.g., scalability and 
usability issues).
     Tools for the development of formal design descriptions.
     Case studies and experience reports on industrial applications of formal 
methods, focusing on lessons learned or identification of new research directions.
     Impact of the adoption of formal methods on the development process and 
associated costs.
     Application of formal methods in standardization and industrial forums.

Paper Submission

Submissions must describe authors' original research work and results. 
Submitted papers must not have previously appeared in a journal or conference 
with published proceedings and must not be concurrently submitted to any other 
peer-reviewed workshop, symposium, conference or archival journal. Any partial 
overlap with any such published or concurrently submitted paper must be 
clearly indicated.

Submissions should clearly demonstrate relevance to industrial application. 
Case study papers should identify lessons learned, validate theoretical 
results (such as scalability of methods), or provide specific motivation for 
further research and development.

Submissions should not exceed 15 pages formatted according to the LNCS style 
(Springer), and should be submitted as Portable Document Format (PDF) files 
using the EasyChair submission site.

All submissions will be reviewed by the program committee who will make a 
selection among the submissions based on the novelty, soundness and 
applicability of the presented ideas and results. The proceedings of the 
workshop will be published in the Springer series Lecture Notes in Computer 
Science (LNCS). An USB stick with an electronic version of the proceedings 
will be distributed among participants during the workshop.

Participants will give a presentation of their papers in twenty minutes, 
followed by a ten-minute round of questions and discussion on participants' work.

Following the tradition of the past editions, a special issue of the journal 
Science of Computer Programming will be devoted to FMICS 2014.
Selected participants will be invited to submit an extended version of their 
papers after the workshop. These extended versions will again be reviewed by a 
program committee, which will decide on their final publication on the special 
issue.

Programme Committee

PC Chairs

     Francesco Flammini (Ansaldo STS, Italy)
     Frédéric Lang (Inria & LIG, France)

Publicity Chair

     Wendelin Serwe (Inria & LIG, France)

PC Members

     Maria Alpuente (Universitat Politècnica de València, Spain)
     Alvaro Arenas (IE University, Spain)
     Jiri Barnat (Masaryk University, Czech Republic)
     Cinzia Bernardeschi (University of Pisa, Italy)
     Simona Bernardi (Centro Universitario de la Defensa, AGM, Zaragoza, Spain)
     Jean Paul Blanquart (Astrium Satellites, France)
     Eckard Böde (Offis, Germany)
     Rocco De Nicola (IMT Lucca, Italy)
     Michael Dierkes (Rockwell Collins, France)
     Susanna Donatelli (University of Torino, Italy)
     Cindy Eisner (IBM Research - Haifa, Israel)
     Alessandro Fantechi (Università di Firenze, Italy)
     Jérôme Feret (CNRS & ENS & Inria, France)
     Wan Fokkink (Vrije Universiteit Amsterdam and CWI, Netherlands)
     Andrew Gacek (Rockwell Collins, USA)
     Stefania Gnesi (ISTI-CNR, Italy)
     Matthias Güdemann (Systerel, France)
     Keijo Heljanko (Aalto University, Finland)
     Jan Jürjens (TU Dortmund & Fraunhofer ISST, Germany)
     Tiziana Margaria (University of Potsdam, Germany)
     Pedro Merino (University of Málaga, Spain)
     Benjamin Monate (TrustInSoft, France)
     Gethin Norman (University of Glasgow, UK)
     Dave Parker (University of Birmingham, UK)
     Charles Pecheur (Université catholique de Louvain, Belgium)
     Ralf Pinger (Siemens AG, Germany)
     Wendelin Serwe (Inria & LIG, France)
     Hans Svensson (Quviq, Sweden)
     Jaco van de Pol (University of Twente, Netherlands)
     Valeria Vittorini (University of Naples Federico II, Italy)
     Angela Vozella (CIRA, Italy)

------------------------------------------------------------------------------
Learn Graph Databases - Download FREE O'Reilly Book
"Graph Databases" is the definitive new guide to graph databases and their
applications. Written by three acclaimed leaders in the field,
this first edition is now available. Download your free book today!
http://p.sf.net/sfu/NeoTech
Lina Ye | 14 Apr 17:00 2014
Picon
Picon

Call for Papers: Workshops Colocated with SEFM 2014

Our apologies if you have received multiple copies.


####################################################################


CALL FOR PAPERS

Five Workshops Colocated with SEFM 2014


Grenoble, France
September 1-2, 2014

http://sefm2014.inria.fr/


####################################################################


WEB SITES AND IMPORTANT DATES


- 1st Workshop on Human-Oriented Formal Methods: From Readability to Automation

This workshop aims to bring together researchers, engineers and practitioners 
from academia and industry to baseline the state of the art in the increasingly 
important domain: applications of human factors to the analysis and to the 
optimization of formal methods area. It also aims to develop a future vision 
and roadmap of usability and automation, focusing especially on readability 
and ease of use. 

For more details please see http://hofm2014.wordpress.com/


Paper Submission: 10 June, 2014
Notification of Acceptance: 5 July, 2014
Post-proceedings Final version: 15 September 2014
Workshop Date: 1 September, 2014


--------------------------------------------------------------------------------


- 3rd International Symposium on Modelling and Knowledge Management 
applications: Systems and Domains

The aim of the Symposium is to bring together practitioners and
researchers from academia, industry, government and non-government
organisations to present research results and exchange experience,
ideas, and solutions for modelling and analysing complex systems
and using knowledge management strategies, technology and systems
in various domain areas (e.g., ecology, biology, medicine, climate, 
economy, governance, education and social software engineering) 
that address problems of sustainable development.


For more details please see http://www.di.unipi.it/mokmasd/symposium-2014/index.html


Paper Submission: 6 June 2014
Notification of Acceptance: 5 July 2014
Pre-proceedings Final version: 31 July 2014
Post-proceedings Final version: 15 September 2014
Symposium Date: 2 September 2014


-------------------------------------------------------------------------------


- 8th International Workshop on Foundations and Techniques for Open 
Source Software Certification


The aim of this workshop is to bring together researchers from Academia 
and Industry who are broadly interested in 1) the quality assessment of 
the open source software projects, and 2) metrics, procedures, and tools 
that could be useful in assessing and qualifying individual participation 
and collaboration patterns in the open source software communities.


For more details please see http://www.di.unipi.it/opencert/workshop-2014/


Paper Submission: 6 June 2014
Notification of Acceptance: 11 July 2014
Notification of Early Registration: 15 July 2014
Pre-proceedings Final version: 31 July 2014
Post-proceedings Final version: 15 September 2014
Workshop Date: 1 September 2014


-------------------------------------------------------------------------------


- 1st Workshop on Safety and Formal Methods


Formal methods have traditionally been advocated for improving the reliability 
of safety-relevant systems. The SaFoMe workshop aims to provide a forum for 
people from academia and industry to communicate their latest results on 
theoretical advances, industrial case studies, and lessons learned in the 
application of formal methods to safety certification, verification and/or 
validation in (but not limited to) component-based systems.


For more details please see http://babel.ls.fi.upm.es/safome2014/


Abstract Submission: 23 May, 2014
Paper Submission: 30 May, 2014
Notification of Acceptance: 30 June, 2014
Camera-ready Paper Due: 15 July, 2014
Registration deadline: 15 July, 2014
Workshop Date: 1 September, 2014


-----------------------------------------------------------------------------------


- 4th Workshop on Formal Methods in the Development of Software


The aim of WS-FMDS is to bring together scientists and practitioners who are 
active in the area of formal methods and interested in exchanging their 
experiences in the industrial usage of these methods. This workshop also 
strives to promote research and development for the improvement of theoretical 
aspects of formal methods and tools focused on practical usability for 
industrial applications.


For more details please see http://antares.sip.ucm.es/ws-fmds2014/


Paper Submission: 23 May, 2014
Notification of Acceptance: 9 June, 2014
Camera-ready Paper Due: 20 June, 2014
Workshop Date: 1-2 September, 2014


####################################################################


PUBLICATION


All accepted papers will be published by Springer in a volume of LNCS.
Condition for inclusion in the post-proceedings is that at least one
of the co-authors has presented the paper at the workshop.

------------------------------------------------------------------------------
Learn Graph Databases - Download FREE O'Reilly Book
"Graph Databases" is the definitive new guide to graph databases and their
applications. Written by three acclaimed leaders in the field,
this first edition is now available. Download your free book today!
http://p.sf.net/sfu/NeoTech
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Ramana Kumar | 14 Apr 16:16 2014
Picon
Picon

list_compset behaviour on EXISTS

I find this very counterintuitive:

> load"listLib";
val it = (): unit
> computeLib.CBV_CONV (listLib.list_compset()) ``EXISTS P []``;
<<HOL message: inventing new type variable names: 'a>>
val it = |- EXISTS P [] ⇔ EXISTS P []: thm

whereas:

> EVAL ``EXISTS P []``;
<<HOL message: inventing new type variable names: 'a>>
val it = |- EXISTS P [] ⇔ F: thm

I also don't understand why it is happening.
Based on how list_compset is defined, it should reduce the term like EVAL does.

Any ideas?
------------------------------------------------------------------------------
Learn Graph Databases - Download FREE O'Reilly Book
"Graph Databases" is the definitive new guide to graph databases and their
applications. Written by three acclaimed leaders in the field,
this first edition is now available. Download your free book today!
http://p.sf.net/sfu/NeoTech
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Peter Höfner | 11 Apr 08:45 2014
Picon

ATVA - (Final) Call for Workshop Proposals


                     ATVA 2014
          CALL FOR WORKSHOP PROPOSALS

12th International Symposium on Automated Technology for
           Verification and Analysis

        November 3-7, 2014, Sydney, Australia
             http://atva-conferences.org

Extended Deadline for proposal submissions:   April 29, 2014

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

The 12th International Symposium on Automated Technology for
Verification and Analysis (ATVA) invites proposals for pre-
and postconference workshops to be held on November 3 (pre)
or November 7 (post). The ATVA conference series covers the
spectrum from theoretical results to practical applications
of automated analysis, verification and synthesis.

Proposals that promise to bring new topics to ATVA, of either
practical or theoretical importance, or to provide a forum for more
detailed discussion on central topics of continuing importance
are highly welcome. Proposals that explore the application of
automated tools to real-world problems are especially encouraged.

Workshop proposals are limited to 2 pages, and should provide at
least the following information:
 - Title
 - Description of the workshop topic and goals
   (Why do you believe this is an interesting and significant topic?)
 - Intended audience
   (From which areas do you expect potential participants to
    come? How many participants do you expect?)
 - Relevance and relation of the workshop to the main conference
 - Organisation of the workshop
   (Describe the intended format (e.g. paper selection process),
    its expected duration (full day or half day) and its preferred
    date (November 3rd or November 7th)
 - Organisers' details
   (Provide affiliations, backgrounds and contact details of
   organisers and potential committee members)

Proposals should be sent as PDF to the workshop chair Peter Höfner
(peter.hoefner <at> nicta.com.au).

Important dates:
  Deadline for proposal submissions:   April 29, 2014  (extended)
  Acceptance/rejection notification:   May 19, 2014
  Workshop Date:                       November 3rd and 7th

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

________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or
copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

------------------------------------------------------------------------------
Put Bad Developers to Shame
Dominate Development with Jenkins Continuous Integration
Continuously Automate Build, Test & Deployment 
Start a new project now. Try Jenkins in the cloud.
http://p.sf.net/sfu/13600_Cloudbees
Klaus Havelund | 10 Apr 09:16 2014
Picon
Picon

[fm-announcements] RV 2014, Deadlines extended: abstract April 18, full paper April 25

[DEADLINES EXTENDED]

[Apologizes for duplicates]

14th International Conference on
Runtime Verification
September 22 – 25, 2014
Toronto, Canada

http://rv2014.imag.fr/

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
  • 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 safety/mission-critical systems, enterprise and systems software, autonomous and reactive control systems, health management and diagnosis systems, and system security and privacy.

 

Technical Research Papers Track:

Technical research papers can be submitted in two categories: regular and short papers. Papers in both categories will be reviewed by the conference Program Committee. All accepted technical papers will appear in an LNCS volume. Submitted papers must use the LNCS style. At least one author of each accepted paper must attend RV’14 to present the paper. Papers must be submitted electronically using the EasyChair system.

  • Regular papers (up to 15 pages) should present original unpublished results. Theoretical and experimental papers as well as papers on applications of runtime verification and case studies are all welcome. A non-monetary Best Paper Award will be given. 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 5 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 short talk (10 minutes) and poster sessions.
 

Program committee

Borzoo Bonakdarpour (University of Waterloo, Canada), co-chair

Scott Smolka (Stony Brook Universtiy, USA), co-chair

 

Gul Agha (University of Illinois at Urbana-Champaign, USA)

Thomas Ball (Microsoft Research, Redmond, USA)

Howard Barringer (The University of Manchester, UK)

Ezio Bartocci (TU Wien, Austria)

David Basin (ETH Zurich, Switzerland)

Saddek Bensalem (Verimag, France)

Ivona Brandic (TU Wien, Austria)

Marsha Chechik (University of Toronto, Canada)    

Michael Clarkson (George Washington University, USA)

Laura Dillon (Michigan State University, USA)

Shlomi Dolev (Ben Gurion University, Israel)

Alastair Donaldson (Imperial College London, UK)

Dawson Engler (Stanford University, USA)                 

Ylies Falcone (Université Joseph Fourier, France)

Vijay Garg (University of Texas at Austin, USA)

Steve Goddard (University of Nebraska-Lincoln, USA)

Ganesh Gopalakrishnan (University of Utah, USA)

Wolfgang Grieskamp (Google, USA)

Radu Grosu (TU- Wien, Austria)

Klaus Havelund (NASA/JPL, USA)

Mats Heimdahl (University of Minnesota, USA)

Laurie Hendren (McGill University, Canada)

Gerard Holzmann (NASA/JPL, USA)

Daniel Keren (Haifa University, Israel)

Sandeep Kulkarni (Michigan State University, USA)

Marta Kwiatkowska (University of Oxford, UK)

Insup Lee (University of Pennsylvania, USA)             

Axel Legay (IRISA/INRIA, France)

Martin Leucker (University of Lübeck, Germany)

Leonardo Mariani (University of Milano Bicocca, Italy)

Patrick Meredith (University of Illinois at Urbana-Champaign, USA)

David Naumann (Stevens Institute of Technology, USA)

Doron Peled (Bar Ilan University, Israel)

Mauro Pezze (University of Lugano, Switzerland)

Lee Pike (Galois Inc., USA)

Zvonimir Rakamaric (University of Utah, USA)

Grigore Rosu (University of Illinois at Urbana-Champaign, USA)

Andrey Rybalchenko (TU-Munich, Germany)

Andre Schiper (EPFL, Switzerland)

Oleg Sokolsky (University of Pennsylvania, USA)

Scott Stoller (Stony Brook University, USA)

Serdar Tasiran (Koc University, Turkey)

Michael Whalen (University of Minnesota, USA)

Lenore Zuck (University of Illinois at Chicago, USA)

 

Tool Demonstrations Track:

The aim of the RV 2014 tool demonstration 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. Tool demonstration papers will be reviewed by the Tools Track Program Committee. All accepted tool demonstration papers will appear in the conference proceedings LNCS volume. Submitted papers must use the LNCS style. At least one author of each accepted paper must attend RV’14 to present the paper. Papers must be submitted electronically using the EasyChair system.

Tool papers should meet the following criteria:

  • A tool paper should present a new tool, a new tool component or novel extensions to existing tools supporting runtime verification. Each submission should be original and not published previously in a tool paper form.
  • Each submission must not exceed 8 pages in the LNCS/Springer proceeding format, including all text, references and figures. The paper must be written in English and provided in PDF format.
  • Each submission must be accompanied at the time of the submission by a short screencast (between 5-10 minutes), with voice and overlay text commentary illustrating the demonstration of the tool (a link to it should be provided in the paper).
  • The paper 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.
  • Each tool paper must 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.
 

Evaluation

Each submission will be reviewed by at least four members of the tool demonstration track program committee. The evaluation criteria will include:

  • the presentation quality
  • the availability (possibly in a open-source format) of the software.
  • the relevance for the Runtime Verification audience
  • the technical soundness of the presented tool
  • the originality of the underlying ideas
 

Tool Demonstration Committee

Ezio Bartocci, (TU-Vienna, Austria), chair
Alastair Donaldson (Imperial College London, UK)
Dawson Engler (Stanford University, USA)
Yliès Falcone (Université Joseph Fourier, France)
Klaus Havelund (NASA/JPL, USA)
Michael Whalen (University of Minnesota, USA)

 

Important Dates:

Both research papers and tool demonstration tracks will follow the following timeline:

  • Abstract deadline: April 18, 2014 (extended)
  • Full paper deadline: April 25, 2014 (extended)
  • Rebuttal phase: May 18-20, 2014
  • Acceptance notification: June 10, 2014
  • Camera ready submission: June 25, 2014
  • Conference dates: 22-25 September, 2014

---
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 
------------------------------------------------------------------------------
Put Bad Developers to Shame
Dominate Development with Jenkins Continuous Integration
Continuously Automate Build, Test & Deployment 
Start a new project now. Try Jenkins in the cloud.
http://p.sf.net/sfu/13600_Cloudbees
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Natarajan Shankar | 10 Apr 08:19 2014

Fourth Summer School on Formal Techniques, May 19-23, 2014, Menlo College, Atherton

Fourth Summer School on Formal Techniques
May 19 - May 23, 2014
Menlo College, Atherton, CA
http://fm.csl.sri.com/SSFT14

Techniques based on formal logic, such as model checking,
satisfiability, static analysis, and automated theorem proving, are
finding a broad range of applications in modeling, analysis,
verification, and synthesis.  This school, the fourth in the series,
will focus on the principles and practice of formal techniques, with a
strong emphasis on the hands-on use and development of this
technology.  It primarily targets graduate students and young
researchers who are interested in developing and using formal
techniques in their research.  Participants at the school will have a
seriously fun time experimenting with the tools and techniques
presented in the lectures during laboratory sessions.

The lecturers at the school include:
* Nikolaj Bjorner (MSR Redmond): Software verification with SMT.
* Veronique Cortier (LORIA, France): Formal analysis of security protocols:
                                         Models, Techniques, and Tools
* Gerard Holzmann (JPL/Caltech): Verifying Safety Critical Code
* Gerwin Klein (NICTA Australia): Programming language semantics in Isabelle
* Marta Kwiatkowska (University of Oxford): Probabilistic model checking 
with PRISM
* Natarajan Shankar (SRI CSL): Speaking Logic

We have NSF funding to support travel and accommodation for students
from US universities, but welcome applications from non-US students as
well.  Non-US students will be charged around $500 for meals and
lodging.  Applications should be submitted at
http://fm.csl.sri.com/SSFT14

Applicants are encouraged to submit their applications before April
30, 2014, since there are only a limited number of spaces available.
Non-US applicants requiring US visas are urged to apply early.

Information about the first three Summer Schools on Formal Techniques 
can be found at
   http://fm.csl.sri.com/SSFT11
   http://fm.csl.sri.com/SSFT12
   http://fm.csl.sri.com/SSFT13

------------------------------------------------------------------------------
Put Bad Developers to Shame
Dominate Development with Jenkins Continuous Integration
Continuously Automate Build, Test & Deployment 
Start a new project now. Try Jenkins in the cloud.
http://p.sf.net/sfu/13600_Cloudbees
Adnan Rashid | 10 Apr 07:23 2014
Picon

How to remove Hilbert choice operator

Dear all,

I am working in HOL-Light. I am having an equation and on the right side of equation, I am having Hilbert choice operator ( <at> ). How to remove this Hilbert choice operator. In the result of that, can I get an existential quantifier.

--
Regards:
Adnan
------------------------------------------------------------------------------
Put Bad Developers to Shame
Dominate Development with Jenkins Continuous Integration
Continuously Automate Build, Test & Deployment 
Start a new project now. Try Jenkins in the cloud.
http://p.sf.net/sfu/13600_Cloudbees
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
SYNASC 2014 | 10 Apr 09:23 2014
Picon

[5 days left for abstract submission] CFP Synasc 2014

[Please post - apologies for multiple copies.]

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

                       SYNASC 2014

              16th International Symposium on
   Symbolic and Numeric Algorithms for Scientific Computing
         September 22-25, 2014, Timisoara, Romania
           	  http://synasc.ro/2014/
	      http://synasc14.info.uvt.ro/

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
---------------

15 April 2014          :  Abstract submission  
30 April 2014          :  Paper submission 
15 July 2014           :  Notification of acceptance
01 September 2014      :  Registration
05 September 2014      :  Revised papers according to the reviews
22-25 September 2014   :  Symposium
30 November 2014       :  Final papers for post-proceedings

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
        + methods for hard computational problems
        + intelligent systems for scientific computing
        + agent-based complex systems modeling and development
        + scientific knowledge management
        + computational intelligence 
        + machine learning 
        + recommender and expert systems for scientific computing
        + data mining and web mining
        + natural language processing  
        + uncertain reasoning in scientific computing       
        + 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.   

Workshops
---------

    * Workshop on Agents for Complex Systems (ACSys)
           http://synasc.ro/2014/workshops/acsys-2014 
    * Workshop on Computational Topology in Image Context (CTIC)
           http://ctic2014.synasc.ro/index.html
    * Workshop on HPC research services (HPCReS)
           http://host.hpc.uvt.ro/events/hpcres-2014-international-workshop-on-hpc-research-services/ 
    * Workshop on GIC and Hydrologic Modeling (HydroGIS)    
           http://synasc.ro/2014/workshops/hydrogis-2014
    * Workshop on Iterative Approximation of Fixed Points (IAFP)
           http://synasc.ro/2014/workshops/iafp-2014
    * Workshop on Management of Resources and Services in Cloud and Sky Computing (MICAS)
           http://amicas.hpc.uvt.ro/micas-2014
    * Workshop on Natural Computing and Applications (NCA)
           http://synasc.ro/2014/workshops/nca-2014

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 considering to be published as special issues in international journals.

Invited Speakers 
----------------
    * Viorica Sofronie-Stokkermans, University Koblenz-Landau, Germany
    * Gheorghe Paun, Institute of Mathematics of the Romanian Academy, Bucharest, Romania
    * William Langdon, University College London, UK
    * Stefan Takacs, TU Chemnitz, Germany
    * Stephen Watt, University of Western Ontario, Canada

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 Chair
-------------
    * Viorel Negru, West University of Timisoara, Romania

Program Chair
-------------
    * Franz Winkler, Johannes Kepler University, Austria

Track Chairs
------------
    * Symbolic Computation
        + Tetsuo Ida, University of Tsukuba, Japan
        + Stephen Watt, University of Western Ontario, Canada

    * Numerical Computing
        + Richard Liska, Technical University of Prague, Czech Republic
        + Dana Petcu, West University of Timisoara, Romania

    * Logic and Programming
        + Tudor Jebelean, Johannes Kepler University Linz, Austria
        + Laura Kovacs, Chalmers University of Technology, Sweden

    * Artificial Intelligence
        + Andrei Petrovski, Robert Gordon University, UK	
        + Daniela Zaharie, West University of Timisoara, Romania

    * Distributed Computing
        + Marc Frincu, University of Southern California, US and 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, Research Institute e-Austria Timisoara, Romania

Special sessions and workshops chair
------------------------------------
    * Daniel Pop, West University of Timisoara, Romania

Tutorial chair
--------------
    * Dana Petcu, West University of Timisoara, Romania

Proceedings Chairs
------------------
    * Franz Winkler, Johannes Kepler University Linz, Austria 
    * Daniela Zaharie, West University of Timisoara, Romania

Local Committee Chairs
----------------------
    * Isabela Dramnesc, West University of Timisoara, Romania
    * Silviu Panica, Institute e-Austria 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 submitting a 
      short abstract (1/2 page, at maximum) where it is clearly 
      stated the main contribution(s) of the paper.

    * In the second step the authors should submit the full paper 
      (up to 8 pages in the two-columns IEEE conference style).

Both the abstract and the full paper should be submitted electronically 
through http://www.easychair.org/conferences/?conf=synasc2014.

-----------
SYNASC 2014
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: synasc14 <at> synasc.ro

------------------------------------------------------------------------------
Put Bad Developers to Shame
Dominate Development with Jenkins Continuous Integration
Continuously Automate Build, Test & Deployment 
Start a new project now. Try Jenkins in the cloud.
http://p.sf.net/sfu/13600_Cloudbees
SYNASC 2014 | 10 Apr 09:13 2014
Picon

[5 days left for abstract submission] CFP SYNASC 2014

[Please post - apologies for multiple copies.]

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

                       SYNASC 2014

              16th International Symposium on
   Symbolic and Numeric Algorithms for Scientific Computing
         September 22-25, 2014, Timisoara, Romania
           	  http://synasc.ro/2014/
	      http://synasc14.info.uvt.ro/

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
---------------

15 April 2014          :  Abstract submission  
30 April 2014          :  Paper submission 
15 July 2014           :  Notification of acceptance
01 September 2014      :  Registration
05 September 2014      :  Revised papers according to the reviews
22-25 September 2014   :  Symposium
30 November 2014       :  Final papers for post-proceedings

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
        + methods for hard computational problems
        + intelligent systems for scientific computing
        + agent-based complex systems modeling and development
        + scientific knowledge management
        + computational intelligence 
        + machine learning 
        + recommender and expert systems for scientific computing
        + data mining and web mining
        + natural language processing  
        + uncertain reasoning in scientific computing       
        + 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.   

Workshops
---------

    * Workshop on Agents for Complex Systems (ACSys)
           http://synasc.ro/2014/workshops/acsys-2014 
    * Workshop on Computational Topology in Image Context (CTIC)
           http://ctic2014.synasc.ro/index.html
    * Workshop on HPC research services (HPCReS)
           http://host.hpc.uvt.ro/events/hpcres-2014-international-workshop-on-hpc-research-services/ 
    * Workshop on GIC and Hydrologic Modeling (HydroGIS)    
           http://synasc.ro/2014/workshops/hydrogis-2014
    * Workshop on Iterative Approximation of Fixed Points (IAFP)
           http://synasc.ro/2014/workshops/iafp-2014
    * Workshop on Management of Resources and Services in Cloud and Sky Computing (MICAS)
           http://amicas.hpc.uvt.ro/micas-2014
    * Workshop on Natural Computing and Applications (NCA)
           http://synasc.ro/2014/workshops/nca-2014

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 considering to be published as special issues in international journals.

Invited Speakers 
----------------
    * Viorica Sofronie-Stokkermans, University Koblenz-Landau, Germany
    * Gheorghe Paun, Institute of Mathematics of the Romanian Academy, Bucharest, Romania
    * William Langdon, University College London, UK
    * Stefan Takacs, TU Chemnitz, Germany
    * Stephen Watt, University of Western Ontario, Canada

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 Chair
-------------
    * Viorel Negru, West University of Timisoara, Romania

Program Chair
-------------
    * Franz Winkler, Johannes Kepler University, Austria

Track Chairs
------------
    * Symbolic Computation
        + Tetsuo Ida, University of Tsukuba, Japan
        + Stephen Watt, University of Western Ontario, Canada

    * Numerical Computing
        + Richard Liska, Technical University of Prague, Czech Republic
        + Dana Petcu, West University of Timisoara, Romania

    * Logic and Programming
        + Tudor Jebelean, Johannes Kepler University Linz, Austria
        + Laura Kovacs, Chalmers University of Technology, Sweden

    * Artificial Intelligence
        + Andrei Petrovski, Robert Gordon University, UK	
        + Daniela Zaharie, West University of Timisoara, Romania

    * Distributed Computing
        + Marc Frincu, University of Southern California, US and 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, Research Institute e-Austria Timisoara, Romania

Special sessions and workshops chair
------------------------------------
    * Daniel Pop, West University of Timisoara, Romania

Tutorial chair
--------------
    * Dana Petcu, West University of Timisoara, Romania

Proceedings Chairs
------------------
    * Franz Winkler, Johannes Kepler University Linz, Austria 
    * Daniela Zaharie, West University of Timisoara, Romania

Local Committee Chairs
----------------------
    * Isabela Dramnesc, West University of Timisoara, Romania
    * Silviu Panica, Institute e-Austria 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 submitting a 
      short abstract (1/2 page, at maximum) where it is clearly 
      stated the main contribution(s) of the paper.

    * In the second step the authors should submit the full paper 
      (up to 8 pages in the two-columns IEEE conference style).

Both the abstract and the full paper should be submitted electronically 
through http://www.easychair.org/conferences/?conf=synasc2014.

-----------
SYNASC 2014
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: synasc14 <at> synasc.ro

------------------------------------------------------------------------------
Put Bad Developers to Shame
Dominate Development with Jenkins Continuous Integration
Continuously Automate Build, Test & Deployment 
Start a new project now. Try Jenkins in the cloud.
http://p.sf.net/sfu/13600_Cloudbees

Gmane