S B Cooper | 22 Oct 22:42 2014
Picon

CiE 2015: Evolving Computability, Bucharest, June 29 - July 3, 2015

1st CALL FOR PAPERS:
      COMPUTABILITY IN EUROPE 2015: Evolving Computability
                   Bucharest, Romania
                    June 29 - July 3
             http://fmi.unibuc.ro/CiE2015/

IMPORTANT DATES:

Submission Deadline for LNCS:                 11 January 2015
Notification of authors:                         9 March 2015
Deadline for final revisions:                    6 April 2015

CiE 2015 is the 11th conference organized by CiE (Computability
in Europe), a European association of mathematicians, logicians,
computer scientists, philosophers, physicists and others
interested in new developments in computability and their
underlying significance for the real world. Previous meetings
have taken place in Amsterdam (2005), Swansea (2006), Siena
(2007), Athens (2008), Heidelberg (2009), Ponta Delgada (2010),
Sofia (2011), Cambridge (2012), Milan (2013) and Budapest (2014).

Evolution of the universe, and us within it, invite a parallel
evolution in understanding. The CiE agenda - fundamental and
engaged - targets the extracting and developing of computational
models basic to current challenges.  From the origins of life, to
the understanding of human mentality, to the characterising of
quantum randomness - computability theoretic questions arise in
many guises.  The CiE community, this coming year meeting for the
first time in Bucharest, carries forward the search for
coherence, depth and new thinking across this rich and vital
(Continue reading)

Michael Winter | 20 Oct 21:19 2014
Picon

CFP: Relational and Algebraic Methods in Computer Science (RAMiCS 2015)


                           CALL FOR PAPERS

 
                  15th International Conference on
    Relational and Algebraic Methods in Computer Science (RAMiCS 2015)

            28 September to 1 October 2015, Braga, Portugal
                  URL:  http://ramics2015.di.uminho.pt
         PDF: http://ramics2015.di.uminho.pt/RAMiCS15-CFP.pdf

 
 Scope
 -----

 We invite submissions in the general area of Relational and Algebraic 
 Methods  in Computer Science. Special focus will lie on formal methods 
 for software engineering, logics of programs and links with neighbouring 
 disciplines.

 Particular topics of interest for the conference cover,
 but are not limited to:

 * Algebraic approaches to
   - specification, development, verification, and analysis of programs
     and algorithms
   - computational logic, in particular logics of programs, modal and
     dynamic logics, interval and temporal logics
   - semantics of programming languages

(Continue reading)

Ramana Kumar | 16 Oct 18:18 2014
Picon
Picon

Theorems Produced by Type Definitions

Hi all,

There has been an interesting discussion on the OpenTheory mailing list recently regarding how to simplify the two theorems produced by a type definition in HOL Light and remove their free variables. The latest message in the thread, which shows the  suggestions by Mario Carneiro can be found here: http://www.gilith.com/pipermail/opentheory-users/2014-October/000415.html.

I'm cross-posting to this list because I think using Mario's suggestions would be an improvement to both HOL Light and Opentheory. I hope the respective authors of those systems might agree and implement the changes, and that anyone else with an interest might voice their opinion.

Cheers,
Ramana
------------------------------------------------------------------------------
Comprehensive Server Monitoring with Site24x7.
Monitor 10 servers for $9/Month.
Get alerted through email, SMS, voice calls or mobile push notifications.
Take corrective actions from your mobile device.
http://p.sf.net/sfu/Zoho
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Geoff Sutcliffe | 15 Oct 14:34 2014
Picon

CADE-25 Call for Papers, etc.

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

CALL FOR WORKSHOPS, TUTORIALS, SYSTEM COMPETITIONS, AND PAPERS

25th International Conference on Automated Deduction (CADE-25)
Berlin, Germany, 1-7 August 2015

http://www.cade-25.info

Submission deadlines:

   14 November 2014 (workshops/tutorials/competitions)
16/23 February 2015 (papers)

CADE is the major international forum at which research on all aspects of
automated deduction is presented. The 25th jubilee edition will feature
a special session on the past, present, and future of automated deduction
with 

  Ursula Martin      University of Oxford
  Frank Pfenning     Carnegie Mellon University
  David Plaisted     University of North Carolina at Chapel Hill
  Andrei Voronkov    University of Manchester

as invited speakers. In addition, there will be invited presentations by

  Ulrich Furbach     University of Koblenz
  Edward Zalta       Stanford University

CALL FOR WORKSHOPS

Workshop proposals for CADE-25 are solicited. Both well-established
workshops and newer ones are encouraged. Similarly, proposals for workshops
with a tight focus on a core automated reasoning specialization, as well as
those with a broader, more applied focus, are very welcome.

Please provide the following information in your application document:

+ Workshop title.
+ Names and affiliations of organizers.
+ Proposed workshop duration (from half a day to two days) and preferred
  day(s).
+ Brief description of the goals and the scope of the workshop. Why is the
  workshop relevant for CADE?
+ Is the workshop new or has it met previously? In the latter case
  information on previous meetings should be given (e.g., links to the
  program, number of submissions, number of participants).
+ What are the plans for publication?

CALL FOR TUTORIALS

Tutorial proposals for CADE-25 are solicited. Tutorials are expected to be
half-day events, with a theoretical or applied focus, on a topic of interest
for CADE-25. Proposals should provide the following information:

+ Tutorial title.
+ Names and affiliations of organizers.
+ Brief description of the tutorial's goals and topics to be covered.
+ Whether or not a version of the tutorial has been given previously.

CADE will take care of printing and distributing notes for tutorials that
would like this service.

CALL FOR SYSTEM COMPETITIONS

The CADE ATP System Competition (CASC), which evaluates automated theorem
proving systems for classical logics, has become an integral part of the
CADE conferences.

Further system competition proposals are solicited. The goal is to foster
the development of automated reasoning systems in all areas relevant for
automated deduction in a broader sense. Proposals should include the
following information:

+ Competition title.
+ Names and affiliations of organizers.
+ Duration and schedule of the competition.
+ Room/space requirements.
+ Description of the competition task and the evaluation procedure.
+ Is the competition new or has it been organized before?
  In the latter case information on previous competitions should be given.
+ What computing resources are required and how will they be provided?

CALL FOR PAPERS

High-quality submissions on the general topic of automated deduction,
including foundations, applications, implementations, and practical
experiences are solicited.

* Logics of interest include propositional, first-order, equational,
  higher-order, classical, description, modal, temporal, many-valued,
  constructive, other non-classical, meta-logics, logical frameworks, type
  theory, set theory, as well as any combination thereof.

* Paradigms of interest include theorem proving, model building, constraint
  solving, computer algebra, model checking, proof checking, and their
  integration.

* Methods of interest include resolution, superposition, completion,
  saturation, term rewriting, decision procedures, model elimination,
  connection methods, tableaux, sequent calculi, natural deduction, as
  well as their supporting algorithms and data structures, including
  matching, unification, orderings, induction, indexing techniques, proof
  presentation and explanation, proof planning.

* Applications of interest include program analysis, verification and
  synthesis of software and hardware, formal methods, computational logic,
  computer mathematics, natural language processing, computational
  linguistics, knowledge representation, ontology reasoning, deductive
  databases, declarative programming, robotics, planning, and other areas
  of AI.

Submissions can be made in the categories regular papers and system
descriptions. The page limit in Springer LNCS style is 15 pages for regular
papers and 10 pages for system descriptions. Submissions must be unpublished
and not submitted for publication elsewhere. They will be judged on
relevance, originality, significance, correctness, and readability. System
descriptions should contain a link to a working system and will also be
judged on usefulness and design. Proofs of theoretical results that do not
fit in the page limit, executables of systems, and input data of experiments
should be made available, via a reference to a website or in an appendix of
the paper. Reviewers will be encouraged to consider this additional
material, but submissions must be self-contained within the respective page
limit; considering the additional material should not be necessary to
assess the merits of a submission. The proceedings of the conference will
be published in the Springer LNCS/LNAI series. Formatting instructions and
the LNCS style files can be obtained at 

http://www.springer.de/comp/lncs/authors.html

At every CADE conference the Program Committee selects one of the
accepted papers to receive the CADE Best Paper Award. The award
recognizes a paper that the Program Committee collegially evaluates as
the best in terms of originality and significance, having substantial
confidence in its correctness. Overall technical quality,
completeness, scholarly accuracy, and readability are also
considered. Characteristics associated with a best paper include, for
instance, introduction of a strong new technique or approach, solution
of a long-standing open problem, introduction and solution of an
interesting and important new problem, highly innovative application
of known ideas or existing techniques, and presentation of a new
system of outstanding power. Under exceptional circumstances, the
Program Committee may give two awards (ex aequo) or give no award.

At CADE-25 we also intend to award the best student paper (details
will follow).

IMPORTANT DATES

Workshop/Tutorials/System Competitions:

Submission deadline:      14 November 2014
Notification:             28 November 2014

Papers:

Abstract deadline:        16 February 2015
Submission deadline:      23 February 2015
Rebuttal phase:           15-18 April 2015
Notification:             26 April 2015
Final version:            17 May 2015

Workshops and Tutorials:  1 August to 3 August (morning) 2015
Competitions:             1 to 7 August 2015
Conference:               3 August (afternoon) to 7 August 2015

SUBMISSION INSTRUCTIONS

Proposals for workshops, tutorials, and system competitions should be
uploaded via

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

Papers should be submitted via

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

CADE-25 ORGANIZERS

Conference Chair:
  Christoph Benzmüller   Freie Universität Berlin

Program Committee Co-Chairs:
  Amy Felty              University of Ottawa
  Aart Middeldorp        University of Innsbruck

Workshop, Tutorial, and Competition Co-Chairs:
  Jasmin Blanchette      Technische Universität München
  Andrew Reynolds        EPFL Lausanne

Publicity and Web Chair:
  Julian Röder           Freie Universität Berlin

Program Committee
  Carlos Areces          Universidad Nacional de Córdoba
  Alessandro Armando     University of Genova
  Christoph Benzmüller   Freie Universität Berlin
  Josh Berdine           Microsoft Research
  Jasmin Blanchette      Technische Universität München
  Marta Cialdea Mayer    Universita di Roma Tre
  Stephanie Delaune      CNRS
  Gilles Dowek           Inria
  Amy Felty              University of Ottawa
  Reiner Hähnle          Technical University of Darmstadt
  Stefan Hetzl           Vienna University of Technology
  Marijn Heule           The University of Texas at Austin
  Nao Hirokawa           JAIST
  Ullrich Hustadt        University of Liverpool
  Deepak Kapur           University of New Mexico
  Gerwin Klein           NICTA and UNSW
  Laura Kovács           Chalmers University of Technology
  Carsten Lutz           Universität Bremen
  Assia Mahboubi         Inria
  Aart Middeldorp        University of Innsbruck
  Albert Oliveras        Technical University of Catalonia
  Nicolas Peltier        CNRS
  Brigitte Pientka       McGill University
  Ruzica Piskac          Yale University
  André Platzer          Carnegie Mellon University
  Andrew Reynolds        EPFL Lausanne
  Christophe Ringeissen  LORIA-INRIA
  Renate Schmidt         University of Manchester
  Stephan Schulz         DHBW Stuttgart
  Georg Struth           University of Sheffield
  Geoff Sutcliffe        University of Miami
  Alwen Tiu              Nanyang Technological University
  Freek Wiedijk          Radboud University Nijmegen

------------------------------------------------------------------------------
Comprehensive Server Monitoring with Site24x7.
Monitor 10 servers for $9/Month.
Get alerted through email, SMS, voice calls or mobile push notifications.
Take corrective actions from your mobile device.
http://p.sf.net/sfu/Zoho
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Geoff Sutcliffe | 13 Oct 18:44 2014
Picon

NETYS 2015 Call for Papers

*CALL FOR PAPERS

THE INTERNATIONAL CONFERENCE ON NETWORKED SYSTEMS**
**NETYS 2015**
**May 13-15, 2015, AGADIR, MOROCCO**
**http://www.netys.net*

*Aim and Scope:**
*
NETYS aims to bring together researchers and engineers from both the 
theory and practice of distributed and networked systems. The scope of 
the conference covers all aspects related to the design and the 
development of these systems, including, but not restricted to, 
multi-core architectures, concurrent and distributed algorithms, 
parallel/concurrent/distributed programming, distributed databases, 
cloud systems, networks, security, formal verification, etc.

NETYS will provide a forum to report on best practices and novel 
algorithms, results and techniques on networked systems. Original 
contributions as well as experience papers on the principles, design, 
implementation, modeling, analysis, verification, and application of 
networked systems are solicited. Specific concepts common to different 
forms of such systems are most welcome.

NETYS is coupled with the METIS Spring School which aims at introducing 
young researchers to the domain of distributed and networked systems 
through tutorials on basics, as well as lectures on new research topics 
and current trends in this domain.

*Paper submission:**
*
Submissions should contain original research and sufficient detail to 
assess the merits and relevance of the contribution. NETYS welcomes 
papers on theory, case studies and comparisons with existing 
experimental research, tools, as well as combinations of new theory with 
experimental evaluation.

NETYS is soliciting two forms of papers: full and short papers. Full 
papers are allowed a maximum of 15 pages in Springer's LNCS format, 
whereas short papers are allowed a maximum of 5 pages (in the same 
format), both in the submission and in the proceedings. A full paper 
submission might be accepted as such, as a short paper or a poster. A 
short paper may be accepted as such or as a poster.

Posters will be presented at the conference to reflect work in progress 
and will not lead to a publication in the proceedings. Authors are given 
the option to accept or not the type in which their paper is selected 
for acceptance.

*Publication:*

Springer's Lecture Notes in Computer Science series will publish the 
proceedings of the conference (www.springer.com/lncs). It is required 
that each accepted paper be presented at the conference by one of its 
authors.

The Computing Journal could publish extended versions of selected papers 
(www.springer.com/computer/journal/607)

Awards will be given to the best paper and the best student paper. A 
paper is eligible for the best student paper award if at least one of 
its authors is a full-time student at the time of submission. This 
should be indicated in the submission.

*Submission instructions:*

All submissions should follow the LNCS template. Submitted papers must 
be written in English. Full papers are allowed a maximum of 15 pages in 
LNCS format, whereas short papers are allowed a maximum of 5 pages, both 
in the submission and in the proceedings. Papers exceeding these limits 
may be rejected without review.

Paper submission will be handled by EasyChair, so please make sure that 
you have an active account. The papers must be submitted electronically at:
https://easychair.org/conferences/?conf=netys2015

*Important dates**
*
- Abstract submission deadline: January 5, 2015
- Paper submission deadline: January 9, 2015
- Acceptance notification: March 9, 2015
- Camera ready copy due: April 10, 2015
- Conference: May 13-15, 2015

*Organization:*

/_General Co-chairs_:/
Mohammed Erradi        ENSIAS, Rabat, Morocco
Rachid Guerraoui       EPFL, Switzerland

/_Program Co-chairs_:/
Ahmed Bouajjani        Univ. Paris Diderot, France
Hugues Fauconnier      Univ. Paris Diderot, France

/_Program Committee_:/
Parosh Aziz Abdulla    Univ. Uppsala, Sweden
Joffroy Beauquier      Univ. Paris 11, France
Gregor Bochmann        Univ. Ottawa, Canada
Carole Delporte        Univ. Paris Diderot, France
Amr El Abbadi          UCSB, USA
Khaldoun El Agha       Univ. Paris 11, France
Mohamed El Koutbi      ENSIAS, Rabat, Morocco
Boualem Benatallah     Univ. New South Wales, Australia
Mohamed El Kamili      USMBA, Fes, Morocco
Bernd Freisleben       Univ. Marburg, Germany
Mohamed Gouda          Univ. Texas at Austin
Vincent Gramoli        Univ. Sydney, Australia
Seif Haridi            SICS, Sweden
Maurice Herlihy        Brown Univ., USA
Claude Jard            Univ. Nantes, France
Zahi Jarir             Univ. Cadi Ayyad, Morocco
Anne-Marie Kermarrec   INRIA, Rennes, France
Rupak Majumdar         MPI-SWS, Germany
Stephan Merz           INRIA, Nancy, France
Louise Moser           UCSB, USA
Hassan Mountassir      Univ. Franche-Comt?, France
Guevara Noubir         Northeastern Univ., USA
Andreas Podelski       Univ. Freiburg, Germany
Shaz Qadeer            Microsoft Research, USA
Vivien Quema           INPG, Grenoble, France
Sergio Rajsbaum        UNAM, Mexico
Ganesan Ramalingam     Microsoft Research, India
Michel Raynal          IRISA, Rennes, France
Alexander Shvartsman   Univ. Connecticut, USA
Sebastian Tixeuil      Univ. Pierre et Marie Curie, France
Martin Vechev          ETH Zurich, Switzerland

_/Organizing Committee/_:
Khadija Bakkouch       IRFC, Rabat
Abdellah Boulouz       Univ. Ibn zohr, Agadir
Mohammed Erradi        ENSIAS, UM5S, Rabat
Zahi Jarir             Univ. Cadi Ayyad, Marrakech
Mohammed Ouzzif        ESTC, UH2M, Casablanca

_/Students Committee/_:
Meryeme Ayache        ENSIAS, UM5S, Rabat
Yahya Benkaouz        ENSIAS, UM5S, Rabat

------------------------------------------------------------------------------
Comprehensive Server Monitoring with Site24x7.
Monitor 10 servers for $9/Month.
Get alerted through email, SMS, voice calls or mobile push notifications.
Take corrective actions from your mobile device.
http://p.sf.net/sfu/Zoho
Sophie Tison | 13 Oct 08:17 2014
Picon

RTA 2015 - First Call For Papers

==================================================================
              RTA 2015 - CALL FOR PAPERS 
           26th International Conference on
        REWRITING TECHNIQUES AND APPLICATIONS
        29 June - 1 July, 2015, Warsaw, Poland 
      co-located with TLCA, as part of RDP 2015
           http://rdp15.mimuw.edu.pl/
==================================================================

RTA is the major forum for the presentation of research on all 
aspects of rewriting.  Topics of interest include:

* Foundations: string, term, net and graph rewriting; higher-order
rewriting; binding techniques; constrained rewriting and deduction;
categorical and infinitary rewriting; stochastic rewriting;
higher-dimensional rewriting; tree automata; confluence; 
termination; complexity; modularity; equational logic; 
universal algebra; rewriting logic; rewriting calculi.

* Algorithmic aspects and implementation: strategies; matching;
unification; anti-unification; narrowing; completion; parallel
execution; certification of rewriting properties; abstract machines;
automated (non)termination and confluence provers; automated
complexity analysis; system descriptions.

* Applications of rewriting: programming languages (functional, 
logic, object-oriented and other programming paradigms); type 
systems; program analysis, transformation and optimisation; 
rewriting models of programs; semantics; process calculi; 
functional calculi; explicit substitution; constraint solving; 
symbolic and algebraic computation; theorem proving; 
proof checking; system modelling; system synthesis and 
verification; XML queries and transformations; cryptographic 
protocols; security policies; systems biology; linguistics; 
rewriting in education.

Important Dates:
# Submission: title and abstract: 30 January 2015
              full paper: 6 February 2015
# Rebuttal period: 19-21 March 2015  
# Notification:    8 April 2015
# Final version:  25 April 2015

Submission and publication:
The RTA 2015 proceedings will be published by LIPIcs (Leibniz
International Proceedings in Informatics). Papers should present
original work, and should be submitted via Easychair:
https://www.easychair.org/conferences/?conf=rta2015
Papers should be at most 15 pages (10 for system descriptions) 
in the style described in:
http://drops.dagstuhl.de/styles/lipics/lipics-authors.tgz 
This year we particularly welcome submissions on applications of
rewriting. Application papers are regular papers (15 pages); their
originality is judged based on the novelty of the application or the
depth of the rewriting methods applied. 
System description papers present new software tools in which 
rewriting plays an important role, or significantly new versions 
of such tools. The paper should also include an evaluation of the 
tool.

Programme Committee:
M. Ayala-Rincon, U. Brasilia
H. Cirstea, Loria Nancy
S. Delaune, ENS Cachan
A. Di Pierro, U. Verona
G. Dowek, Inria
M. Fernandez, KCL, chair
J. Giesl, RWTH Aachen U.
M. Hanus, CAU Kiel
D. Kesner, U. Paris-Diderot
T. Kutsia, Johannes Kepler U. Linz
J. Levy, IIIA-CSIC Barcelona
S. Lucas, Polytechnic U. Valencia
C. Lynch, Clarkson U.
I. Mackie, E. Polytechnique
G. Moser, U. Innsbruck
D. Plump, U. York
F. van Raamsdonk, VU Amsterdam
K. Rose, Two Sigma, US
M. Sakai, Nagoya U.
A. Scedrov, U. Pennsylvania
M. Schmidt-Schauss, U. Frankfurt
C. Schuermann, ITU Copenhagen	
P. Selinger, Dalhousie U.
P. Severi, U. Leicester
K. Ueda, Waseda U.

Conference Chair:
Aleksy Schubert
Warsaw University

For more information, please contact the PC chair:
Maribel.Fernandez <at> kcl.ac.uk

******************************************************
Pr. Sophie Tison (RTA publicity chair)
LIFL - University of Lille- CNRS
www.lifl.fr/~tison
sophie.tison <at> lifl.fr

Attachment (smime.p7s): application/pkcs7-signature, 3818 bytes
------------------------------------------------------------------------------
Meet PCI DSS 3.0 Compliance Requirements with EventLog Analyzer
Achieve PCI DSS 3.0 Compliant Status with Out-of-the-box PCI DSS Reports
Are you Audit-Ready for PCI DSS 3.0 Compliance? Download White paper
Comply to PCI DSS 3.0 Requirement 10 and 11.5 with EventLog Analyzer
http://p.sf.net/sfu/Zoho
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Ramana Kumar | 11 Oct 11:11 2014
Picon
Picon

annotation with HOLKeyword

When I make a munger with monadsyntax and use it to typeset some monadic functions, the "do" and "od" delimiters of a list of binds are emitted as-is. I would like them to be annotated as HOLKeywords.

I know I could probably use the override map for that, but it seems like there ought to be a more proper way of doing it. How do keywords (like "if") normally get annotated, and can we do the same for "do" and "od"?
------------------------------------------------------------------------------
Meet PCI DSS 3.0 Compliance Requirements with EventLog Analyzer
Achieve PCI DSS 3.0 Compliant Status with Out-of-the-box PCI DSS Reports
Are you Audit-Ready for PCI DSS 3.0 Compliance? Download White paper
Comply to PCI DSS 3.0 Requirement 10 and 11.5 with EventLog Analyzer
http://p.sf.net/sfu/Zoho
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Marjan Sirjani | 7 Oct 00:02 2014
Picon

Final CFP: FSEN 2015

Our apologies if you have received multiple copies.

######################################################################
                                                                    FSEN  2015: CALL FOR PAPERS
 
Sixth International Conference on
Fundamentals of Software Engineering 2015 Theory and Practice (FSEN '15)
http://fsen.ir/2015
Tehran, Iran
22 - 24 April, 2015
######################################################################
 
-- About FSEN --
 
FSEN is an international conference that aims to bring together researchers, engineers, developers,
and practitioners from the academia and the industry to present and discuss their research work in
the area of formal methods for software engineering. This conference seeks to facilitate the transfer
of experience, adaptation of methods, and where possible, foster collaboration among different groups.
The topics of interest cover all aspects of formal methods, especially those related to advancing
the application of formal methods in the software industry and promoting their integration with
practical engineering techniques.
 
-- Important Dates --
 
Abstract Submission: October 24, 2014
Paper Submission: October 31, 2014
Notification: December 26, 2014
Camera Ready: January 16, 2015
Conference: April 22-24, 2015
 
-- Keynote Speakers --
 
 Holger Giese, Hasso Plattner Institute, Germany
 John Hughes, Chalmers University of Technology, Sweden
 Paola Inverardi, University of L'Aquila, Italy
 
-- Topics of Interest --
 
The topics of this conference include, but are not restricted to, the following:
* Models of programs and software systems
* Software specification, validation, and verification
* Software testing
* Software architectures and their description languages
* Object and multi-agent systems
* Coordination and feature interaction
* Integration of formal and informal methods
* Integration of different formal methods
* Component-based and Service-oriented software systems
* Self-adaptive software systems
* Model checking and theorem proving
* Software and hardware verification
* CASE tools and tool integration
* Industrial Applications
 
-- Paper Submission --
 
Papers should be formatted according to the Springer LNCS style,
not exceed 15 pages (including figures and references), submitted in PDF or postscript format,
and not be submitted simultaneously for publication elsewhere.
Papers will be evaluated based on originality, significance, relevance, correctness and clarity.
 
-- Proceedings and Special Issues --
 
The post-proceedings of FSEN'15 will be published by Springer Verlag in the LNCS series
(official approval in process). There will also be a pre-proceeding, printed locally by IPM,
available at the conference. Following the tradition of the past editions,
we plan to have a special issue of Science of Computer Programming journal devoted to FSEN'15 (to be confirmed).
 
 
-- General Chair --
 
 Farhad Arbab - CWI, Netherlands; Leiden University, Netherlands
 Hamid Sarbazi-azad - IPM, Iran; Sharif University of Technology, Iran
 
-- Program Chairs --
 
 Mehdi Dastani - Utrecht University, The Netherlands
 Marjan Sirjani - Reykjavík University, Iceland; University of Tehran, Iran
 
-- Publicity Chair --
 
 Hossein Hojjat - Cornell University, USA
 
-- Steering Committee --
 
 Farhad Arbab - CWI, Netherlands; Leiden University, Netherlands
 Christel Baier - University of Dresden, Germany
 Frank de Boer - CWI, Netherlands; Leiden University, Netherlands
 Ali Movaghar - IPM, Iran; Sharif University of Technology, Iran
 Hamid Sarbazi-azad - IPM, Iran; Sharif University of Technology, Iran
 Marjan Sirjani - Reykjavik University, Iceland; University of Tehran, Iran (chair)
 Jan Rutten - CWI, Netherlands; Vrije University Amsterdam, Netherlands
 
-- Program Committee --
 
 Mohammad Abdollahi Azgomi - Iran University of Science and Technology, Iran
 Christel Baier - TU Dresden, Germany
 Ezio Bartocci, Vienna University of Technology, Austria
 Borzoo Bonakdarpour - University of Waterloo, Canada
 Marcello Bonsangue - Leiden University, Netherlands
 Mario Bravetti - University of Bologna, Italy
 Fabiano Dalpiaz - Utrecht University, Netherlands
 Mehdi Dastani - Utrecht University, Netherlands
 Erik De Vink - Technical University of Eindhoven, Netherlands
 Klaus Dräger - University of Oxford, UK
 Wan Fokkink - Vrije Universiteit Amsterdam, Netherlands
 Masahiro Fujita - University of Tokyo, Japan
 Maurizio Gabbrielli - University of Bologna, Italy
 Fatemeh Ghassemi - University of Tehran, Iran
 Jan Friso Groote - Technical University of Eindhoven, Netherlands
 Hassan Haghighi - Shahid Beheshti University, Iran
 Hossein Hojjat - Cornell University, USA
 Mohammad Izadi - Sharif University of Technology, Iran
 Mohammad Mahdi Jaghoori - CWI, Netherlands; Academic Medical Center of University of Amsterdam, Netherlands
 Einar Broch Johnsen - University of Oslo, Norway
 Joost-Pieter Katoen - RWTH Aachen University, Germany
 Narges Khakpour - KTH, Sweden
 Ramtin Khosravi - University of Tehran, Iran
 Zhiming Liu - Birmingham City University, UK
 Seyyed Hassan Mirian Hosseinabadi - Sharif University of Technology, Iran
 Ugo Montanari - University of Pisa, Italy
 Peter Mosses - Swansea University, UK
 Mohammad Reza Mousavi - Halmstad University, Sweden
 Ali Movaghar - Sharif University of Technology, Iran
 Peter Olveczky - University of Oslo, Norway
 Jose Proenca - K.U.Leuven, Belgium
 Niloofar Razavi - University of Toronto, Canada
 Philipp Ruemmer - Uppsala University, Sweden
 Gwen Salaun - Grenoble INP, Inria, France
 Cesar Sanchez - IMDEA Software Institute, Spain
 Wendelin Serwe - INRIA, France
 Marjan Sirjani - Reykjavik University, Iceland
 Meng Sun - Peking University, China
 Carolyn Talcott - SRI International, USA
 Samira Tasharofi - Microsoft, USA
 Tayssir Touili - LIAFA, France
 Danny Weyns - Linnaeus University, Sweden
------------------------------------------------------------------------------
Meet PCI DSS 3.0 Compliance Requirements with EventLog Analyzer
Achieve PCI DSS 3.0 Compliant Status with Out-of-the-box PCI DSS Reports
Are you Audit-Ready for PCI DSS 3.0 Compliance? Download White paper
Comply to PCI DSS 3.0 Requirement 10 and 11.5 with EventLog Analyzer
http://p.sf.net/sfu/Zoho
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
DIFTS14 | 7 Oct 15:26 2014
Picon

DIFTS'14 - Call For Participation

***************************************************************************
                              DIFTS'14
             DESIGN and IMPLEMENTATION of FORMAL TOOLS and
SYSTEMS
                      CALL FOR PARTICIPATION
***************************************************************************

Third International Workshop on Design and Implementation
of Formal Tools
and Systems (co-located with FMCAD 2014, and MEMOCODE
2014)

http://fmgroup.polito.it/cabodi/difts2014/

Lausanne, Switzerland
October 20, 2014

WORKSHOP SCOPE

DIFTS (Design and Implementation of Formal Tools and
Systems) workshop
emphasizes insightful experiences in formal tools and
systems design.  It
provides a forum for sharing challenges and solutions that
are original with
ground breaking results.

Often the design and implementation of tools for formal
analysis require
non-trivial engineering decisions. Many challenges are
faced, which often can
only be met with ingenious implementation techniques.
These techniques actually
play a crucial role in making the idea work in practice.
The workshop provides
an opportunity for discussing engineering aspects and
various design decisions
required to put such formal tools and systems into
practical use.

WORKSHOP PROGRAM

http://fmgroup.polito.it/cabodi/difts2014/#program

INVITED SPEAKERS

Rolf Drechsler, University of Bremen, Germany
"Coverage at the Formal Specification Level"

Wolfgang Kunz, University of Kaiserslautern, Germany
"The big hurdles for FV tools in industrial practice – can
we overcome them insystem-level design flows?"

Fahim Rahim, Atrenta, France
"Efficiently using formal verification techniques to
reduce power"

REGISTRATION (provided through FMCAD'14 website)

Registration information is available at
http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD14/registration.shtml

A list of recommended hotels with preferential rates is
available at
http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD14/venue.shtml

ORGANIZATION

PROGRAM CHAIRS

Malay K. Ganai, Atrenta, USA
Gianpiero Cabodi, Politecnico di Torino, Italy

PROGRAM COMMITTEE

Chao Wang, Virginia Tech, USA
Shuvendu Lahiri, Microsoft Research, USA
Roberto Bruttomesso, Atrenta, France
Alberto Griggio, FBK-IRST, Italy
Alper Sen, Bogazici University, Turkey
Joao Marques-Silva, University College Dublin, Ireland
Priyank Kalla, University of Utah, USA
Supratik Chakraborty, IIT Bombay, India
Erika Abraham, RWTH Aachen University, Germany
Andreas Veneris, University of Toronto, Canada
Daniel Grosse, University of Bremen, Germany

WEBMASTERS

Pasini Paolo, Politecnico di Torino, Italy
Marco Palena, Politecnico di Torino, Italy

------------------------------------------------------------------------------
Meet PCI DSS 3.0 Compliance Requirements with EventLog Analyzer
Achieve PCI DSS 3.0 Compliant Status with Out-of-the-box PCI DSS Reports
Are you Audit-Ready for PCI DSS 3.0 Compliance? Download White paper
Comply to PCI DSS 3.0 Requirement 10 and 11.5 with EventLog Analyzer
http://p.sf.net/sfu/Zoho
Klaus Havelund | 3 Oct 18:28 2014
Picon
Picon

[fm-announcements] NFM 2015 - 3rd call for papers


CALL FOR PAPERS

The 7th NASA Formal Methods Symposium

http://www.NASAFormalMethods.org/nfm2015

27 – 29 April 2015
Pasadena, California, USA

Paper Submission: 10 Nov 2014

THEME

The widespread use and increasing complexity of mission- and safety-critical systems require advanced
techniques that address their specification, verification, validation, and certification.

The NASA Formal Methods Symposium is a forum for theoreticians and practitioners from academia,
industry, and government, with the goals of identifying challenges and providing solutions to
achieving assurance in mission- and safety-critical systems. Within NASA such systems include for
example autonomous robots, separation assurance algorithms for aircraft, Next Generation Air
Transportation (NextGen), and autonomous rendezvous and docking for spacecraft. Moreover, emerging
paradigms such as property-based design, code generation, and safety cases are bringing with them new
challenges and opportunities. The focus of the symposium will be on formal techniques, their theory,
current capabilities, and limitations, as well as their application to aerospace, robotics, and other
mission- and safety-critical systems in all design life-cycle stages. We encourage submissions on
cross-cutting approaches marrying formal verification techniques with advances in critical system
development, such as requirements generation, analysis of aerospace operational concepts, and formal
methods integrated in early design stages and carrying throughout system development.

TOPICS

Topics of interest include, but are not limited to:

Model checking
Theorem proving
SAT and SMT solving
Symbolic execution
Static analysis
Runtime verification
Program refinement
Compositional verification
Modeling and specification formalisms
Model-based development
Model-based testing
Requirement engineering
Formal approaches to fault tolerance
Security and intrusion detection
Applications of formal methods to aerospace systems
Applications of formal methods to cyber-physical systems
Applications of formal methods to human-machine interaction analysis

INVITED SPEAKERS

Dino Distefano
Software Engineer at Facebook, California, USA and Professor at Queen Mary University of London, UK.

Viktor Kuncak
Leads Lab for Automated Reasoning and Analysis at EPFL, Lausanne, Switzerland.

Rob Manning
Chief Engineer at NASA/JPL.

IMPORTANT DATES

Paper Submission:	10 Nov 2014
Paper Notifications:	12 Jan 2015
Camera-ready Papers:	9 Feb 2015
Symposium:   27 – 29 April 2015

LOCATION AND COST

The symposium will take place at the Hilton Hotel, Pasadena, California, USA, April 27-29, 2015.

There will be no registration fee for participants. All interested individuals, including non-US
citizens, are welcome to submit, to attend, to listen to the talks, and to participate in discussions;
however, all attendees must register.

SUBMISSION DETAILS

There are two categories of submissions:

- Regular papers describing fully developed work and complete results (15 pages)
- Short papers describing tools, experience reports, or descriptions of work in progress with
preliminary results  
  (6 pages)

All papers should be in English and describe original work that has not been published or submitted
elsewhere. All submissions will be fully reviewed by members of the Programme Committee. Papers will
appear in a volume of Springer’s Lecture Notes on Computer Science (LNCS), and must use LNCS style
formatting. Papers should be submitted in PDF format.

PC CHAIRS

Klaus Havelund, NASA Jet Propulsion Laboratory
Gerard Holzmann, NASA Jet Propulsion Laboratory
Rajeev Joshi, NASA Jet Propulsion Laboratory

PROGRAMME COMMITTEE

Erika Abraham, RWTH Aachen University, Germany
Julia Badger, NASA Johnson Space Center, USA
Christel Baier, Technische Universität Dresden, Germany
Saddek Bensalem, VERIMAG/UJF, France
Dirk Beyer, University of Passau, Germany
Armin Biere, Johannes Kepler University, Austria
Nikolaj Bjorner, Microsoft Research, USA
Borzoo Bonakdarpour, McMaster University, Canada
Alessandro Cimatti, Fondazione Bruno Kessler, Italy
Leonardo de Moura, Microsoft Research, USA
Ewen Denney, NASA Ames Research Center, USA
Ben Di Vito, NASA Langley Research Center, USA
Dawson Engler, Stanford University, USA
Jean-Christophe Filliatre, Université Paris-Sud, France
Dimitra Giannakopoulou, NASA Ames Research Center, USA
Alwyn Goodloe, NASA Langley Research Center, USA
Susanne Graf, VERIMAG, France
Alex Groce, Oregon State University, USA
Radu Grosu, Vienna University of Technology, Austria
John Harrison, Intel Corporation, USA
Mike Hinchey, University of Limerick/Lero, Ireland
Bart Jacobs, University of Leuven, Belgium
Sarfraz Khurshid, The University of Texas at Austin, USA
Gerwin Klein, NICTA, Australia
Daniel Kroening, Oxford University, UK
Orna Kupferman, Hebrew University Jerusalem, Israel
Kim Larsen, Aalborg University, Denmark
Rustan Leino, Microsoft Research, USA
Martin Leucker, University of Lubeck, Germany
Rupak Majumdar, Max Planck Institute, Germany
Pete Manolios, Northeastern University, USA
Peter Mueller, ETH Zurich, Switzerland
Kedar Namjoshi, Bell Labs/Alcatel-Lucent, USA
Corina Pasareanu, NASA Ames Research Center, USA
Doron Peled, Bar Ilan University, Israel
Suzette Person, NASA Langley Research Center, USA
Andreas Podelski, University of Freiburg, Germany
Grigore Rosu, University of Illinois, USA
Kristin Yvonne Rozier, NASA Ames Research Center, USA
Natarajan Shankar, SRI International, USA
Natasha Sharygina, University of Lugano, Switzerland
Scott Smolka, Stony Brook University, USA
Willem Visser, University of Stellenbosch, South Africa
Mahesh Viswanathan, University of Illinois, USA
Mike Whalen, University of Minnesota, USA
Jim Woodcock, University of York, UK

STEERING COMMITTEE

Julia Badger, NASA Johnson Space Center
Ewen Denney, NASA Ames Research Center
Ben Di Vito, NASA Langley Research Center
Klaus Havelund, NASA Jet Propulsion Laboratory
Gerard Holzmann, NASA Jet Propulsion Laboratory
Cesar Munoz, NASA Langley Research Center
Corina Pasareanu, NASA Ames Research Center
Suzette Person, NASA Langley Research Center
Kristin Yvonne Rozier, NASA Ames Research Center

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

------------------------------------------------------------------------------
Meet PCI DSS 3.0 Compliance Requirements with EventLog Analyzer
Achieve PCI DSS 3.0 Compliant Status with Out-of-the-box PCI DSS Reports
Are you Audit-Ready for PCI DSS 3.0 Compliance? Download White paper
Comply to PCI DSS 3.0 Requirement 10 and 11.5 with EventLog Analyzer
http://p.sf.net/sfu/Zoho
Mario Carneiro | 11 Oct 04:34 2014
Picon

Instrumenting the HOL light core

Hello,

I'm interested in examining the core axiom functions of HOL so that I can produce diagnostic information on the actual proof process as the program runs. What is the best way to do this? I remember hearing somewhere that someone made a program to convert HOL light proofs into something understandable by an automated prover, and I am trying to something similar (I want to translate HOL proofs into another language), so I'm curious if there is an already established method for getting this sort of data out of the core.

Mario Carneiro
------------------------------------------------------------------------------
Meet PCI DSS 3.0 Compliance Requirements with EventLog Analyzer
Achieve PCI DSS 3.0 Compliant Status with Out-of-the-box PCI DSS Reports
Are you Audit-Ready for PCI DSS 3.0 Compliance? Download White paper
Comply to PCI DSS 3.0 Requirement 10 and 11.5 with EventLog Analyzer
http://p.sf.net/sfu/Zoho
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Gmane