[Why3-club] 2d Call for Papers F-IDE Workshop 2019

2019-05-23 Thread Virgile Prevosto 
F-IDE - 5th Workshop on Formal Integrated Development Environments

https://fideworkshop2019.inesctec.pt

part of FM Week 2019 (http://formalmethods2019.inesctec.pt/?page_id=84)

# News

We are happy to announce that Wolfgang Ahrendt (Chalmers University)
accepted to give the opening keynote at F-IDE 2019.

# Important Dates

- Abstract submission: June 18, 2019
- Paper submission: June 25, 2019
- Notification: August 20, 2019
- Camera-ready version: September 3, 2019
- Workshop date: October 7, 2019

# About F-IDE

High levels of safety, security and also privacy standards require the
use of formal methods to specify and develop compliant software
(sub)systems. Any standard comes with an assessment process, which
requires a complete documentation of the application to ease the
justification of design choices and the review of code and proofs.

Ideally, an F-IDE dedicated to such developments should comply with
several requirements. The first one is to associate a logical theory
with a programming language, in a way that facilitates the tightly
coupled handling of specification properties and program constructs. The
second is to offer a language/environment simple enough to be usable by
most developers, even if they are not fully acquainted with higher-order
logics or set theory, in particular by making development of proofs as
easy as possible. The third is to offer automated management of
application documentation. It may also be expected that developments
done with such an F-IDE are reusable and modular. Tools for testing and
static analysis may be embedded within F-IDEs to support the assessment
process.

# Submission Guidelines

Submitted papers should follow EPTCS format (http://style.eptcs.org/).
Authors are invited to submit the following types of contributions:

Research papers providing new concepts and results
Experience reports
Position papers and research perspectives
Tool presentations

Two kinds of submissions will be considered: normal paper (15 pages
including bibliography), and shorter papers describing work in progress
and preliminary results (6 pages including bibliography). Submissions
will be made through EasyChair at:

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

All papers will be peer-reviewed by at least two members of the program
committee. They must describe original contributions whose main results
and conclusions have not been published or submitted elsewhere.
Preliminary proceedings, including all the papers selected for the
workshop, will be available electronically at the workshop. Post
proceedings will be proposed for publication with Electronic Proceedings
in Theoretical Computer Science (EPTCS).

# List of Topics

The workshop is open to contributions on all aspects of a system
development process, including specification, design, implementation,
analysis and documentation. It welcomes the presentation of tools,
methods, techniques and experiments. Topics of interest include, but are
not limited to, the following:

F-IDE building: design and integration of languages,
development of user-friendly front-ends
How to make high-level logical and programming concepts palatable
to industrial developers
Integration of Object-Oriented and modularity features
Integration of static analyzers
Integration of automatic proof tools,
theorem provers and testing tools
Documentation tools
Impact of tools on certification
Experience reports on developing F-IDEs
Experience reports on using F-IDEs
Experience reports on formal methods-based assessments
in industrial applications

# Committees
## PC Co-Chairs

Rosemary Monahan, Maynooth University, rosemary (dot) monahan (at)
nuim (dot) ie
Virgile Prevosto, Institut List, CEA Tech, Université Paris-Saclay,
virgile (dot) prevosto (at) cea (dot) fr
José Proença, HASLab/INESC-TEC and Universidade do Minho, jose (dot)
p (dot) proenca (at) inesctec (dot) pt

## Steering Committee

Catherine Dubois, Samovar / ENSIIE, catherine (dot) dubois (at)
ensiie (dot) fr
Paolo Masci, HASLab/INESC-TEC and Universidade do Minho, paolo (dot)
masci (at) inesctec (dot) pt
Dominique Méry, LORIA / Université de Lorraine, dominique (dot) mery
(at) loria (dot) fr

## Program Committee

Cinzia Bernardeschi (University of Pisa)
José Creissac Campos (University of Minho)
Paul Curzon (Queen Mary University of London)
Damien Doligez (INRIA)
Andrea Domenici (University of Pisa)
Carlo A. Furia (Chalmers University of Technology)
Kenneth Lausdahl (Aarhus University)
Stephan Merz (Inria Nancy)
Stefan Mitsch (Carnegie Mellon University)
Yannick Moy (Adacore)
César Muñoz (NASA Langley)
Andrei Paskevich (Université Paris-Sud, LRI)
François Pessaux (ENSTA ParisTech)
James Power (Maynooth University)
Steve Reeves (University of Waikato)
Bernhard Rumpe (RWTH Aachen University)
Claudio Sacerdoti-Cohen (University

[Why3-club] Call for Papers F-IDE Workshop 2019

2019-03-06 Thread Virgile Prevosto 
F-IDE - 5th Workshop on Formal Integrated Development Environments

https://fideworkshop2019.inesctec.pt

part of FM Week 2019 (http://formalmethods2019.inesctec.pt/?page_id=84)

# Important Dates

- Abstract submission: June 18, 2019
- Paper submission: June 25, 2019
- Notification: August 20, 2019
- Camera-ready version: September 3, 2019
- Workshop date: October 7, 2019

# About F-IDE

High levels of safety, security and also privacy standards require the
use of formal methods to specify and develop compliant software
(sub)systems. Any standard comes with an assessment process, which
requires a complete documentation of the application to ease the
justification of design choices and the review of code and proofs.

Ideally, an F-IDE dedicated to such developments should comply with
several requirements. The first one is to associate a logical theory
with a programming language, in a way that facilitates the tightly
coupled handling of specification properties and program constructs. The
second is to offer a language/environment simple enough to be usable by
most developers, even if they are not fully acquainted with higher-order
logics or set theory, in particular by making development of proofs as
easy as possible. The third is to offer automated management of
application documentation. It may also be expected that developments
done with such an F-IDE are reusable and modular. Tools for testing and
static analysis may be embedded within F-IDEs to support the assessment
process.

# Submission Guidelines

Submitted papers should follow EPTCS format (http://style.eptcs.org/).
Authors are invited to submit the following types of contributions:

Research papers providing new concepts and results
Experience reports
Position papers and research perspectives
Tool presentations

Two kinds of submissions will be considered: normal paper (15 pages
including bibliography), and shorter papers describing work in progress
and preliminary results (6 pages including bibliography). Submissions
will be made through EasyChair at:

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

All papers will be peer-reviewed by at least two members of the program
committee. They must describe original contributions whose main results
and conclusions have not been published or submitted elsewhere.
Preliminary proceedings, including all the papers selected for the
workshop, will be available electronically at the workshop. Post
proceedings will be proposed for publication with Electronic Proceedings
in Theoretical Computer Science (EPTCS).

# List of Topics

The workshop is open to contributions on all aspects of a system
development process, including specification, design, implementation,
analysis and documentation. It welcomes the presentation of tools,
methods, techniques and experiments. Topics of interest include, but are
not limited to, the following:

F-IDE building: design and integration of languages,
development of user-friendly front-ends
How to make high-level logical and programming concepts palatable
to industrial developers
Integration of Object-Oriented and modularity features
Integration of static analyzers
Integration of automatic proof tools,
theorem provers and testing tools
Documentation tools
Impact of tools on certification
Experience reports on developing F-IDEs
Experience reports on using F-IDEs
Experience reports on formal methods-based assessments
in industrial applications

# Committees
## PC Co-Chairs

Rosemary Monahan, Maynooth University, rosemary (dot) monahan (at)
nuim (dot) ie
Virgile Prevosto, Institut List, CEA Tech, Université Paris-Saclay,
virgile (dot) prevosto (at) cea (dot) fr
José Proença, HASLab/INESC-TEC and Universidade do Minho, jose (dot)
p (dot) proenca (at) inesctec (dot) pt

## Steering Committee

Catherine Dubois, Samovar / ENSIIE, catherine (dot) dubois (at)
ensiie (dot) fr
Paolo Masci, HASLab/INESC-TEC and Universidade do Minho, paolo (dot)
masci (at) inesctec (dot) pt
Dominique Méry, LORIA / Université de Lorraine, dominique (dot) mery
(at) loria (dot) fr

## Program Committee

Cinzia Bernardeschi (University of Pisa)
José Creissac Campos (University of Minho)
Paul Curzon (Queen Mary University of London)
Damien Doligez (INRIA)
Andrea Domenici (University of Pisa)
Carlo A. Furia (Chalmers University of Technology)
Kenneth Lausdahl (Aarhus University)
Stephan Merz (Inria Nancy)
Stefan Mitsch (Carnegie Mellon University)
Yannick Moy (Adacore)
César Muñoz (NASA Langley)
Andrei Paskevich (Université Paris-Sud, LRI)
François Pessaux (ENSTA ParisTech)
James Power (Maynooth University)
Steve Reeves (University of Waikato)
Bernhard Rumpe (RWTH Aachen University)
Claudio Sacerdoti-Cohen (University of Bologna)
Silvia Lizeth Tapia Tarifa (University of Oslo)
Mattias Ulbricht (Karlsruhe Institute of Technology)
Laurent

Re: [Why3-club] how to install why3 0.88.3 using opam for mac os

2018-04-12 Thread Virgile Prevosto 
2018-04-12 18:36 GMT+02:00 wenlong xie :
>
>
> [conf-gtksourceview: pkg-config gtksourceview-2.0] Command started
> + pkg-config "--short-errors" "--print-errors" "gtksourceview-2.0" 
> (CWD=/Users/wenlongxie/.opam/system/build/conf-gtksourceview.2)
> [ERROR] The compilation of conf-gtksourceview failed at "pkg-config 
> --short-errors --print-errors gtksourceview-2.0".
>
> #=== ERROR while installing conf-gtksourceview.2 
> ==#
> # opam-version 1.2.2
> # os   darwin
> # command  pkg-config --short-errors --print-errors gtksourceview-2.0
> # path /Users/wenlongxie/.opam/system/build/conf-gtksourceview.2
> # compiler system (4.06.1)
> # exit-code127

Thanks for the update. As I was suspecting, it seems like pkg-config
is not installed on your machine (under POSIX, 127 is the shell's
error code when it does not find the executable it is asked to
launch). It is quite surprising, as this is a fairly standard command
for any gtk-based library, and I'd have thought that brew would have
installed it together with the rest. Could you check whether there's a
brew package called pkg-config or something similar and if yes,
whether installing it through brew solve your issue? Otherwise, I'm
afraid you'll need help from someone who actually has a Mac on which
they can reproduce the issue.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club

Re: [Why3-club] how to install why3 0.88.3 using opam for mac os

2018-04-10 Thread Virgile Prevosto 
Hello,

As I asked on the issue you opened on Frama-C's bts yesterday (
https://bts.frama-c.com/view.php?id=2373) for the exact same problem: did
you try the suggestion offered by opam, i.e.
launching opam depext conf-gtksourceview.2? There is apparently an issue
with the way gtksourceview was installed on your system (which should have
been done by the line
brew install gmp gtk+ gtksourceview libgnomecanvas according to the
installation you link to). Note that this implies that you have install
depext with opam install depext before.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club

[Why3-club] CfP F-IDE: Formal Integrated Development Environment

2018-03-12 Thread Virgile Prevosto 
==
  Call for Papers F-IDE 2018

  4th Workshop on Formal Integrated Development Environment

 A satellite workshop of FLoC/FM2018

  July 14, 2018 - Oxford, UK

https://sites.google.com/view/fideworkshop2018
==

Aims


High levels of safety, security and also privacy standards require the
use of formal methods to specify and develop compliant software
(sub)systems. Any standard comes with an assessment process, which
requires a complete documentation of the application to ease the
justification of design choices and the review of code and proofs.

Ideally, an F-IDE dedicated to such developments should comply with
several requirements. The first one is to associate a logical theory
with a programming language, in a way that facilitates the tightly
coupled handling of specification properties and program
constructs. The second is to offer a language/environment simple
enough to be usable by most developers, even if they are not fully
acquainted with higher-order logics or set theory, in particular by
making development of proofs as easy as possible. The third is to
offer automated management of application documentation. It may also
be expected that developments done with such an F-IDE are reusable and
modular. Tools for testing and static analysis may be embedded within
F-IDEs to support the assessment process.

Topics
==

The workshop is open to contributions on all aspects of a system
development process, including specification, design, implementation,
analysis and documentation. It welcomes the presentation of tools,
methods, techniques and experiments. Topics of interest include, but
are not limited to, the following:

 - F-IDE building: design and integration of languages, development of
   user-friendly front-ends
 - How to make high-level logical and
   programming concepts palatable to industrial developers
 - Integration of Object-Oriented and modularity features
 - Integration of static analyzers
 - Integration of automatic proof tools, theorem provers and testing tools
 - Documentation tools
 - Impact of tools on certification
 - Experience reports on developing F-IDEs
 - Experience reports on using F-IDEs
 - Experience reports on formal methods-based assessments in
   industrial applications

Important dates
===

Abstract submission: April 23, 2018
Paper submission: April 30, 2018
Notification: May 15, 2018
Camera-ready version: May 25, 2018
Workshop date: July 14, 2018

PC Co-Chairs


Paolo Masci, HASLab/INESC-TEC and Universidade do Minho,
paolo (dot) masci (at) inesctec (dot) pt

Rosemary Monahan, Maynooth University,
rosemary (dot) monahan (at) nuim (dot) ie

Virgile Prevosto, Institut List, CEA, Université Paris-Saclay,
virgile (dot) prevosto (at) cea (dot) fr

Steering Committee
==

Catherine Dubois, Samovar / ENSIIE,
catherine (dot) dubois (at) ensiie (dot) fr

Dominique Méry, LORIA / Université de Lorraine,
dominique (dot) mery (at) loria (dot) fr

Submission Guidelines & Proceedings
===

Papers can be submitted through EasyChair using the following link:
  https://easychair.org/conferences/?conf=fide18

Authors are invited to submit the following types of contributions:

Research papers providing new concepts and results
Position papers and research perspectives
Experience reports
Tool presentations

Papers must describe original contributions whose main results and
conclusions have not been published or submitted elsewhere. All papers
will be peer-reviewed by at least two members of the program
committee. Submitted papers will follow the FM 2018 Format and
Submission Guidelines.

All the papers selected for the workshop will be available
electronically at the workshop. Post proceedings will be proposed for
publication with Electronic Proceedings in Theoretical Computer
Science (EPTCS).

Program Committee
=

Bernhard Beckert (Karlsruhe Institute of Technology)
Cinzia Bernardeschi (University of Pisa)
José Creissac Campos (University of Minho)
Claudio Sacerdoti Coen (University of Bologna)
Paul Curzon (Queen Mary University of London)
Damien Doligez (INRIA)
Andrea Domenici (University of Pisa)
Michalis Famelis (University of Montreal)
Carlo A. Furia (Chalmers University of Technology)
Andrew Gacek (Rockwell Collins, Inc.)
Kenneth Lausdahl (Aarhus University)
Stephan Merz (Inria Nancy)
Stefan Mitsch (Carnegie Mellon University)
César Muñoz (NASA Langley)
Andrei Paskevich (Université Paris-Sud, LRI)
François Pessaux (ENSTA ParisTech)
Marie-Laure Potet (Laboratoire Vérimag)
James Power (Maynooth University)
Steve Re

Re: [Why3-club] why3-base 0.86 opam switch 4.03.0

2016-06-29 Thread Virgile Prevosto 
Hello,

2016-06-29 19:13 GMT+02:00 sh0t :
> I can't opam install the 0.86 version of why3 with switch 4.03.0 because
> it asks me to downgrade menhir at 20141215 and then it fails for hygiene
> reasons.

Is there any particular reason for not installing the latest version
(0.87) of Why3? If I'm not mistaken, 0.86 has been released before
OCaml 4.03.0, thus it is not completely unexpected to run into trouble
with this particular mix of versions.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
http://lists.gforge.inria.fr/mailman/listinfo/why3-club

Re: [Why3-club] IDE in 0.85

2015-02-25 Thread Virgile Prevosto 
Hello,

2015-02-25 16:37 GMT+01:00 David Naumann naum...@cs.stevens.edu:
 I installed from OPAM but where's the IDE?  According to the 0.85 manual the
 following should have worked.

 why3 --version

 Why3 platform, version 0.85 (build date: Tue Feb 24 13:45:43 EST 2015)

 why3 ide

 'ide' is not a Why3 command.


Have you installed lablgtk through opam? According to 'opam show why3'
this is an optional dependency of why3. This means that if lablgtk is
already installed, why3 will be compiled with ide, but 'opam install
why3' will not trigger the installation of lablgtk (thus the ide won't
be built).

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club