Adnan Rashid | 23 Jun 06:36 2016
Picon

About proof of a Theorem (Integrability of a Vector Function)

Dear all,

I am working in HOL Light and I want to verify the following theorem regarding integrability of a vector function:

f integrable_on (:real^1) ==> f integrable_on {t | a <= drop t}

which says that if a function is integrable on (-inf, inf) then it is integrable on its subset which looks true to me.

Can anyone guide me in its proof?

Thanks.

--
Adnan


------------------------------------------------------------------------------
Attend Shape: An AT&T Tech Expo July 15-16. Meet us at AT&T Park in San
Francisco, CA to explore cutting-edge tech and listen to tech luminaries
present their vision of the future. This family event has something for
everyone, including kids. Get more information and register today.
http://sdm.link/attshape
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Ada | 22 Jun 10:21 2016

A question about the theorem in HOL4?

    Hi,guys
    I am working with HOL4. 
    FST is in pairTheory, its definition is   
[FST] Theorem |- ∀x y. FST (x,y) = x But, When I use it like following: val n = FST (1,2); It responses: ! Toplevel input:
! val n = FST (1,2);
!         ^^^
! Type clash: expression of type
!   thm
! cannot have type
!   'a -> 'b What is the reason? Does anyone know how to use it?
        Thanks!
------------------------------------------------------------------------------
Attend Shape: An AT&T Tech Expo July 15-16. Meet us at AT&T Park in San
Francisco, CA to explore cutting-edge tech and listen to tech luminaries
present their vision of the future. This family event has something for
everyone, including kids. Get more information and register today.
http://sdm.link/attshape
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Jasmin Blanchette | 21 Jun 15:18 2016
Picon

ITP 2016: Call for participation

The 7th International Conference on Interactive Theorem Proving
22 to 27 August 2016 in Nancy, France
https://itp2016.inria.fr

Early registration deadline: 30 June
Main conference: 22 August to 25 August (morning)
Affiliated events: 25 August (afternoon) to 27 August

ITP is the premier international conference for researchers from all areas of
interactive theorem proving and its applications. The program committee
accepted 27 regular papers and 5 rough diamonds this year:

    https://itp2016.inria.fr/program/

There will be invited talks by

    Viktor Kuncak (EPFL)
    Grant Olney Passmore (Aesthetic Integration and University of Cambridge)
    Nikhil Swamy (Microsoft Research)

The following affiliated events will take place after the main conference:

    Coq Workshop 2016
    Isabelle Workshop 2016
    Mathematical Components, an Introduction

Up-to-date information and online registration can be found at

    https://itp2016.inria.fr

------------------------------------------------------------------------------
Attend Shape: An AT&T Tech Expo July 15-16. Meet us at AT&T Park in San
Francisco, CA to explore cutting-edge tech and listen to tech luminaries
present their vision of the future. This family event has something for
everyone, including kids. Get more information and register today.
http://sdm.link/attshape
Thomas Tuerk | 21 Jun 11:29 2016
Picon

Re: How to show the function body in ML?

Hi Ada,

you can't print the definition from the ML REPL. I expect you use
PolyML. In this case look into the file "POLYML_DIR/basis/List.sml".
There you will find the following definition.

fun find _ [] = NONE
| find f (a::b) = if f a then SOME a else find f b

Best

Thomas

On 21.06.2016 11:18, Ada wrote:
>     Hi,guys
>     I am working with HOL4. 
>     I finded a function "find" in ML Structure list,and I wanted to see
> the function body of "find". I printed :
>    - find;
>    > > val it = fn : string -> ((string * string) * (thm * class)) list
>    The result only shows the types of the function.
>    Its description in ML library is:
>    [*find* p xs] applies f to each element x of xs, from left to  right
> until p(x) evaluates to true; returns SOME x if such an x  exists
> otherwise NONE.
>     But,the function body or the definition of function doesn't exist.  
>     Does anyone know how to show the function body ?
>     Thanks!
> 
> 
> ------------------------------------------------------------------------------
> Attend Shape: An AT&T Tech Expo July 15-16. Meet us at AT&T Park in San
> Francisco, CA to explore cutting-edge tech and listen to tech luminaries
> present their vision of the future. This family event has something for
> everyone, including kids. Get more information and register today.
> http://sdm.link/attshape
> 
> 
> 
> _______________________________________________
> hol-info mailing list
> hol-info <at> lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
> 

------------------------------------------------------------------------------
Attend Shape: An AT&T Tech Expo July 15-16. Meet us at AT&T Park in San
Francisco, CA to explore cutting-edge tech and listen to tech luminaries
present their vision of the future. This family event has something for
everyone, including kids. Get more information and register today.
http://sdm.link/attshape
Andrea Rosa | 21 Jun 00:14 2016
Picon

Call for Participation: 3rd Virtual Machine Meetup, September 1-2, Lugano, Switzerland


                   Call for Participation: VMM’16
                   ==============================

                     3rd Virtual Machine Meetup

                       Co-located with PPPJ
              September 1-2, 2016, Lugano, Switzerland

                   http://vmmeetup.github.io/2016/



The 3rd Virtual Machine Meetup (VMM'16) is a venue for discussing the latest
research and developments in the area of managed language execution. It will be
held on 1st and 2nd of September at the Università della Svizzera italiana
(USI), Lugano, Switzerland and is part of the Managed Languages & Runtimes Week
2016 (http://manlang16.inf.usi.ch/, other colocated events are PPPJ'16 and
JTRES'16, room Auditorium from 9am - 5pm). We welcome presentations of new
research results, experience reports, as well as position statements that can
lead to interesting discussions.


Topics include, but are not limited to:

- Programming language design
- Dynamic and static program analysis
- Compiler construction
- Managed runtime architectures
- Data processing engines
- Distributed execution environments

To participate, please email
thomas.wuerthinger <at> oracle.com<mailto:thomas.wuerthinger <at> oracle.com> stating your wish to
attend, and your name and affiliation as you wish to have them on your name
badge. There are limited participant slots due to the constraints of the room,
so please register early, and by July 20th the latest.

If you would like to give a presentation, please email Thomas with a title
(max. 100 characters) and abstract (max. 400 characters). We may ask for
additional information from you before making the program decision.
Presentation slots are either 30 minutes (long) or 15 minutes (short)
including Q/A.


Important dates:

- Submissions:  July 10, 2016
- Author notification: July 17, 2016
- Registration for participation: July 20, 2016
- Virtual machine Meetup: Sep 1st + 2nd 2016 at USI Lugano
- Social Event: Sep 3rd 2016, optional


Program committee:

- Stefan Marr, JKU Linz, Austria
- Matthias Grimmer, JKU Linz, Austria
- Laurence Tratt, King's College London
- Thomas Wuerthinger, Oracle Labs Switzerland

As an optional social event, we will plan this year for Saturday the 3rd of
September a trip to the Lake Como - a gorgeous lake in Italy close to Lugano.
Please let us know whether you intend to participate for planning purposes.
------------
Andrea Rosà
PhD student - Teaching assistant
Faculty of Informatics - 2nd floor
Università della Svizzera italiana (USI)
Via G. Buffi 13
CH-6904 Lugano
Switzerland
(e) andrea.rosa <at> usi.ch<mailto:andrea.rosa <at> usi.ch>
(p) +41 58 666 4455 ext. 2183
(w) http://www.inf.usi.ch/phd/rosaa/


------------------------------------------------------------------------------
Attend Shape: An AT&T Tech Expo July 15-16. Meet us at AT&T Park in San
Francisco, CA to explore cutting-edge tech and listen to tech luminaries
present their vision of the future. This family event has something for
everyone, including kids. Get more information and register today.
http://sdm.link/attshape
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Heiko Becker | 16 Jun 11:01 2016
Picon

Fwd: Re: HOL-Light Beginner Questions


-------- Forwarded Message -------- Subject: Date: From: To: CC:
Re: [Hol-info] HOL-Light Beginner Questions
Thu, 16 Jun 2016 10:59:44 +0200
Heiko Becker <heikobecker92 <at> gmail.com>
Ramana Kumar <Ramana.Kumar <at> cl.cam.ac.uk>
hol-info <hol-info <at> lists.sourceforge.net>



On 06/16/2016 01:57 AM, Ramana Kumar wrote:
I expect it could be because the Boolean constants are spelled "T" and "F" rather than "true" and "false" in the logic, so the latter are being treated as free variables.


Thank you for your explanation. I am getting closer to getting my definition working.
I have changed it as follows:

let sstep_RULES,sstep_INDUCT,sstep_CASES = new_inductive_definition
  `(!x e s env v. exp_eval e env = v ==> sstep (Ass x e s) env s (upd_env x v env)) /\
  (!c s t env. bval c env = T ==> sstep (Ite c s t) env s env) /\
  (!c s t env. bval c env = F ==> sstep (Ite c s t) env t env)`;;

But now HOL-Light complains about some construct not being a variable:
Exception: Failure "dest_var: not a variable".

Can you maybe help me again?

Best regards,

Heiko

On 16 June 2016 at 01:09, Heiko Becker <heikobecker92 <at> gmail.com> wrote:

My formalization:

let exp_INDUCT, exp_REC= define_type
   "exp = Var num
   | Const real
   | Plus exp exp
   | Sub exp exp
   | Mult exp exp
   | Div exp exp";;

let exp_eval_SIMPS = define
   `(exp_eval (Var x) E = E x) /\
   (exp_eval (Const r) E = r) /\
   (exp_eval (Plus e1 e2) E = (exp_eval e1) E + (exp_eval e2) E) /\
   (exp_eval (Sub e1 e2) E = (exp_eval e1) E - (exp_eval e2) E) /\
   (exp_eval (Mult e1 e2) E = (exp_eval e1) E * (exp_eval e2) E) /\
   (exp_eval (Div e1 e2) E = (exp_eval e1) E / (exp_eval e2) E)`;;

let bexp_INDUCT, bexp_REC = define_type
   "bexp = leq exp exp
         | less exp exp";;

let bval_SIMPS = define
   `(bval (leq e1 e2) (E:num->real) = (exp_eval e1 E) <= (exp_eval e2 E)) /\
   (bval (less e1 e2) E = (exp_eval e1 E) < (exp_eval e2 E))`;;

let cmd_INDUCT, cmd_REC = define_type
   "cmd = Ass num exp cmd
        | Ite bexp cmd cmd
        | Nop";;

let upd_env_simps1 = define
   `upd_env (x:num) (v:real) (E:num->real) =(\y. if y = x then v else E
y)`;;

let sstep_RULES,sstep_INDUCT,sstep_CASES = new_inductive_definition
   `(!x e s E v. exp_eval e E = v ==> sstep (Ass x e s) E s (upd_env x v
E)) /\
   (! c s t E. bval c E = true ==> sstep (Ite c s t) E s E) /\
   (! c s t E. bval c E = false ==> sstep (Ite c s t) E t E)`;;


When loading the sstep definitions I get the following failure:
     Exception: Failure "new_definition: term not closed".


Forwarding my message. Send from wrong mail account intially.

------------------------------------------------------------------------------
What NetFlow Analyzer can do for you? Monitors network bandwidth and traffic
patterns at an interface-level. Reveals which users, apps, and protocols are 
consuming the most bandwidth. Provides multi-vendor support for NetFlow, 
J-Flow, sFlow and other flows. Make informed decisions using capacity planning
reports. http://pubads.g.doubleclick.net/gampad/clk?id=1444514421&iu=/41014381
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Peter Csaba Ölveczky | 7 Jun 17:10 2016
Picon
Picon

[Memocode] CfP: Formal Techniques for Safety-Critical Systems (FTSCS'16)

To unsubscribe, just enter your email address at the bottom of the following page:  https://lists.cs.columbia.edu/mailman/listinfo/memocode
and click "Unsubscribe or edit options."
On the next page, just click "Unsubscribe." You do not have to register or enter a password.

Unsubscribe: <mailto:memocode-unsubscribe <at> lists.cs.columbia.edu>
---------------------------------------------------------------------
                       Call for Papers

                          FTSCS 2016

5th International Workshop on Formal Techniques for Safety-Critical Systems

                   Tokyo, November 14/15, 2016
              (satellite workshop of ICFEM 2016)

                    http://www.ftscs.org

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

*** Science of Computer Programming special issue ***
*** Springer CCIS proceedings ***

Aims and Scope:

There is an increasing demand for using formal methods to validate and
verify safety-critical systems in fields such as power generation and
distribution, avionics, automotive systems, and medical systems. In
particular, newer standards, such as DO-178C (avionics), ISO 26262
(automotive systems), IEC 62304 (medical devices), and CENELEC EN
50128 (railway systems), emphasize the need for formal methods and
model-based development, thereby speeding up the adaptation of such
methods in industry.

The aim of this workshop is to bring together researchers and engineers
who are interested in the application of formal and semi-formal methods
to improve the quality of safety-critical computer systems. FTSCS
strives to promote research and development of formal methods and
tools for industrial applications, and is particularly interested in
industrial applications of formal methods. 

Specific topics include, but are not limited to:

* case studies and experience reports on the use of formal methods for
  analyzing safety-critical systems, including avionics, automotive,
  medical, railway, and other kinds of safety-critical and QoS-critical systems
* methods, techniques and tools to support automated analysis,
  certification, debugging, etc., of complex safety/QoS-critical systems
* analysis methods that address the limitations of formal methods in
  industry (usability, scalability, etc.)
* formal analysis support for modeling languages used in industry,
  such as AADL, Ptolemy, SysML, SCADE, Modelica, etc.
* code generation from validated models.

The workshop will provide a platform for discussions and the exchange of
innovative ideas, so submissions on work in progress are encouraged.

Submission:

We solicit submissions reporting on:

A- original research contributions (15 pages max, LNCS format);
B- applications and experiences (15 pages max, LNCS format);
C- surveys, comparisons, and state-of-the-art reports (15 pages max, LNCS);
D- tool papers (5 pages max, LNCS format);
E- position papers and work in progress (5 pages max, LNCS format)

related to the topics mentioned above.

All submissions must be original, unpublished, and not submitted
concurrently for publication elsewhere. Paper submission is done
via EasyChair at https://easychair.org/conferences/?conf=ftscs2016.
The final version of the paper must be prepared in LaTeX, adhering to
the LNCS format available at
http://www.springer.com/computer/lncs?SGWID=0-164-6-793341-0.

Publication:

All accepted papers will appear in the pre-proceedings of FTSCS 2016.
Accepted papers in the categories A-D above will appear in the
workshop proceedings that will be published as a volume in
Springer's CCIS series. 

The authors of a selected subset of accepted papers will be invited to
submit extended versions of their papers to appear in a special issue
of the Science of Computer Programming journal.

Important dates:

Submission deadline: September 4, 2016
Notification of acceptance: October 7, 2016
Workshop: November 14/15, 2016

Venue:

Tokyo, Japan

Program chairs:

Cyrille Artho        AIST, Japan
Peter Olveczky       University of Oslo, Norway

Program committee:

Etienne Andre        University Paris 13, France
Toshiaki Aoki        JAIST, Japan
Cyrille Artho        AIST, Japan
Kyungmin Bae         Pohang University of Science and Technology, Korea
Eun-Hye Choi         AIST, Japan
Alessandro Fantechi  University of Florence and ISTI-CNR, Pisa, Italy
Bernd Fischer        Stellenbosch University, South Africa
Osman Hasan          National University of Sciences & Technology, Pakistan
Klaus Havelund       NASA JPL, USA
Jerome Hugues        Institute for Space and Aeronautics Engineering, France
Marieke Huisman      University of Twente, The Netherlands
Ralf Huuck           Synopsys, Australia
Fuyuki Ishikawa      National Institute of Informatics, Japan
Takashi Kitamura     AIST, Japan
Alexander Knapp      Augsburg University, Germany
Thierry Lecomte      ClearSy System Engineering, France
Yang Liu             Nanyang Technological University, Singapore
Robi Malik           University of Waikato, New Zealand
Frederic Mallet      INRIA Sophia Antipolis, France
Roberto Nardone      University of Napoli "Federico II", Italy
Vivek Nigam          Federal University of Paraíba, Brazil
Thomas Noll          RWTH Aachen University, Germany
Kazuhiro Ogata       JAIST, Japan
Peter Olveczky       University of Oslo, Norway
Charles Pecheur      Universite catholique de Louvain, Belgium
Markus Roggenbach    Swansea University, UK
Ralf Sasse           ETH Zurich, Switzerland
Martina Seidl        Johannes Kepler University, Austria
Oleg Sokolsky        University of Pennsylvania, USA
Sofiene Tahar        Concordia University, Canada
Carolyn Talcott      SRI International, USA
Tatsuhiro Tsuchiya   Osaka University, Japan
Andras Voros         Budapest University of Technology and Economics, Hungary
Chen-Wei Wang        State University of New York (SUNY), Korea
Alan Wassyng         McMaster University, Canada
Michael Whalen       University of Minnesota, USA
Huibiao Zhu          East China Normal University, China

_______________________________________________
Memocode mailing list
Memocode <at> lists.cs.columbia.edu
------------------------------------------------------------------------------
What NetFlow Analyzer can do for you? Monitors network bandwidth and traffic
patterns at an interface-level. Reveals which users, apps, and protocols are 
consuming the most bandwidth. Provides multi-vendor support for NetFlow, 
J-Flow, sFlow and other flows. Make informed decisions using capacity planning
reports. http://pubads.g.doubleclick.net/gampad/clk?id=1444514421&iu=/41014381
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Wendelin Serwe | 6 Jun 17:57 2016
Picon
Picon

PhD position at INRIA Grenoble on formal methods for testing

The CONVECS (Inria Grenoble / LIG) and CTSYS (LCIS Valence) teams are
offering a fixed term (3 years) PhD position for research on formal
methods for the testing of networks of controllers.

See http://convecs.inria.fr/jobs/2016c.html for details.

Applications after July might not be considered.

Regards,
Wendelin Serwe

--

-- 
Inria/LIG - Convecs, Inovallee, CS 90051 38334 Montbonnot Cedex, FRANCE
Tel: (+33) 4 76 61 53 52,  Fax: (+33) 4 76 61 52 52

------------------------------------------------------------------------------
What NetFlow Analyzer can do for you? Monitors network bandwidth and traffic
patterns at an interface-level. Reveals which users, apps, and protocols are 
consuming the most bandwidth. Provides multi-vendor support for NetFlow, 
J-Flow, sFlow and other flows. Make informed decisions using capacity planning
reports. http://pubads.g.doubleclick.net/gampad/clk?id=1444514421&iu=/41014381
Vincent Aravantinos | 10 Jun 10:08 2016

Job offer: close-to-industry research position

Hi,


the job offer below might be interesting for those who would like to get more in touch with problems coming from the industry but without leaving research completely:


http://www.fortiss.org/karriere/wissenschaftliche-mitarbeiter/?tx_ttnews%5Btt_news%5D=392&cHash=29b18ed94ab6e4893d0e4b9a6afdfe90


As you will notice, the job description is in German, meaning that we are essentially looking for German speakers. However this is not an absolute restriction and if Google Translate makes you believe that this sounds really like you're made for this, feel free to contact me to know more.


Best,


Vincent Aravantinos

-- 

Senior researcher - Model-based engineering tools
fortiss · An-Institut Technische Universität München
Guerickestraße 25
80805 München
Germany
Tel.: +49 (89) 3603522 33
Fax: +49 (89) 3603522 50
E-Mail: aravantinos <at> fortiss.org
www.fortiss.org

Amtsgericht München: HRB: 176633
USt-IdNr.: DE263907002, Steuer-Nr.: 143/237/25900
Rechtsform: gemeinnützige GmbH
Sitz der Gesellschaft: München
Geschäftsführer: Prof. Dr. Helmut Krcmar, Thomas Vallon
Vorsitzender des Aufsichtsrats: Dr. Ronald Mertz

------------------------------------------------------------------------------
What NetFlow Analyzer can do for you? Monitors network bandwidth and traffic
patterns at an interface-level. Reveals which users, apps, and protocols are 
consuming the most bandwidth. Provides multi-vendor support for NetFlow, 
J-Flow, sFlow and other flows. Make informed decisions using capacity planning
reports. http://pubads.g.doubleclick.net/gampad/clk?id=1444514421&iu=/41014381
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Roopsha Samanta | 7 Jun 11:16 2016
Picon

Call for Participation: CAV 2016, July 17-23, Toronto

Apologies for multiple copies of this email. 

*****************************************************************
CALL FOR PARTICIPATION 28th International Conference on Computer Aided Verification (CAV 2016), July 17–23, 2016 Hyatt Regency Toronto Toronto, Ontario, Canada http://i-cav.org/2016/ ****************************************************************** Highlights ---------- * 46 regular papers, 12 tool papers * Four invited talks, four invited tutorials * Talk by a winner of the 2016 CAV award Registration deadline ------------------- * Early registration deadline: June 10, 2016 * Register at https://regmaster4.com/2016conf/CAV16/register.php Hotel registration -------------------- * Hotel Registration Deadline: June 17, 2016 * Special block rate (available until the above deadline): 179 CAD/night * Book at https://aws.passkey.com/event/14116269/owner/1460357/home Conference program -------------------- Available at http://i-cav.org/2016/program/ Invited talks ---------------------- * Gilles Barthe (IMDEA Software Institute) Computer-aided Cryptography * Gerwin Klein (NICTA and University of New South Wales) Scaling Up - From Trustworthy seL4 to Trustworthy Systems * Moshe Vardi (Rice University) Constrained Sampling and Counting * A winner of the 2016 CAV Award (To be announced at the conference) Invited tutorials --------------------------- * Parosh Abdulla (Uppsala University) Small Models in Parameterized Verification * Vitaly Chipounov (EPFL) The S2E Platform: Design, Implementation, and Applications * Paulo Tabuada (UCLA) Synthesizing Robust Cyber-Physical Systems * Martin Vechev and Pavol Bielek (ETH) Machine Learning for Programs Associated workshops ----------------------------- * NSV: 9th International Workshop on Numerical Software Verification http://nsv2016.pages.ist.ac.at/ * VSTTE: 8th Working Conference on Verified Software: Theories, Tools, and Experiments http://www.cs.toronto.edu/~chechik/vstte16/ * SYNT: 5th Workshop on Synthesis http://formal.epfl.ch/synt/2016/ * (EC)2: 9th International Workshop on Exploiting Concurrency Efficiently and Correctly http://ecee.colorado.edu/pavol/ec2-2016/ * HCCV: Workshop on High-Consequence Control Verification http://www.sandia.gov/hccv/ * VMW: Verification Mentoring Workshop http://i-cav.org/2016/vmw/ Conference chairs ----------------- Swarat Chaudhuri (Rice University) Azadeh Farzan (University of Toronto)
------------------------------------------------------------------------------
What NetFlow Analyzer can do for you? Monitors network bandwidth and traffic
patterns at an interface-level. Reveals which users, apps, and protocols are 
consuming the most bandwidth. Provides multi-vendor support for NetFlow, 
J-Flow, sFlow and other flows. Make informed decisions using capacity planning
reports. http://pubads.g.doubleclick.net/gampad/clk?id=1444514421&iu=/41014381
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
pedro.lopez | 14 Jun 23:24 2016

LOPSTR'16: Final Call for Papers and *Deadline Extension*

[ Please distribute, apologies for multiple postings. ]

======================================================================
            LOPSTR 2016: Final Call for Papers / Deadline Extension
======================================================================

                    26th International Symposium on
            Logic-Based Program Synthesis and Transformation
                              LOPSTR 2016

                http://cliplab.org/Conferences/LOPSTR16/

                   Edinburgh, UK, September 6-8, 2016
                (co-located with PPDP 2016 and SAS 2016)

======================================================================
NEW DEADLINES:
Abstract submission (extended):                June 20, 2016
Paper/Extended abstract submission (extended): June 27, 2016
======================================================================
INVITED SPEAKERS:
Francesco Logozzo (Facebook, USA)        [jointly with PPDP]
Greg Morrisett (Cornell University, USA) [jointly with PPDP]
Martin Vechev  (ETH Zurich, Switzerland) [jointly with SAS ]
======================================================================

The aim of the LOPSTR series is to stimulate and promote international
research and collaboration on  logic-based program development. LOPSTR
is open  to contributions  in logic-based  program development  in any
language  paradigm.  LOPSTR  has  a reputation  for  being  a  lively,
friendly forum for presenting and  discussing work in progress. Formal
proceedings are produced only after  the symposium so that authors can
incorporate this feedback in the published papers.

The 26th International Symposium  on Logic-based Program Synthesis and
Transformation  (LOPSTR  2016)  will  be held  at  the  University  of
Edinburgh,  Edinburgh,  UK;  previous  symposia were  held  in  Siena,
Canterbury,  Madrid,  Leuven,  Odense, Hagenberg,  Coimbra,  Valencia,
Lyngby,  Venice,  London,  Verona, Uppsala,  Madrid,  Paphos,  London,
Venice, Manchester, Leuven, Stockholm, Arnhem, Pisa, Louvain-la-Neuve,
and  Manchester.  LOPSTR  2016  will  be  co-located  with  PPDP  2016
(International  Symposium on  Principles and  Practice of  Declarative
Programming) and SAS 2016 (Static Analysis Symposium).

Topics  of   interest  cover   all  aspects  of   logic-based  program
development, all stages of the software life cycle, and issues of both
programming-in-the-small   and  programming-in-the-large.   Both  full
papers and  extended abstracts describing applications  in these areas
are especially  welcome. Contributions are  welcome on all  aspects of
logic-based program development, including, but not limited to:

  * synthesis
  * transformation
  * specialization
  * composition
  * optimization
  * inversion
  * specification
  * analysis and verification
  * testing and certification
  * program and model manipulation
  * transformational techniques in SE
  * applications and tools

Survey papers that present some aspects of the above topics from a new
perspective,  and application  papers  that  describe experience  with
industrial applications are also welcome.

Papers  must  describe original  work,  be  written and  presented  in
English, and must not substantially overlap with papers that have been
published  or   that  are  simultaneously  submitted   to  a  journal,
conference, or  workshop with refereed proceedings.  Work that already
appeared in  unpublished or informally published  workshop proceedings
may be submitted (please contact the PC chair in case of questions).

Important Dates

  Abstract submission (*extended*):                 Jun  20, 2016
  Paper/Extended abstract submission (*extended*):  Jun  27, 2016
  Notification:                                     Aug   3, 2016
  Camera-ready (for electronic pre-proceedings):    Aug  19, 2016
  Symposium:                                        Sep 6-8, 2016

Submission Guidelines

Authors  should submit  an electronic  copy of  the paper  (written in
English) in  PDF, formatted in  the Lecture Notes in  Computer Science
style. Each submission must include on its first page the paper title;
authors and their affiliations;  contact author's email; abstract; and
three  to  four keywords  which  will  be used  to  assist  the PC  in
selecting appropriate reviewers  for the paper. Page  numbers (and, if
possible, line  numbers) should appear  on the manuscript to  help the
reviewers in writing their report.  Submissions cannot exceed 15 pages
including references but excluding well-marked appendices not intended
for publication.  Reviewers are not  required to read  the appendices,
and thus papers should be  intelligible without them. Papers should be
submitted  via  the  Easychair  submission website  for  LOPSTR  2016:
http://www.easychair.org/conferences/?conf=lopstr2016
(can be accessed also through the LOPSTR 2016 web site).

Best Paper Award and Prize

A best paper award will be granted, which will include a 500 EUR prize
provided by  Springer.  This  award will  be given  to the  best paper
submitted to the conference, based  on the relevance, originality, and
technical quality. The program committee may split the award among two
or more papers, also considering authorship (e.g., student paper).

Proceedings

The formal  post-conference proceedings will be  published by Springer
in the  Lecture Notes in Computer  Science series. Full papers  can be
directly  accepted  for  publication  in the  formal  proceedings,  or
accepted  only for  presentation  at the  symposium  and inclusion  in
informal  proceedings. After  the symposium,  all authors  of extended
abstracts  and full  papers  accepted only  for  presentation will  be
invited to revise and/or extend their  submissions in the light of the
feedback  solicited at  the symposium.  Then, after  another round  of
reviewing, these  revised papers may  also be published in  the formal
proceedings.

Program Committee

      Slim Abdennadher, German University of Cairo, Egypt
      Maria Alpuente, Universitat Politecnica de Valencia, Spain
      Sergio Antoy, Portland State University, USA
      Michael Codish, Ben-Gurion University of the Negev, Israel
      Jerome Feret, CNRS/ENS/INRIA Paris, France.
      Fabio Fioravanti, University of Chieti - Pescara, Italy.
      Maurizio Gabbrielli, University of Bologna, Italy
      Maria Garcia de la Banda, Monash University, Australia
      Robert Glueck, University of Copenhagen, Denmark.
      Miguel Gomez-Zamalloa, Complutense University of Madrid, Spain
      Gopal Gupta, University of Texas at Dallas, USA
      Patricia Hill, Univ. of Leeds, UK and BUGSENG Srl, Italy
      Jacob Howe, City University London, UK
      Viktor Kuncak , EPFL Lausanne, Switzerland
      Michael Leuschel, University of Duesseldorf, Germany
      Heiko Mantel TU Darmstadt, Germany
      Jorge A. Navas, NASA, USA
      Naoki Nishida, Nagoya University, Japan
      Catuscia Palamidessi,  INRIA, France
      C.R. Ramakrishnan, SUNY Stony Brook, USA
      Vitor Santos Costa, Universidade do Porto, Portugal
      Hirohisa Seki, Nagoya Institute of Technology, Japan
      Peter Schneider-Kamp, University of Southern Denmark, Denmark

Program Chairs

     Manuel Hermenegildo, IMDEA Software Institute and T.U. Madrid (UPM)
     Pedro Lopez-Garcia, IMDEA Software Institute and CSIC

Organizing Committee

     James Cheney (University of Edinburgh, Local Organizer)
     Moreno Falaschi (University of Siena, Italy)

In cooperation with:

     The European Association for Theoretical Computer Science
     The European Association for Programming Languages and Systems
     The Association for Logic Programming
     The IMDEA Software Institute

------------------------------------------------------------------------------
What NetFlow Analyzer can do for you? Monitors network bandwidth and traffic
patterns at an interface-level. Reveals which users, apps, and protocols are 
consuming the most bandwidth. Provides multi-vendor support for NetFlow, 
J-Flow, sFlow and other flows. Make informed decisions using capacity planning
reports. http://pubads.g.doubleclick.net/gampad/clk?id=1444514421&iu=/41014381

Gmane