Jiaqi Tan | 26 Jan 13:54 2015
Picon

Question: Internal HOL4 resource usage when using prove, store_thm, and Define

Hi,

I have some questions regarding the internals of HOL4, and whether there are any internal resources (memory/storage) used when certain functions are used.

1. If I use prove or TAC_PROOF, and a theorem is successfully proved, is the theorem automatically saved in internal HOL4 storage? I would believe it is not stored, unless I assigned it to a variable with val my_thm = prove(...). In this case, if I just use prove() (or TAC_PROOF) without saving the result to a variable, does this mean that one command later on the interactive shell, the prove theorem will no longer use any resources? (i.e. after val it has been overwritten).

2. If I use store_thm instead, then this would consume resources in HOL4's internal memory? After I call store_thm, suppose I don't need the theorem any more, is there any way to reclaim the internal storage used?

3. Similarly for Define, are the theorems which described the Define-d function stored internally in HOL4 storage? Suppose I do "Define ``MY_FUNC = 1``", and I do not store the definition theorem in a variable, does the definition still get stored internally in HOL4? And is there any way to clear/remove the definition later to reclaim space if so?

In general, if I am Define-ing a large number of functions for temporary use (e.g. rewriting away a large expression), but I do not need them after a certain point in the code, are there any internal HOL4 memory/resources used, and is there any way to reclaim these resources later?

Thank you in advance!

Regards,
Jiaqi

------------------------------------------------------------------------------
Dive into the World of Parallel Programming. The Go Parallel Website,
sponsored by Intel and developed in partnership with Slashdot Media, is your
hub for all things parallel software development, from weekly thought
leadership blogs to news, videos, case studies, tutorials and more. Take a
look and join the conversation now. http://goparallel.sourceforge.net/
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Fabio Zanasi | 21 Jan 22:54 2015
Picon
Picon

CALCO 2015: Second Call for Papers

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

              CALL FOR PAPERS:  CALCO 2015

6th International Conference on Algebra and Coalgebra in Computer Science

                 June 24 - 26, 2015

                Nijmegen, Netherlands

               http://coalg.org/calco15/

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

       Abstract submission:    March 22, 2015
       Paper submission:       April 2, 2015
       Author notification:    May 6, 2015
       Final version due:      June 3, 2015

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

-- SCOPE --

CALCO aims to bring together researchers and practitioners with interests in foundational aspects, and both traditional and emerging uses of algebra and coalgebra in computer science.

It is a high-level, bi-annual conference formed by joining the forces and reputations of CMCS (the International Workshop on Coalgebraic Methods in Computer Science), and WADT (the Workshop on Algebraic Development Techniques). Previous CALCO editions took place in Swansea (Wales, 2005), Bergen (Norway, 2007), Udine (Italy, 2009), Winchester (UK, 2011) and Warsaw (Poland, 2013). The sixth edition will be held in Nijmegen, the Netherlands, colocated with MFPS XXXI.

-- INVITED SPEAKERS --

Andy Pitts - University of Cambridge, UK (joint with MFPS)
Chris Heunen - University of Oxford, UK
Matteo Mio - CNRS, ENS Lyon, FR
Daniela Petrisan - Radboud University, Nijmegen, NL

-- TOPICS OF INTEREST --

We invite submissions of technical papers that report results of theoretical work on the mathematics of algebras and coalgebras, the way these results can support methods and techniques for software development, as well as experience with the transfer of the resulting technologies into industrial practice. We encourage submissions in topics included or related to those listed below.

 * Abstract models and logics
   - Automata and languages
   - Categorical semantics
   - Modal logics
   - Relational systems
   - Graph transformation
   - Term rewriting

 * Specialised models and calculi
   - Hybrid, probabilistic, and timed systems
   - Calculi and models of concurrent, distributed, mobile, and
     context-aware computing
   - General systems theory and computational models (chemical,
     biological, etc.)

 * Algebraic and coalgebraic semantics
   - Abstract data types
   - Inductive and coinductive methods
   - Re-engineering techniques (program transformation)
   - Semantics of conceptual modelling methods and techniques
   - Semantics of programming languages

 * System specification and verification
   - Algebraic and coalgebraic specification
   - Formal testing and quality assurance
   - Validation and verification
   - Generative programming and model-driven development
   - Models, correctness and (re)configuration of
     hardware/middleware/architectures,
   - Process algebra

 * Corecursion in Programming Languages
    - Corecursion in logic / constraint / functional / answer set
      programming
    - Corecursive type inference
    - Coinductive methods for proving program properties
    - Implementing corecursion
    - Applications

 * Algebra and Coalgebra in quantum computing
    - Categorical semantics for quantum computing
    - Quantum calculi and programming languages
    - Foundational structures for quantum computing
    - Applications of quantum algebra

-- NEW TOPIC --

This edition of CALCO will feature a new topic, and submission of papers
in this area is particularly encouraged.

* String Diagrams and Network Theory
    - Combinatorial approaches 
    - Theory of PROPs and operads
    - Rewriting problems and higher-dimensional approaches
    - Automated reasoning with string diagrams
    - Applications of string diagrams
    - Connections with Control Theory, Engineering and Concurrency


-- SUBMISSION GUIDELINES --

Prospective authors are invited to submit full papers in English presenting original research. Submitted papers must be unpublished and not submitted for publication elsewhere. Experience papers are welcome, but they must clearly present general lessons learned that would be of interest and benefit to a broad audience of both researchers and practitioners. Starting with CALCO 2015, proceedings will be published in the Dagstuhl LIPIcs–Leibniz International Proceedings in Informatics series. Final papers should be no more than 15 pages long in the format specified by LIPIcs (http://www.dagstuhl.de/publikationen/lipics/anleitung-fuer-autoren/).
It is recommended that submissions adhere to that format and length. Submissions that are clearly too long may be rejected immediately. Proofs omitted due to space limitations may be included in a clearly marked appendix. Both an abstract and the full paper must be submitted by their respective submission deadlines.

A special issue of the open access journal Logical Methods in Computer Science (http://www.lmcs-online.org), containing extended versions of selected papers, is also being planned.

Submissions will be handled via EasyChair https://www.easychair.org/conferences/?conf=calco2015

-- BEST PAPER AND BEST PRESENTATION AWARDS --

Following from the successful trial at CALCO 2013, this edition of CALCO will feature two awards: a best paper award whose recipients will be selected by the PC before the conference and a best presentation award, elected by the participants.

-- IMPORTANT DATES --

Abstract submission:    March 22, 2015
Paper submission:       April 2, 2015
Author notification:    May 6, 2015
Final version due:      June 3, 2015

-- PROGRAMME COMMITTEE --

Samson Abramsky, University of Oxford, UK
Andrej Bauer, University of Ljubljana, SLO
Filippo Bonchi, CNRS and ENS Lyon, FR
Corina Cirstea, University of Southampton, UK
Andrea Corradini, University of Pisa, IT
Ross Duncan, University of Strathclyde, UK
Martín Escardó, University of Birmingham, UK
Dan Ghica, University of Birmingham, UK
Helle Hansen, Radboud University Nijmegen and CWI, NL
Ichiro Hasuo, University of Tokyo, JP
Bart Jacobs, Radboud University Nijmegen, NL
Bartek Klin, University of Warsaw, PL
Barbara König, University of Duisburg-Essen, D
Dexter Kozen, Cornell, US
Alexander Kurz, University of Leicester, UK
Paul-André Melliès, CNRS and University Paris VII, FR
Stefan Milus, University of Erlangen-Nürnberg, D
Larry Moss (co-chair), Indiana University, US
Dusko Pavlovic, University of Hawaii, US
Daniela Petrisan, ENS Lyon, FR
Damien Pous, ENS Lyon, FR
John Power, University of Bath, UK
Jan Rutten, Radboud University Nijmegen and CWI, NL
Lutz Schroeder, University of Erlangen-Nuernberg, D
Monika Seisenberger, University of Swansea, UK
Alexandra Silva, Radboud University Nijmegen, NL
Pawel Sobocinski (co-chair), University of Southampton, UK
Ana Sokolova, University of Salzburg, AT
Andrzej Tarlecki, University of Warsaw, PL 

-- ORGANISING COMMITTEE --

Alexandra Silva
Bart Jacobs
Nicole Messink
Sam Staton 

-- PUBLICITY --

Fabio Zanasi

-- LOCATION --

Nijmegen is the oldest city in the Netherlands and celebrated its 2,000th year of existence in 2005. It is situated in the eastern province of Gelderland, quite near to the German border. The latin name for Nijmegen, `Noviomagus´, is a reminder of its Roman past. `Noviomagus´ means `new market´ and refers to the right to hold a market as granted by the Romans. In the days of Charlemagne, the city was called `Numaga´; later on, this became `Nieumeghen´ and `Nimmegen´. However, citizens born and bred in Nijmegen speak affectionately of `Nimwegen´.

Nijmegen is one of the warmest cities of the Netherlands, especially during summer, when the highest temperatures in the country are usually measured in the triangle Roermond – Nijmegen – Eindhoven. The lack of north-south oriented mountain ranges in Europe make this area prone to sudden shifts in weather, giving the region a semi-continental climate.

-- SATELLITE WORKSHOPS --

The workshop is intended to enable presentation of work in progress and original research proposals. PhD students and young researchers are particularly encouraged to contribute. CALCO 2015 will run together with the CALCO Early Ideas Workshop, with dedicated Early Ideas sessions at the end of each conference day.

-- CALCO Early Ideas Overview --

The CALCO Early Ideas Workshop invites submissions on the same topics as the CALCO conference: reporting results of theoretical work on the mathematics of algebras and coalgebras, the way these results can support methods and techniques for software development, as well as experience with the transfer of the resulting technologies into industrial practice. The list of topics of particular interest is shown on the main CALCO 2015 page.

CALCO Early Ideas presentations will be selected according to originality, significance, and general interest, on the basis of submitted 2-page short contributions.  It can be work in progress, a summary of work submitted to a conference or workshop elsewhere, or work that in some other way might be interesting to the CALCO audience. A booklet with the accepted short contributions will be made available.

We encourage PhD students and young researchers to submit Early Ideas papers to the CALCO 2015 Easychair site as for ordinary submissions, mentioning in the abstract that the paper is to be considered for an Early Ideas talk.

------------------------------------------------------------------------------
New Year. New Location. New Benefits. New Data Center in Ashburn, VA.
GigeNET is offering a free month of service with a new server in Ashburn.
Choose from 2 high performing configs, both with 100TB of bandwidth.
Higher redundancy.Lower latency.Increased capacity.Completely compliant.
http://p.sf.net/sfu/gigenet
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
YuHui Lin | 21 Jan 13:50 2015
Picon
Picon

AVoCS 2015: First Call for Papers

---------------------------------------------------------------------
                      FIRST CALL FOR PAPERS

              The 15th International Workshop on 
          Automated Verification of Critical Systems 
                        AVoCS 2015

             1-4 September 2015, Edinburgh, UK

          https://sites.google.com/site/avocs15/
                avocs2015 <at> easychair.org
---------------------------------------------------------------------

IMPORTANT DATES
  Submission of abstract (full papers): 5th June 2015
  Submission of full papers: 12th June 2015
  Notification (full papers): 14th July 2015
  Submission of research idea papers: 7th August 2015
  Notification (research idea): 14th August 2015
  Early registration: 18th August 2015
  Submissions of final versions: 21st August 2015 

INVITED SPEAKERS
  Colin O'Halloran (D-RisQ & the University of Oxford)
  Don Sannella (Contemplate & the University of Edinburgh)

SPONSORS
  Formal Methods Europe (FME)
  The Scottish Informatics & Computer Science Alliance (SICSA)

BACKGROUND 
  The aim of Automated Verification of Critical Systems (AVoCS) 2015 
  is to contribute to the interaction and exchange of ideas among members 
  of the international research community on tools and techniques for the 
  verification of critical systems. 

SCOPE
  The subject is to be interpreted broadly and inclusively. It covers 
  all aspects of automated verification, including model checking, 
  theorem proving, SAT/SMT constraint solving, abstract interpretation, 
  and refinement pertaining to various types of critical systems which 
  need to meet stringent dependability requirements (safety-critical, 
  business-critical, performance-critical, etc.). Contributions that 
  describe different techniques, or industrial case studies are encouraged. 

  The technical programme will consist of invited and contributed talks 
  and also allow for short presentations of research ideas. The workshop 
  will be relatively informal, with an emphasis on discussion where special 
  discussion sessions will be organised around the research ideas presentations. 
  Topics include (but are not limited to):
    - Model Checking
    - Automatic and Interactive Theorem Proving
    - SAT, SMT or Constraint Solving for Verification
    - Abstract Interpretation
    - Specification and Refinement
    - Requirements Capture and Analysis
    - Verification of Software and Hardware
    - Specification and Verification of Fault Tolerance and Resilience
    - Probabilistic and Real-Time Systems
    - Dependable Systems
    - Verified System Development
    - Industrial Applications

WORKSHOPS
  AI4FM 2015: 1 September 2015 -- www.ai4fm.org/ai4fm-2015/

VENUE
  The event will be held in the International Centre for Mathematical Sciences 
  (ICMS) in the centre of the historic old town of Edinburgh - an UNESCO world
  heritage site. 

STUDENT GRANTS
  Thanks to sponsorships from FME and SICSA we can offer financial support for a 
  limited number of students registering for AVoCS in the form of a registration 
  fee waiver (full or partial). As this is limited, we ask the students that 
  would like to take the advantage of this support to submit a short application. 
  The details on how to apply will be available in due course from the AVoCS 
  webpage.

SUBMISSION DETAILS
   Submissions of full papers to the workshop must not have been published 
   or be concurrently considered for publication elsewhere. All submissions 
   will be peer-reviewed and judged on the basis of originality, contribution 
   to the field, technical and presentation quality, and relevance to the 
   workshop. Submissions are handled via Easychair: 

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

   The papers must be written in English and not exceed 15 pages and should 
   use the dedicated AVoCS 2015 EASST template available rom the the 
   following link (for LaTeX and Word):

       http://journal.ub.tu-berlin.de/eceasst

   AVoCS also encourages the submissions of research ideas in order to stimulate 
   discussions at the workshop. Reports on ongoing work or surveys on work 
   published elsewhere are welcome. The Programme Committee will select 
   research ideas on the basis of submitted abstracts according to significance 
   and general interest. Research ideas must be written in English and not exceed 
   2 pages using the EASST template. The presentation of these ideas will be organised 
   around discussions, where the presenter should also prepare a set of question in 
   which the audience will discuss.

PROCEEDINGS
  At the workshop, pre-proceedings will be available in the form of a Heriot-Watt 
  University Technical Report; this report will also include the research ideas.
  After the workshop, the authors of accepted full papers will have about one 
  month in order to revise their papers for publication in the workshop post-
  proceedings which will appear in the Electronic Communications of the EASST 
  Open Access Journal. Research ideas will not be part of the proceedings in the 
  Open Access Journal.

SPECIAL SCP JOURNAL ISSUE
  Authors of a selection of the best papers presented at the workshop will be 
  invited to submit extended versions of their work for publication in a 
  special issue of Elsevier's journal Science of Computer Programming.

PROGRAM COMMITTEE  
  Ernie Cohen, University of Pennsylvania, USA
  Ewen Denney, NASA Ames, USA
  Jean-Christophe Filliatre, CNRS, France
  Michael Goldsmith, University of Oxford, UK
  Gudmund Grov, Heriot-Watt University, UK (co-chair)
  Keijo Heljanko, Aalto University, Finland
  Mike Hinchey, University of Limerick, Ireland
  Marieke Huisman, University of Twente, Netherlands
  Andrew Ireland, Heriot-Watt University, UK (co-chair)
  Gerwin Klein, NICTA/UNSW, Australia
  Thierry Lecomte, ClearSy, France
  Peter Gorm Larsen, Aarhus University, Denmark 
  Panagiotis (Pete) Manolios, Northeastern University, USA
  Stephan Merz, INRIA Nancy & LORIA, France
  Jaco van de Pol, University of Twente, Netherlands
  Markus Roggenbach, Swansea University, UK
  Marco Roveri, FBK, Italy
  Thomas Santen, Microsoft Research, Germany
  Bernard Steffen, Technical University Dortmund, Germany
  Jan Strejček, Masaryk University, Czech Republic
  Jun Sun, Singapore University of Technology and Design, Singapore
  Tayssir Touili, LIAFA, CNRS & University Paris Diderot, France
  Helen Treharne, University of Surrey, UK
  Laurent Voisin, Systerel, France
  Angela Wallenburg, Altran, UK
  John Wickerson, Imperial College London, UK
  Peter Ölveczky, University of Oslo, Norway

ORGANISERS 
  Gudmund Grov, Heriot-Watt University, UK
  Andrew Ireland, Heriot-Watt University, UK
  Yuhui Lin, Heriot-Watt University, UK (Local arrangements and publicity chair)

STEERING COMMITTEE 
  Michael Goldsmith, University of Oxford, UK
  Stephan Merz, INRIA Nancy & LORIA, France
  Markus Roggenbach, Swansea University, UK

----- 
We invite research leaders and ambitious early career researchers to 
join us in leading and driving research in key inter-disciplinary themes. 
Please see www.hw.ac.uk/researchleaders for further information and how
to apply.

Heriot-Watt University is a Scottish charity
registered under charity number SC000278.

------------------------------------------------------------------------------
New Year. New Location. New Benefits. New Data Center in Ashburn, VA.
GigeNET is offering a free month of service with a new server in Ashburn.
Choose from 2 high performing configs, both with 100TB of bandwidth.
Higher redundancy.Lower latency.Increased capacity.Completely compliant.
http://p.sf.net/sfu/gigenet
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Geoff Sutcliffe | 13 Jan 16:32 2015
Picon

10th Ershov Informatics Conference, Call for Papers

CALL FOR PAPERS
PSI: 10th Ershov Informatics Conference
25 - 27 August 2015, Innopolis, Kazan, Russia
http://easychair.org/smart-program/PSI2015/

The Ershov Informatics Conference (the PSI Conference Series, 10th edition) 
is the premier international forum in Russia for research and applications 
in computer, software and information sciences. The conference brings together 
academic and industrial researchers, developers and users to discuss the most 
recent topics in the field. PSI provides an ideal venue for setting up research 
collaborations between the rapidly growing Russian informatics community and 
its international counterparts, as well as between established scientists and 
younger researchers.

Local Organizers

Tanya Stanko
Innopolis University
Inna Baskakova
Innopolis University

Publicity Chairs

Timur Tsiunchuk
Innopolis University
Salvatore Distefano
Politecnico di Milano

Conference Chairs 

Bertrand Meyer
ETH, Zurich
Irina Virbitskaite
A.P. Ershov Institute, Novosibirsk

Steering Committee 

Dines Bjorner 
Technical University of Denmark 
Manfred Broy
Technische Universitaet Muenchen 
Victor Ivannikov
Institute for System Programming, Russian Academy of Sciences 
Ugo Montanari 
University of Pisa

Programme Committee Chairs 

Manuel Mazzara
Innopolis University
Andrei Voronkov
The University of Manchester

Keynote speakers

Hans-Ulrich Heiss, TUB, Germany
Jane Hillston, University of Edinburgh, UK
Helmut Veith, Vienna University of Technology, Austria

Conference Topics

1. Foundations of Program and System Development and Analysis
* Specification, validation, and verification techniques.
* Program analysis, transformation and synthesis.
* Semantics, logic and formal models of programs.
* Partial evaluation, mixed computation, abstract interpretation, compiler 
  construction.
* Theorem proving and model checking.
* Concurrency theory.
* Static program analysis.
* Modeling and analysis of real-time and hybrid systems.
* Computer models and algorithms for bioinformatics.

2. Programming Methodology and Software Engineering
* Object-oriented, aspect-oriented, component-based and generic programming.
* Programming by contract.
* Program and system construction for parallel and distributed computing.
* Constraint programming.
* Multi-agent technology.
* System re-engineering and reuse.
* Integrated programming environments.
* Software architecture.
* Software development and testing.
* Model-driven system/software development.
* Agile software development.
* Software engineering methods and tools.
* Service engineering, service oriented architecture.
* Reverse engineering.
* Reflection techniques.
* Software bugs, aging and reliability models and countermeasures.
* Program understanding and visualization.

3. Information Technologies
* Data models. 
* Database and information systems.
* Data mining, analytics.
* Knowledge-based systems and knowledge engineering.
* Bioinformatics engineering.
* Ontologies and semantic Web.
* Digital libraries, collections and archives, Web publishing.
* Peer-to-peer data management.

More generally, the conference welcomes novel scientific contributions in 
software-related areas, and application papers showing practical applications 
of research results.

Important Dates

* April 16, 2015: abstract submission
* April 23, 2015: submission deadline
* May 31, 2015: notification of acceptance
* August 25-27, 2015: the conference dates
* November 1, 2015: camera ready papers due

Programme Committee Members

Farhad Arbab, CWI and Leiden University, Netherlands
David Aspinall, Univ. of Edinburgh, UK
Marcello Maria Bersani, Politecnico di Milano, Italy 
Eike Best, Univ. of Oldenburg, Germany
Nikolaj Bjrner, Microsoft Research, Redmond, USA
Andrea Calì, Birbeck College, UK
Mauro Caporuscio, Linnaeus University, Sweden
Néstor Cataño, Madeira Univ., Portugal
Gabriel Ciobanu, Romanian Academy, Iasi, Romania
Volker Diekert, Univ. Stuttgart, Germany
Salvatore Distefano, Politecnico di Milano, Italy
Nicola Dragoni, DTU, Denmark and Örebro Univ., Sweden
Schahram Dustdar, Vienna Univ. Technology, Austria
Dieter Fensel, STI Innsbruck, Austria 
Carlo Furia, ETH, Switzerland
Carlo Ghezzi, Politecnico di Milano, Italy 
Sergei Gorlatch, Univ. Muenster, Germany 
Jan Friso Groote, Eindhoven Univ. Tech., The Netherlands 
Arie Gurfinkel, Carnegie Mellon Univ., US 
Cliff Jones, Newcastle Univ., UK
Joost-Pieter Katoen, RWTH Aachen Univ., Germany
Konstantin Korovin, Univ. Manchester, UK 
Maciej Koutny, Newcastle Univ., UK 
Laura Kovacs, Chalmers Univ. Tech., Gothenburg, Sweden 
Gregory Kucherov, CNRS/LIGM, Marne-la-Vallee, France
Johan Lilius, Abo Akademi Univ., Turku, Finland
Anthony Widjaja Lin, Yale-NUS College, Singapore
Zhiming Liu, Birmingham City University 
Jan Madsen, DTU Copenhagen, Denmark
Rupak Majumdar, MPI, Kaiserslautern, Germany 
Klaus Meer, Tech. Univ. Cottbus, Germany
Hernán Melgratti, Univ. de Buenos Aires, Argentina
Torben Mogensen, Univ. Copenhagen, Denmark
Peter Mosses, Swansea Univ., UK
Martin Nordio, ETH, Switzerland
José R. Paramá, Univ. A Coruña, Spain
Wojciech Penczek, Inst. Comp. Sci., Warsaw, Poland
Peter Pepper, TU Berlin, Germany
Alexander Petrenko, ISP RAS, Moscow, Russia 
Paul Pettersson, Mälardalen Univ., Sweden
Nadia Polikarpova, MIT, USA  
Qiang Qu, Innopolis University, Russia
Andrey Rybalchenko, TUM, Munchen, Germany
Wolfgang Reisig, Humboldt Univ., Berlin, Germany
Davide Sangiorgi, Univ. of Bologna, Italy
Natalia Sidorova, Technische Univ. Eindhoven, Netherlands
Giancarlo Succi, University of Bolzano, Italy
Klaus-Dieter Schewe, SW Competence C., Hagenberg, Austria
Max Talanov, Kazan Federal Universty, Russia
Mark Trakhtenbrot, Holon Inst. of Technology, Israel
Kishor S. Trivedi, Duke University, USA
Domagoj Vrgoc, Center for Semantic Web Research, Chile
Sergey Zykov, Higher School of Economics, Russia  

Submissions

There are three categories of submissions:
* Regular  papers  describing  fully  developed  work  and complete results 
  (15 pages / 30 minute talks).
* Short papers reporting on interesting work in progress and/or preliminary 
  results (9 pages / 15 minute talks).
* System and experimental papers describing implementation or evaluation of 
  experimental systems and containing a link to a working system 
  (7 pages / 10 minute presentations). 

Submissions should:
* Present original contributions that have not been previously published and 
  are not being submitted to another publication. 
* Clearly state the problem being addressed, the goal of the work, the results 
  achieved, and the relation to other work.
* Be in good-quality English, in a form that can be immediately published 
  without revision.
* Be sent electronically, as a PDF file formatted according to Springer LNCS 
  Instructions for Authors: http://www.springeronline.com) through the 
  submissions link to the conference website 
       https://easychair.org/conferences/?conf=psi2015
  no later than April 23, 2015.

It is permissible to include or link to an appendix listing detailed results 
or supporting data that do not fit within the page limits, as long as the 
paper can be evaluated without reading this appendix.

At least one author of each accepted paper must register, attend the conference 
and present the paper.

Conference Proceedings

Preliminary proceedings will be available at the conference. Final versions of 
invited and accepted papers will be published by Springer-Verlag after the 
conference in the Lecture Notes in Computer Science series. Proceedings of 
previous PSIs are volumes 1181, 1755, 2244, 2890, 4378, 5947 and 7162 of LNCS.

Location

PSI 2015 will take place in the Korston conference hall in Kazan, one of the 
oldest, largest and most beautiful cities in Russia, with a rich multicultural 
heritage and architectural treasures recognized as a UNESCO World Heritage 
Site. Kazan was recently noted by TripAdvisor as one of the destination on the 
rise. A social and cultural program will enable participants and companions to 
discover the beauty of Kazan. Pre- and post-conference tours are available upon 
request.

Travelling

You can fly directly to Kazan through Moscow or directly from a number of 
international destinations such as Helsinki. Trains are also available from 
Moscow.

Conference Secretary

Inna Baskakova
Innopolis University 
42 Profsoyuznaya str., 420100, Kazan, Russia 
Tel: +7 (843) 203-92-53 (Kazan)
i.baskakova <at> innopolis.ru

------------------------------------------------------------------------------
New Year. New Location. New Benefits. New Data Center in Ashburn, VA.
GigeNET is offering a free month of service with a new server in Ashburn.
Choose from 2 high performing configs, both with 100TB of bandwidth.
Higher redundancy.Lower latency.Increased capacity.Completely compliant.
http://p.sf.net/sfu/gigenet
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Ashish Darbari | 16 Jan 15:43 2015
Picon

Formal Verification Opportunity at Imagination Technologies UK

All

If it is of interest for budding formal verification engineers, my group is looking for a Graduate Engineer to work in the area of formal hardware verification at our UK office. Please get in touch with me if you're interested and for details of the opening see: Vacancy Detail - Imagination Technologies




Ashish

Principal Hardware Design Engineer
Imagination Technologies
Kings Langley WD4 8LZ UK 
------------------------------------------------------------------------------
New Year. New Location. New Benefits. New Data Center in Ashburn, VA.
GigeNET is offering a free month of service with a new server in Ashburn.
Choose from 2 high performing configs, both with 100TB of bandwidth.
Higher redundancy.Lower latency.Increased capacity.Completely compliant.
http://p.sf.net/sfu/gigenet
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Piotr Trojanek | 12 Jan 14:07 2015
Picon

Weakest precondition of While as the least fixpoint

Dear all,

I am still experimenting with programming language semantics using
both HOL Light and HOL4. My question is not specific to any of these
two implementations, but I could not find any better place to ask,
sorry.

I am following the HOL Light tutorial, where the weakest preconditions
`wp`are derived from inductively defined big-step operational
semantics. I want to prove that `wp (While e c) q` is the least fixed
point:

wp (While e c) q = lfp (λw. e AND wp c w OR NOT e AND q)

but I can only prove that the right hand side implies the left hand
side. Can you point me to a proof, ideally in HOL, of the above
equivalence?

The code from HOL Light tutorial is similar to the what Harrison
describes in "Formalizing Dijkstra." He says "We could in fact prove
that `Do gcs` is the least fixpoint," but do not give a proof (page
12). Dijkstra and Scholten give a proof in their "Predicate calculus
and program semantics," but they heavily depend on their own notation
and I found their reasoning difficult to mechanize in HOL. On the
other extreme, HOL mechanizations of the refinement calculus simply
define the weakest precondition for While as the least fixpoint.

--

-- 
Piotr Trojanek

------------------------------------------------------------------------------
New Year. New Location. New Benefits. New Data Center in Ashburn, VA.
GigeNET is offering a free month of service with a new server in Ashburn.
Choose from 2 high performing configs, both with 100TB of bandwidth.
Higher redundancy.Lower latency.Increased capacity.Completely compliant.
vanity: www.gigenet.com
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Sophie Tison | 8 Jan 14:29 2015
Picon

RTA 2015: 2nd CFP

==================================================================
              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; planning; 
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.

Invited Speakers:
Helene Kirchner, INRIA
Grigore Rosu, U. Illinois at Urbana-Champaign
Carolyn Talcott, SRI International

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

Attachment (smime.p7s): application/pkcs7-signature, 3818 bytes
------------------------------------------------------------------------------
Dive into the World of Parallel Programming! The Go Parallel Website,
sponsored by Intel and developed in partnership with Slashdot Media, is your
hub for all things parallel software development, from weekly thought
leadership blogs to news, videos, case studies, tutorials and more. Take a
look and join the conversation now. http://goparallel.sourceforge.net
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Gergely Buday | 4 Jan 15:38 2015
Picon

hardware verification

Hi,

my question is not strictly about the HOL family of provers but since
the most successful application area for HOL is hardware verification
I think this is the right place to ask.

There is a research on functional, i.e. purely functional description
languages: CλaSH. reFLect, Lava, Confluence, HDCaml, Bluespec, SAFL
etc.

http://www.hindawi.com/journals/isrn/2012/271836/ wrote in 2012 that

"There are only few published circuit designs developped using FHLs"

Is this because the functional description languages are not mature
yet, or simply the hardware industry does not want to move from the
used and proven methods of VHDL, Verilog and SystemC, despite of their
verbosity? Also there can be a resistance of engineers to learn a
non-C-like language?

- Gergely

------------------------------------------------------------------------------
Dive into the World of Parallel Programming! The Go Parallel Website,
sponsored by Intel and developed in partnership with Slashdot Media, is your
hub for all things parallel software development, from weekly thought
leadership blogs to news, videos, case studies, tutorials and more. Take a
look and join the conversation now. http://goparallel.sourceforge.net
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Julian Tschannen | 19 Dec 16:36 2014
Picon

LASER Summer School 2015 --- Concurrency: the next frontiers

LASER Summer School on Software Engineering

Concurrency: the next frontiers
September 6-12, 2015 - Elba Island, Italy

http://laser.inf.ethz.ch/2015/

Application deadline: March 31, 2015

Goals
--------

The LASER summer school, organized by the ETH Chair of Software
Engineering, brings together the concepts and practice of software
engineering in the idyllic setting of the Elba Island off the coast of
Tuscany, easily reachable by air, car, bus or train.

The LASER school is intended for professionals from the industry
(engineers and managers) as well as university researchers, including
PhD students. Participants learn about the most important software
technology advances from the pioneers in the field. The school's focus
is applied, although theory is welcome to establish solid foundations.
The format of the school favors extensive interaction between
participants and speakers.

Topic and speakers
-------------------------

Concurrent and parallel computation is the locus of many of the
toughest challenges in computer science and software engineering.
The school brings together concurrency experts representing many
different approaches and views, and presents their answers to these
challenges. It is a unique opportunity to familiarize yourself with
the most important results in concurrency and get familiar with
work at the frontier of concurrency research.

The speakers are among the most respected experts in the field:

- Manfred Broy, TU München
- Maurice Herlihy, Brown University
- Jeff Kramer, Imperial College London
- Bertrand Meyer, ETH Zürich
- Jayadev Misra, University of Texas
- David Parnas, Middle Road Software, Inc

How to apply?
-----------------

Use the online registration form available on the LASER website
http://laser.inf.ethz.ch/2015. Registration is open until March 31,
2015. The number of participants is strictly limited to ensure quality
interaction with the lecturers and the rest of the audience. For more
information, visit our website or contact the organizers: se-laser at
lists.inf.ethz.ch

Venue
--------

The school takes place at the magnificent Hotel del Golfo
(http://www.hoteldelgolfo.it/) in Golfo di Procchio, Elba. Along with an
intensive scientific program, participants will have time to enjoy the
natural and cultural riches of this history-laden jewel of the
Mediterranean.

------------------------------------------------------------------------------
Dive into the World of Parallel Programming! The Go Parallel Website,
sponsored by Intel and developed in partnership with Slashdot Media, is your
hub for all things parallel software development, from weekly thought
leadership blogs to news, videos, case studies, tutorials and more. Take a
look and join the conversation now. http://goparallel.sourceforge.net
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Klaus Havelund | 23 Dec 16:16 2014
Picon
Picon

[fm-announcements] First CFP: CRV15 - 2nd Competition on Runtime Verification


CRV 2015
The 2nd International Competition on Runtime Verification, 
held with RV 2015, September 22 – 25, 2015 Vienna, Austria


CRV-2015 is the 2nd International Competition on Runtime Verification and is part of the 15th International 
Conference on Runtime Verification. The event will be held in September 2015, in Vienna, Austria. CRV-2015 will 
draw attention to the invaluable effort of software developers and researchers who contribute in this field by 
providing the community with new or updated tools, libraries and frameworks for the instrumentation and runtime
verification of software.

Runtime Verification is a verification technique for the analysis of software at execution-time based on extracting
information from a running system and checking if the observed behaviors satisfy or violate the properties of interest.
During the last decade, many important tools and techniques have been developed and successfully employed. However, 
there is a pressing need to compare such tools and techniques, since we currently lack a common benchmark suite as well
as scientific evaluation methods to validate and test new prototype runtime verification tools. 

The main aims of CRV-2015 are to:

• Stimulate the development of new efficient and practical runtime verification tools and the maintenance 
          and improvement of the already developed ones.
• Produce a benchmark suite for runtime verification tools, by sharing case studies and programs that 
          researchers and developers can use in the future to test and to validate their prototypes.
• Discuss the metrics employed for comparing the tools.
• Provide a comparison of the tools on different benchmarks and evaluate them using different criteria.
• Enhance the visibility of presented tools among the different communities (verification, software 
          engineering, cloud computing and security) involved in software monitoring.

Please direct any enquiries to the competition co-organizers (crv15.chairs <at> imag.fr)

• Yliès Falcone (Université Joseph Fourier, France).
• Dejan Nickovic (AIT Austrian Institute of Technology GmbH, Austria).
• Giles Reger (University of Manchester, UK).
• Daniel Thoma (University of Luebeck, Germany).

CRV-2015 Jury

The CSRV Jury will include a representative for each participating team and the competition chairs. The Jury will be consulted at each stage of the competition to ensure that the rules set by the competition chairs are fair and reasonable.

Call for Participation

The main goal of CRV 2015 is to compare tools for runtime verification. We invite and encourage the participation with benchmarks and tools for the competition.The competition will consist of three main tracks based on the input language used:

• Track on monitoring Java programs (online monitoring).
• Track on monitoring C programs (online monitoring).
• Track on monitoring of traces (offline monitoring).

The competition will follow three phases:

• Benchmarks/Specification collection phase - the participants are invited to submit their benchmarks 
          (C or Java programs and/or traces). The organizers will collect them in a common repository 
          (publicly available). The participants will then train their tools using the shared benchmarks.
• Monitor collection phase - the participants are invited to submit their monitors. The participants with 
          the tools/monitors that meet the qualification requirements will be qualified for the evaluation phase.
• Evaluation phase - the qualified tools will be evaluated on the submitted benchmarks and they will be 
          ranked using different criteria (i.e., memory utilization, CPU utilization, ...). The final results 
          will be presented at the RV 2015 conference.

The detailed description of each phase will be available on the RV 2015 website at http://rv2015.conf.tuwien.ac.at.

 

Expected Important Dates

January 15, 2015: Declaration of intent (email: crv15.chairs <at> imag.fr)
March 1, 2015 Submission deadline for benchmark programs and the properties to be monitored
March 15, 2015 Tool training starts by participants
May 15, 2015 Monitor submission
June 15, 2015 Notifications
At RV 2015 Presentation of results

———


---
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 
------------------------------------------------------------------------------
Dive into the World of Parallel Programming! The Go Parallel Website,
sponsored by Intel and developed in partnership with Slashdot Media, is your
hub for all things parallel software development, from weekly thought
leadership blogs to news, videos, case studies, tutorials and more. Take a
look and join the conversation now. http://goparallel.sourceforge.net
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Cyber Security Symposium 2015 Call for Papers

I apologize if you receive multiple copies of this.

-jimaf

 

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

CALL FOR ABSTRACTS

Cyber Security Symposium: Your Security, Your Future

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

 

April 7-8, 2015 - - - Coeur d’Alene, Idaho, U.S.A.

 

http://www.cybersecuritysymposium.com

 

Key Dates

Abstract Submission Deadline: January 16, 2015

Presenter Notification: February 3, 2015

Early Registration Deadline: February 6, 2015

 

Introduction

The 2015 Cyber Security Symposium is an opportunity for academic researchers from all disciplines, software developers, and system developers from industry and government to meet and discuss state-of-the-art and state-of-the-practice research, technologies, and processes related to cyber security.  The symposium seeks submissions from academia, industry and government presenting novel research, case studies, and best practices on all practical and theoretical aspects of cyber security.

 

We are interested in presentations and papers with topics including, but not limited to:

·                   Network Security

·                   Secure Coding Practices

·                   Software Analysis

·                   Security Policies

·                   Economic Impacts of Security

·                   Privacy

·                   Sociological and Human Factor Aspects of Security

·                   Critical Infrastructure Security

·                   Transportation System Security

·                   Power grid/Smart Grid security

·                   System Security Case Studies

 

Electronic Submission

Abstract submissions up to 500 words in length are being accepted at this time.  To submit your abstract, please go to the submission site at: https://www.easychair.org/conferences/?conf=cybersec15

 

Each abstract submission should be submitted with an understanding that, if accepted, at least one of the authors must attend the conference to present the work.

 

All authors of accepted abstracts will be given the opportunity to submit full research papers (up to 10 pages) and extended abstracts (up to 4 pages) in the form of position papers, discussions of new technologies from industry, and discussions of current hot topics/needs in cyber security to be considered for future publication in a Springer Verlag publication. 

------------------------------------------------------------------------------
Download BIRT iHub F-Type - The Free Enterprise-Grade BIRT Server
from Actuate! Instantly Supercharge Your Business Reports and Dashboards
with Interactivity, Sharing, Native Excel Exports, App Integration & more
Get technology previously reserved for billion-dollar corporations, FREE
http://pubads.g.doubleclick.net/gampad/clk?id=164703151&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Gmane