***********************************************************
* *
* SFM-13:DS *
* *
* 13th International School on *
* Formal Methods for the Design of *
* Computer, Communication and Software Systems: *
* Dynamical Systems *
* *
* Bertinoro (Italy), 17-22 June 2013 *
* *
* http://www.sti.uniurb.it/events/sfm13ds/ *
* *
***********************************************************
* CALL FOR PARTICIPATION *
* (deadline: EXTENDED TO 04 April 2013) *
***********************************************************
GENERAL INFORMATION ABOUT SFM
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Formal methods are emerging in computer science as a prominent
approach to the rigorous design of computer, communication and
software systems.
The aim of the SFM series is to offer a good spectrum of
current research in foundations as well as applications of
formal methods, which can be of interest for graduate students
and young researchers who intend to approach the field.
This year SFM is an offspring of the workshops QAPL and MLQA
and is devoted to dynamical systems. It covers topics such as
chaotic dynamics, information theory, systems biology, hybrid systems,
quantum computing, and automata-based models and model checking.
COURSES AND LECTURERS
^^^^^^^^^^^^^^^^^^^^^
The school features the following lectures:
"Introduction to Dynamical Systems"
Herbert Wiklicky (Imperial College London, UK)
"Introduction to Chaotic Dynamics and Fractals"
Abbas Edalat (Imperial College London, UK)
"Information-Theoretic Security Analysis"
Boris Koepf (IMDEA Software, ES)
"Quantum Information Theory"
Renato Renner (ETH Zurich, CH)
"Quantitative Automata-Based Models and Model Checking"
Joost-Pieter Katoen (RWTH Aachen, DE)
"Fluid Analysis of Markov Models"
Jeremy Bradley (Imperial College London, UK)
"Discrete and Hybrid Methods in Systems Biology"
Oded Maler (VERIMAG, FR)
"ODE Analysis of Biological Systems"
Ion Petre (Abo Akademi, FI)
"Model Checking of Biological Models"
Lubos Brim (Masaryk Univ., CZ)
"Fluid Model Checking"
Luca Bortolussi (Univ. Trieste, IT)
"Checking Stability of Hybrid Systems"
Andreas Podelski (Univ. Freiburg, DE)
"Topological Quantum Computing"
Jiannis Pachos (Univ. Leeds, UK)
All participants will receive a copy of a tutorial book published by
Springer as a volume in the Lecture Notes in Computer Science series.
LOCATION
^^^^^^^^
SFM-13:DS will be held in the medieval hilltop town of Bertinoro.
This town is in Emilia Romagna, about 70 km south-east of Bologna,
at an elevation of about 230 m. It can be reached in a couple of
hours from the international airport "G. Marconi" of Bologna by
shuttle (from the airport to the railway station) + train (from
Bologna to Forli`) + bus/taxi (from the railway station to Bertinoro).
The closest airport is the "L. Ridolfi" airport of Forli`, which is
13 km away.
Bertinoro is close to many splendid locations such as Urbino,
Gradara, San Leo, and the Republic of San Marino, as well as some
less well-known locations like the thermal springs of Fratta Terme.
Bertinoro can also be a base for visiting some of the better-known
Italian locations such as Bologna, Rimini, Ravenna, Ferrara, Venezia,
Padova, Verona, Firenze, Pisa, and Siena.
Bertinoro itself is picturesque, with its narrow streets and
walkways winding around the central peak. The school will be held
at the Centro Residenziale Universitario (CRU), an ex-episcopal
fortress that has been converted by the University of Bologna into
a modern conference center with computing facilities and Internet
access. From the fortress, it is possible to enjoy a beautiful vista
stretching from the Apennines to the Adriatic coast and the Alps
over the Po Valley.
ORGANIZATION
^^^^^^^^^^^^
Scientific directors:
* Marco Bernardo (University of Urbino, IT)
* Erik de Vink (Eindhoven University of Technology, NL)
* Alessandra Di Pierro (University of Verona, IT)
* Herbert Wiklicky (Imperial College London, UK)
Secretary:
* Monica Michelacci (CRU Bertinoro, IT)
APPLICATION
^^^^^^^^^^^
Prospective participants should send by 21 March 2013
the application form, available on the school website,
to the two e-mail addresses below:
Marco Bernardo
marco.bernardo AT uniurb.it
Monica Michelacci
mmichelacci AT ceub.it
The registration fee is 600 euros and includes the school material.
The accommodation fee is 350 euros and covers the period June 16-23
(7 nights), double room (to share with another participant),
half board (breakfast and lunch, dinner of June 16 included,
lunch of June 23 excluded).
The reduced accommodation fee for the participants who do not
need a room is 100 euros and covers the period June 17-22
(6 lunches).
A very limited number of grants is available to cover part
of the registration fee (no grant can be requested to cover
the accommodation fee or the travel expenses).
Notification of accepted/rejected applications and grant requests
will be communicated by April 10.
Registration to the school is due by April 20.
No refund is possible for cancellation after May 15.
--
Caml-list mailing list. Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs
2013-03-20
[Caml-list] VeriSure Workshop Call for Papers
**********************************************************
CALL FOR PAPERS
**********************************************************
VeriSure: Verification and Assurance
In association with Computer-Aided Verification (CAV) 2013
July 14, 2013, Saint Petersburg, Russia
http://fm.csl.sri.com/VeriSure/
Workshop Organizers
Sam Owre, Natarajan Shankar, and John Rushby, SRI International
*** Workshop Description ***
The purpose of this workshop is to explore issues at the conjunction
of computer-aided verification and system assurance. An autonomous
car, for example, must safely negotiate an environment that is
imperfectly and incompletely modeled, while using actuators that are
themselves imperfect, and guided by fallible sensors whose data
requires delicate interpretation and fusion. Assurance here clearly
requires more than verification, but can build on verified
foundations.
In general, computer-aided verification is usually performed in
support of a larger activity whose goal is to provide assurance for a
decision with large consequences. The decision may be to send a
hardware design for fabrication or to release a commercial software
product, in which cases the consequences are economic, or it may be to
deploy a system in a context with potential consequences for societal
safety or security. In all these cases, verification will be just one
of many strands of evidence that contribute to system assurance, and
the overall structure of the assurance may be specified or constrained
by regulation or certification requirements.
This workshop will explore challenges and opportunities posed for
computer-aided verification by the larger context of system
assurance. One immediate set of challenges arises from the (recursive)
need to provide assurance for the claims delivered by computer-aided
verification itself. Related is the challenge of providing assurance
for the assumptions and requirements with respect to which the
verification is performed. These challenges are situated in pragmatic
engineering settings where choices must be made about what should be
verified, and to what level of detail, and what should or must be
assured by other means (such as testing, human review, or runtime
monitoring), and how all these should be combined.
Opportunities arise from the possibility of formalizing and verifying
aspects of the larger assurance activity, stimulated by recent
proposals that this should be structured as an assurance "case." An
assurance case is composed of claims, argument, and evidence, where
the argument justifies claims (e.g., for security or safety) based on
evidence about the system and its development. An interesting
complication is that many top-level claims are probabilistic (e.g.,
10-9 for certain aircraft software) while traditional formal
verification is unconditional.
We solicit papers on relevant topics, which include but are not
restricted to the following. We encourage exploratory work that will
stimulate discussion.
o Quantitative and qualitative assurance claims and arguments
o Integration of formal verification with assurance
and with assurance cases
o Modular and incremental methods of verification and assurance
o Toolchains for integrated assurance arguments
o Soundness guarantees for tools, toolchains, and workflows
o Certification and regulatory requirements and standards
o Experience reports and challenges
The program will include invited speakers, presentation of selected
papers, and discussion.
The workshop is colocated with CAV 2013 in Saint Petersburg, Russia
*** Invited Speakers ***
Robin Bloomfield, City University and Adelard
Others to be announced
*** Workshop Committee ***
Jean-Christophe Filliâtre, LRI Université Paris Sud, France
Mike Gordon, Cambridge University, UK
Sofia Guerra, Adelard, UK
Michael Holloway, NASA Langley, USA
Michaela Huhn, TU-Clausthal, Germany
Florent Kirchner, CEA, France
Gerwin Klein, NICTA, Australia
Tom Maibaum, McMaster University, Canada
Bertrand Meyer, ETH Zurich, Switzerland
Grigori Mints, Stanford University, USA
Harald Ruess, FORTISS, Germany
Oleg Sokolsky, University of Pennsylvania, USA
Virginie Wiels, ONERA, France
*** Important Dates ***
Position papers due Soon
Reviews/decisions TBA
Camera ready versions due TBA
VeriSure Workshop July 14
Note: We ask potential participants to apply for a visa invitation
letter as soon as possible (even if their trip plans may change
later). For further details please check the CAV Visa page at
http://cav2013.forsyte.at/visa/
*** Electronic Submissions ***
Submissions should be in PDF format between 3-12 pages. We recommend
the guidelines for ACM SIG Proceedings. The submissions page is open at
https://www.easychair.org/conferences/?conf=verisure2013
--
Caml-list mailing list. Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs
CALL FOR PAPERS
**********************************************************
VeriSure: Verification and Assurance
In association with Computer-Aided Verification (CAV) 2013
July 14, 2013, Saint Petersburg, Russia
http://fm.csl.sri.com/VeriSure/
Workshop Organizers
Sam Owre, Natarajan Shankar, and John Rushby, SRI International
*** Workshop Description ***
The purpose of this workshop is to explore issues at the conjunction
of computer-aided verification and system assurance. An autonomous
car, for example, must safely negotiate an environment that is
imperfectly and incompletely modeled, while using actuators that are
themselves imperfect, and guided by fallible sensors whose data
requires delicate interpretation and fusion. Assurance here clearly
requires more than verification, but can build on verified
foundations.
In general, computer-aided verification is usually performed in
support of a larger activity whose goal is to provide assurance for a
decision with large consequences. The decision may be to send a
hardware design for fabrication or to release a commercial software
product, in which cases the consequences are economic, or it may be to
deploy a system in a context with potential consequences for societal
safety or security. In all these cases, verification will be just one
of many strands of evidence that contribute to system assurance, and
the overall structure of the assurance may be specified or constrained
by regulation or certification requirements.
This workshop will explore challenges and opportunities posed for
computer-aided verification by the larger context of system
assurance. One immediate set of challenges arises from the (recursive)
need to provide assurance for the claims delivered by computer-aided
verification itself. Related is the challenge of providing assurance
for the assumptions and requirements with respect to which the
verification is performed. These challenges are situated in pragmatic
engineering settings where choices must be made about what should be
verified, and to what level of detail, and what should or must be
assured by other means (such as testing, human review, or runtime
monitoring), and how all these should be combined.
Opportunities arise from the possibility of formalizing and verifying
aspects of the larger assurance activity, stimulated by recent
proposals that this should be structured as an assurance "case." An
assurance case is composed of claims, argument, and evidence, where
the argument justifies claims (e.g., for security or safety) based on
evidence about the system and its development. An interesting
complication is that many top-level claims are probabilistic (e.g.,
10-9 for certain aircraft software) while traditional formal
verification is unconditional.
We solicit papers on relevant topics, which include but are not
restricted to the following. We encourage exploratory work that will
stimulate discussion.
o Quantitative and qualitative assurance claims and arguments
o Integration of formal verification with assurance
and with assurance cases
o Modular and incremental methods of verification and assurance
o Toolchains for integrated assurance arguments
o Soundness guarantees for tools, toolchains, and workflows
o Certification and regulatory requirements and standards
o Experience reports and challenges
The program will include invited speakers, presentation of selected
papers, and discussion.
The workshop is colocated with CAV 2013 in Saint Petersburg, Russia
*** Invited Speakers ***
Robin Bloomfield, City University and Adelard
Others to be announced
*** Workshop Committee ***
Jean-Christophe Filliâtre, LRI Université Paris Sud, France
Mike Gordon, Cambridge University, UK
Sofia Guerra, Adelard, UK
Michael Holloway, NASA Langley, USA
Michaela Huhn, TU-Clausthal, Germany
Florent Kirchner, CEA, France
Gerwin Klein, NICTA, Australia
Tom Maibaum, McMaster University, Canada
Bertrand Meyer, ETH Zurich, Switzerland
Grigori Mints, Stanford University, USA
Harald Ruess, FORTISS, Germany
Oleg Sokolsky, University of Pennsylvania, USA
Virginie Wiels, ONERA, France
*** Important Dates ***
Position papers due Soon
Reviews/decisions TBA
Camera ready versions due TBA
VeriSure Workshop July 14
Note: We ask potential participants to apply for a visa invitation
letter as soon as possible (even if their trip plans may change
later). For further details please check the CAV Visa page at
http://cav2013.forsyte.at/visa/
*** Electronic Submissions ***
Submissions should be in PDF format between 3-12 pages. We recommend
the guidelines for ACM SIG Proceedings. The submissions page is open at
https://www.easychair.org/conferences/?conf=verisure2013
--
Caml-list mailing list. Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs
2013-03-16
[Caml-list] ICFP 2013: Second Call for Papers
===================================================================== 18th ACM SIGPLAN International Conference on Functional Programming ICFP 2013 Boston, MA, USA, 25-27 September 2013 http://www.icfpconference.org/icfp2013 ===================================================================== Important Dates ~~~~~~~~~~~~~~~ Submissions due: Thursday, 28 March 2013 23:59 UTC-11 (Pago Pago, American Samoa, time) Author response: Wednesday, 22 May 0:00 UTC-11 Friday, 24 May 2013 23:59 UTC-11 Notification: Friday, 7 June 2013 Final copy due: Friday, 5 July 2013 Scope ~~~~~ ICFP 2013 seeks original papers on the art and science of functional programming. Submissions are invited on all topics from principles to practice, from foundations to features, and from abstraction to application. The scope includes all languages that encourage functional programming, including both purely applicative and imperative languages, as well as languages with objects, concurrency, or parallelism. Topics of interest include (but are not limited to): * Language Design: concurrency and distribution; modules; components and composition; metaprogramming; interoperability; type systems; relations to imperative, object-oriented, or logic programming * Implementation: abstract machines; virtual machines; interpretation; compilation; compile-time and run-time optimization; memory management; multi-threading; exploiting parallel hardware; interfaces to foreign functions, services, components, or low-level machine resources * Software-Development Techniques: algorithms and data structures; design patterns; specification; verification; validation; proof assistants; debugging; testing; tracing; profiling * Foundations: formal semantics; lambda calculus; rewriting; type theory; monads; continuations; control; state; effects; program verification; dependent types * Analysis and Transformation: control-flow; data-flow; abstract interpretation; partial evaluation; program calculation * Applications and Domain-Specific Languages: symbolic computing; formal-methods tools; artificial intelligence; systems programming; distributed-systems and web programming; hardware design; databases; XML processing; scientific and numerical computing; graphical user interfaces; multimedia programming; scripting; system administration; security * Education: teaching introductory programming; parallel programming; mathematical proof; algebra * Functional Pearls: elegant, instructive, and fun essays on functional programming * Experience Reports: short papers that provide evidence that functional programming really works or describe obstacles that have kept it from working If you are concerned about the appropriateness of some topic, do not hesitate to contact the program chair. Abbreviated instructions for authors ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ * By Thursday, 28 March 2013, 23:59 UTC-11 (American Samoa time), submit a full paper of at most 12 pages (6 pages for an Experience Report), including bibliography and figures. The deadlines will be strictly enforced and papers exceeding the page limits will be summarily rejected. * Authors have the option to attach supplementary material to a submission, on the understanding that reviewers may choose not to look at it. * Each submission must adhere to SIGPLAN's republication policy, as explained on the web at http://www.sigplan.org/Resources/Policies/Republication * Authors of resubmitted (but previously rejected) papers have the option to attach an annotated copy of the reviews of their previous submission(s), explaining how they have addressed these previous reviews in the present submission. If a reviewer identifies him/herself as a reviewer of this previous submission and wishes to see how his/her comments have been addressed, the program chair will communicate to this reviewer the annotated copy of his/her previous review. Otherwise, no reviewer will read the annotated copies of the previous reviews. Overall, a submission will be evaluated according to its relevance, correctness, significance, originality, and clarity. It should explain its contributions in both general and technical terms, clearly identifying what has been accomplished, explaining why it is significant, and comparing it with previous work. The technical content should be accessible to a broad audience. Functional Pearls and Experience Reports are separate categories of papers that need not report original research results and must be marked as such at the time of submission. Detailed guidelines on both categories are on the conference web site. Proceedings will be published by ACM Press. Authors of accepted submissions are expected to transfer the copyright to the ACM. Presentations will be videotaped and released online if the presenter consents. Formatting: Submissions must be in PDF format printable in black and white on US Letter sized paper and interpretable by Ghostscript. Papers must adhere to the standard ACM conference format: two columns, nine-point font on a ten-point baseline, with columns 20pc (3.33in) wide and 54pc (9in) tall, with a column gutter of 2pc (0.33in). A suitable document template for LaTeX is available: http://www.acm.org/sigs/sigplan/authorInformation.htm Submission: Submissions will be accepted on the web at https://www.easychair.org/conferences/?conf=icfp2013 . Improved versions of a paper may be submitted at any point before the submission deadline using the same web interface. Author response: Authors will have a 72-hour period, starting at 0:00 UTC-11 on Wednesday, 22 May 2013, to read reviews and respond to them. Special Journal Issue: There will be a special issue of the Journal of Functional Programming with papers from ICFP 2013. The program committee will invite the authors of select accepted papers to submit a journal version to this issue. General Chair: Greg Morrisett, Harvard University Program Chair: Tarmo Uustalu, Institute of Cybernetics, Tallinn Program Committee: Thorsten Altenkirch, University of Nottingham Olaf Chitil, University of Kent Silvia Ghilezan, University of Novi Sad Michael Hanus, Christian-Albrechts-Universität zu Kiel Fritz Henglein, University of Copenhagen Mauro Jaskelioff, Universidad Nacional de Rosario Alan Jeffrey, Alcatel-Lucent Bell Labs Shin-ya Katsumata, Kyoto University Shriram Krishnamurthi, Brown University John Launchbury, Galois Ryan Newton, Indiana University Sungwoo Park, Pohang University of Science and Technology Sam Staton, University of Cambridge Nikhil Swamy, Microsoft Research, Redmond, WA Dimitrios Vytiniotis, Microsoft Research, Cambridge
2013-03-13
[Caml-list] Call for papers: FSFMA (PhD session)
====================================================================
Call for papers (PhD session)
FSFMA 2013
1st French Singaporean Workshop in Formal Methods and Applications
http://www.comp.nus.edu.sg/~pat/fsfma2013/
====================================================================
The 1st French Singaporean Workshop in Formal Methods and Applications (FSFMA)
aims at sharing research interests and launching collaborations in the area of
formal methods and their applications.
The scientific subject of the workshop covers (but does not limit to) areas
such as formal specification, model checking, verification, program analysis
and transformation, software engineering, and applications in major areas of
computer science, including aeronautics and aerospace.
The workshop will bring together researchers and industry R&D experts from all
countries together to exchange their knowledge, discuss their research
findings,
and explore potential collaborations.
Round tables will focus on French-Singaporean funding and cooperation
opportunities.
----------------------------------------------------------------------------
| A PhD session will allow Master and PhD students to present their work.
| The workshop may offer travel grants to a selection of PhD students.
----------------------------------------------------------------------------
The workshop will take place on July 15th and 16th, 2013, in the National
University of Singapore as a satellite of ICECCS 2013.
=================
IMPORTANT DATES
=================
Abstract: April 14th, 2013
Full papers: April 21st, 2013
Notification: June 3rd, 2013
Camera ready: June 13th, 2013
Workshop: July 15th-16th, 2013
=================
TOPICS OF THE WORKSHOP
=================
The main theme of the workshop is to establish links between academic and
industry scientists interested in methods and techniques for constructing
reliable systems using formal methods. The scientific topics of the workshop
include, but are not limited to:
- concurrent and distributed systems
- formal specification and semantics
- infinite-state and parameterized systems
- model checking algorithms
- SAT and SMT solvers
- security and privacy
- software engineering and formal methods
- specification and verification (hardware and embedded systems, probabilistic
and real-time systems, etc.)
- case studies and experience reports on the use of formal methods
- tools and industrial applications
- applications in aeronautics and aerospace
=================
SUBMISSION AND PUBLICATION
=================
Two kinds of papers are welcome:
- regular papers
- PhD papers (for the doctoral session).
The content of papers should be original and not submitted elsewhere.
All papers will be submitted to at least three reviews.
The page limit is 15 pages (regular) and 6 pages (PhD) in the OASIcs format.
-------------------------------------------------------------------------------
| Both regular and PhD papers will be published by the OpenAccess Series in
| Informatics (OASIcs), a free open-access and online electronic proceedings
| series edited by Schloss Dagstuhl, indexed with ISBN and referenced in major
| databases such as DBLP.
-------------------------------------------------------------------------------
OASIcs proceedings are published under the Creative Commons CC-BY license.
Hereby, the authors retain their copyright.
Submission will be made in PDF format through Easychair:
https://www.easychair.org/conferences/?conf=fsfma2013
Additional remarks:
-------------------------------------------------------------------------------
- There are no restrictions on authors' citizenships and working countries.
- For PhD papers, at least one author must be Master or PhD student.
-------------------------------------------------------------------------------
=================
CHAIRS
=================
- Christine Choppy (Université Paris 13, Sorbonne Paris Cité, France)
- Jun Sun (Singapore University of Technology and Design, Singapore)
=================
PhD SESSION CHAIRS
=================
- Étienne André (Université Paris 13, Sorbonne Paris Cité, France)
- Yang Liu (Nanyang Technological University, Singapore)
=================
INVITED SPEAKERS
=================
- Laurent Fribourg (LSV, CNRS & ENS de Cachan, France)
- Ng Wee Keong (School of Computer Engineering, NTU, Singapore)
(to be completed)
--
Caml-list mailing list. Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs
Call for papers (PhD session)
FSFMA 2013
1st French Singaporean Workshop in Formal Methods and Applications
http://www.comp.nus.edu.sg/~pat/fsfma2013/
====================================================================
The 1st French Singaporean Workshop in Formal Methods and Applications (FSFMA)
aims at sharing research interests and launching collaborations in the area of
formal methods and their applications.
The scientific subject of the workshop covers (but does not limit to) areas
such as formal specification, model checking, verification, program analysis
and transformation, software engineering, and applications in major areas of
computer science, including aeronautics and aerospace.
The workshop will bring together researchers and industry R&D experts from all
countries together to exchange their knowledge, discuss their research
findings,
and explore potential collaborations.
Round tables will focus on French-Singaporean funding and cooperation
opportunities.
----------------------------------------------------------------------------
| A PhD session will allow Master and PhD students to present their work.
| The workshop may offer travel grants to a selection of PhD students.
----------------------------------------------------------------------------
The workshop will take place on July 15th and 16th, 2013, in the National
University of Singapore as a satellite of ICECCS 2013.
=================
IMPORTANT DATES
=================
Abstract: April 14th, 2013
Full papers: April 21st, 2013
Notification: June 3rd, 2013
Camera ready: June 13th, 2013
Workshop: July 15th-16th, 2013
=================
TOPICS OF THE WORKSHOP
=================
The main theme of the workshop is to establish links between academic and
industry scientists interested in methods and techniques for constructing
reliable systems using formal methods. The scientific topics of the workshop
include, but are not limited to:
- concurrent and distributed systems
- formal specification and semantics
- infinite-state and parameterized systems
- model checking algorithms
- SAT and SMT solvers
- security and privacy
- software engineering and formal methods
- specification and verification (hardware and embedded systems, probabilistic
and real-time systems, etc.)
- case studies and experience reports on the use of formal methods
- tools and industrial applications
- applications in aeronautics and aerospace
=================
SUBMISSION AND PUBLICATION
=================
Two kinds of papers are welcome:
- regular papers
- PhD papers (for the doctoral session).
The content of papers should be original and not submitted elsewhere.
All papers will be submitted to at least three reviews.
The page limit is 15 pages (regular) and 6 pages (PhD) in the OASIcs format.
-------------------------------------------------------------------------------
| Both regular and PhD papers will be published by the OpenAccess Series in
| Informatics (OASIcs), a free open-access and online electronic proceedings
| series edited by Schloss Dagstuhl, indexed with ISBN and referenced in major
| databases such as DBLP.
-------------------------------------------------------------------------------
OASIcs proceedings are published under the Creative Commons CC-BY license.
Hereby, the authors retain their copyright.
Submission will be made in PDF format through Easychair:
https://www.easychair.org/conferences/?conf=fsfma2013
Additional remarks:
-------------------------------------------------------------------------------
- There are no restrictions on authors' citizenships and working countries.
- For PhD papers, at least one author must be Master or PhD student.
-------------------------------------------------------------------------------
=================
CHAIRS
=================
- Christine Choppy (Université Paris 13, Sorbonne Paris Cité, France)
- Jun Sun (Singapore University of Technology and Design, Singapore)
=================
PhD SESSION CHAIRS
=================
- Étienne André (Université Paris 13, Sorbonne Paris Cité, France)
- Yang Liu (Nanyang Technological University, Singapore)
=================
INVITED SPEAKERS
=================
- Laurent Fribourg (LSV, CNRS & ENS de Cachan, France)
- Ng Wee Keong (School of Computer Engineering, NTU, Singapore)
(to be completed)
--
Caml-list mailing list. Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs
2013-03-10
[Caml-list] CS2BIO 2013: 2nd Call for Paper
[We apologise for multiple copies]
NOTE THE SPECIAL ISSUES OF "THEORETICAL COMPUTER SCIENCE" JOURNAL
AND FOR PAPERS CONTRIBUTING TO THE EU FP7 DyM-CS SESSION
THE SPECIAL ISSUE OF "MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE" JOURNAL
========================================================================
First call for papers
CS2Bio'13
4th International Workshop on
Interactions between Computer Science and Biology
Affiliated to DisCoTec'13
June 6th, 2013
Florence, Italy
http://cs2bio13.di.unito.it/
========================================================================
Systems Biology is a stimulating field of application for computer
scientists and a promising resource for biologists. The aim of this
workshop is to gather researchers in formal methods that are
interested in the convergence of Computer Science and Life Sciences.
In particular, in this forth edition, we solicit the contribution of
original results, from any research areas, such as Mathematics,
Physics, Complex Systems, and Computational Sciences that address both
theoretical aspects of modelling and applied work on the comprehension
of biological behaviour. Furthermore, to facilitate the integration of
different research areas we encourage the presentation of the main
objectives and preliminary results of active projects on the CS2Bio
topics conducted by interdisciplinary teams.
*** SCOPE ***
Contributions selected for presentation at CS2Bio should either present
the modelling of a specific biological phenomenon using formal
techniques, or a modelling, simulation, testing or verification
approach in computer science that leads to a novel and promising
application to a range of biological or medical systems. In the latter
case, some emphasis on the scope and scalability of the approach will
be required. The workshop intends to attract researchers interested in
models, verification, tools, and programming primitives concerning the
complex interactions encountered. Topics of interest include, but shall
not be limited to:
- Formal Biological Modelling
- Formal methods for the representation of biological systems and
their dynamics;
- Theoretical links and comparisons between different formal models
for the modelling of biological processes;
- Quantitative (probabilistic, timed, stochastic, etc.) languages
and calculi;
- Spatial (geometrical, topological) languages and calculi;
- Prediction of biological behaviour from incomplete information;
- Model checking, abstract interpretation, type systems, etc.
- Novel Computational Paradigms for Understanding Biological Complex
Systems
- Quantum information and life sciences;
- Geometry, algebraic and computational topology and
biomathematics;
- Information processing and biomedicine;
- Statistical mechanics and biophysics.
- Tools and Simulations
- Modelling, analysis and simulation tools for systems biology;
- Emergence of properties in complex biological systems;
- Tools for parallel, distributed, and multi-resolution simulation
methods;
- Detailed biological case-studies.
*** INVITED SPEAKERS ***
- Giuseppe Longo (ENS Paris, France)
- Mario Rasetti (ISI Foundation, Italy)
*** SUBMISSION GUIDELINES ***
We solicit three kinds of contributions:
- Regular papers: must report previously unpublished work and not be
submitted concurrently to a journal or to another conference with
refereed proceedings (limited to 14 pages).
- Tool presentations: describing new tools or platforms for the
modelling of biological systems (limited to 7 pages).
- Dissemination of project results: concern recent or ongoing work
on topics relevant to CS2Bio and are intended to provide discussion
and stimulate feedback during the workshop. The focus of a
dissemination should be put on the main objectives and preliminary
results of active projects on topics relevant to the workshop. There
are no restrictions about previous or future publication of the
contents of a dissemination, it could also be based on a recently
published paper or on a work which has not yet been submitted
(limited to 4 pages).
Authors should submit their contributions via EasyChair
(http://www.easychair.org/conferences/?conf=cs2bio13) in the form of a
pdf file compiled using the ENTCS style for the workshop proceedings
(http://www.entcs.org/files/cs2bio/prentcsmacro.sty). If necessary,
detailed proofs or other additional material can be added in an appendix
(referees might review it at their discretion).
*** DISSEMINATION ***
The proceedings of the workshop will be published in a volume of the
Elsevier series "Electronic Notes on Theoretical Computer Science". After
the event, papers presented at the workshop will be invited to be
furtherly extended and submitted to an open special issue of the journal
"Theoretical Computer Science".
A special issue of the journal "Mathematical Structures in Computer Science"
will be open for papers that will contribute to the session on
EU FP7 DyM-CS - Dynamics of Multi-level Complex Systems -
that will be held on the 5th of June.
*** IMPORTANT DATES ***
- Submission deadline: 26 March 2013
- Notification to authors: 03 May 2013
- Workshop: 06 June 2013
*** PROGRAM COMMITTEE ***
- Erik de Vink
- Jasmin Fisher
- Paola Giannini
- Radu Grosu
- Jean Krivine
- Pietro Lio'
- Daniele Manini
- Emanuela Merelli (Co-chair)
- Paolo Milazzo
- Ion Petre
- Marco Pettini
- Christian Reidys
- David Safranek
- Luca Tesei
- Angelo Troina (Co-chair)
- Verena Wolf
*** STEERING COMMITTEE ***
- Erik de Vink
- Paola Giannini
- Jean Krivine
- Angelo Troina
--
Emanuela Merelli
School of Science and Technology, Computer Science Division
University of Camerino
Via Madonna delle Carceri, 13 - 62032, Camerino, Italy
office: +390737402567, fax: +390737402561, mobile: +393383990412
skype: emanuela.merelli , http://www.cs.unicam.it/merelli
NOTE THE SPECIAL ISSUES OF "THEORETICAL COMPUTER SCIENCE" JOURNAL
AND FOR PAPERS CONTRIBUTING TO THE EU FP7 DyM-CS SESSION
THE SPECIAL ISSUE OF "MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE" JOURNAL
========================================================================
First call for papers
CS2Bio'13
4th International Workshop on
Interactions between Computer Science and Biology
Affiliated to DisCoTec'13
June 6th, 2013
Florence, Italy
http://cs2bio13.di.unito.it/
========================================================================
Systems Biology is a stimulating field of application for computer
scientists and a promising resource for biologists. The aim of this
workshop is to gather researchers in formal methods that are
interested in the convergence of Computer Science and Life Sciences.
In particular, in this forth edition, we solicit the contribution of
original results, from any research areas, such as Mathematics,
Physics, Complex Systems, and Computational Sciences that address both
theoretical aspects of modelling and applied work on the comprehension
of biological behaviour. Furthermore, to facilitate the integration of
different research areas we encourage the presentation of the main
objectives and preliminary results of active projects on the CS2Bio
topics conducted by interdisciplinary teams.
*** SCOPE ***
Contributions selected for presentation at CS2Bio should either present
the modelling of a specific biological phenomenon using formal
techniques, or a modelling, simulation, testing or verification
approach in computer science that leads to a novel and promising
application to a range of biological or medical systems. In the latter
case, some emphasis on the scope and scalability of the approach will
be required. The workshop intends to attract researchers interested in
models, verification, tools, and programming primitives concerning the
complex interactions encountered. Topics of interest include, but shall
not be limited to:
- Formal Biological Modelling
- Formal methods for the representation of biological systems and
their dynamics;
- Theoretical links and comparisons between different formal models
for the modelling of biological processes;
- Quantitative (probabilistic, timed, stochastic, etc.) languages
and calculi;
- Spatial (geometrical, topological) languages and calculi;
- Prediction of biological behaviour from incomplete information;
- Model checking, abstract interpretation, type systems, etc.
- Novel Computational Paradigms for Understanding Biological Complex
Systems
- Quantum information and life sciences;
- Geometry, algebraic and computational topology and
biomathematics;
- Information processing and biomedicine;
- Statistical mechanics and biophysics.
- Tools and Simulations
- Modelling, analysis and simulation tools for systems biology;
- Emergence of properties in complex biological systems;
- Tools for parallel, distributed, and multi-resolution simulation
methods;
- Detailed biological case-studies.
*** INVITED SPEAKERS ***
- Giuseppe Longo (ENS Paris, France)
- Mario Rasetti (ISI Foundation, Italy)
*** SUBMISSION GUIDELINES ***
We solicit three kinds of contributions:
- Regular papers: must report previously unpublished work and not be
submitted concurrently to a journal or to another conference with
refereed proceedings (limited to 14 pages).
- Tool presentations: describing new tools or platforms for the
modelling of biological systems (limited to 7 pages).
- Dissemination of project results: concern recent or ongoing work
on topics relevant to CS2Bio and are intended to provide discussion
and stimulate feedback during the workshop. The focus of a
dissemination should be put on the main objectives and preliminary
results of active projects on topics relevant to the workshop. There
are no restrictions about previous or future publication of the
contents of a dissemination, it could also be based on a recently
published paper or on a work which has not yet been submitted
(limited to 4 pages).
Authors should submit their contributions via EasyChair
(http://www.easychair.org/conferences/?conf=cs2bio13) in the form of a
pdf file compiled using the ENTCS style for the workshop proceedings
(http://www.entcs.org/files/cs2bio/prentcsmacro.sty). If necessary,
detailed proofs or other additional material can be added in an appendix
(referees might review it at their discretion).
*** DISSEMINATION ***
The proceedings of the workshop will be published in a volume of the
Elsevier series "Electronic Notes on Theoretical Computer Science". After
the event, papers presented at the workshop will be invited to be
furtherly extended and submitted to an open special issue of the journal
"Theoretical Computer Science".
A special issue of the journal "Mathematical Structures in Computer Science"
will be open for papers that will contribute to the session on
EU FP7 DyM-CS - Dynamics of Multi-level Complex Systems -
that will be held on the 5th of June.
*** IMPORTANT DATES ***
- Submission deadline: 26 March 2013
- Notification to authors: 03 May 2013
- Workshop: 06 June 2013
*** PROGRAM COMMITTEE ***
- Erik de Vink
- Jasmin Fisher
- Paola Giannini
- Radu Grosu
- Jean Krivine
- Pietro Lio'
- Daniele Manini
- Emanuela Merelli (Co-chair)
- Paolo Milazzo
- Ion Petre
- Marco Pettini
- Christian Reidys
- David Safranek
- Luca Tesei
- Angelo Troina (Co-chair)
- Verena Wolf
*** STEERING COMMITTEE ***
- Erik de Vink
- Paola Giannini
- Jean Krivine
- Angelo Troina
--
Emanuela Merelli
School of Science and Technology, Computer Science Division
University of Camerino
Via Madonna delle Carceri, 13 - 62032, Camerino, Italy
office: +390737402567, fax: +390737402561, mobile: +393383990412
skype: emanuela.merelli , http://www.cs.unicam.it/merelli
2013-03-06
[Caml-list] SFM-13:DS school in Bertinoro -- last call for participation
***********************************************************
* *
* SFM-13:DS *
* *
* 13th International School on *
* Formal Methods for the Design of *
* Computer, Communication and Software Systems: *
* Dynamical Systems *
* *
* Bertinoro (Italy), 17-22 June 2013 *
* *
* http://www.sti.uniurb.it/events/sfm13ds/ *
* *
***********************************************************
* CALL FOR PARTICIPATION *
* (deadline: 21 March 2013) *
***********************************************************
GENERAL INFORMATION ABOUT SFM
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Formal methods are emerging in computer science as a prominent
approach to the rigorous design of computer, communication and
software systems.
The aim of the SFM series is to offer a good spectrum of
current research in foundations as well as applications of
formal methods, which can be of interest for graduate students
and young researchers who intend to approach the field.
This year SFM is an offspring of the workshops QAPL and MLQA
and is devoted to dynamical systems. It covers topics such as
chaotic dynamics, information theory, systems biology, hybrid systems,
quantum computing, and automata-based models and model checking.
COURSES AND LECTURERS
^^^^^^^^^^^^^^^^^^^^^
The school features the following lectures:
"Introduction to Dynamical Systems"
Herbert Wiklicky (Imperial College London, UK)
"Introduction to Chaotic Dynamics and Fractals"
Abbas Edalat (Imperial College London, UK)
"Information-Theoretic Security Analysis"
Boris Koepf (IMDEA Software, ES)
"Quantum Information Theory"
Renato Renner (ETH Zurich, CH)
"Quantitative Automata-Based Models and Model Checking"
Joost-Pieter Katoen (RWTH Aachen, DE)
"Fluid Analysis of Markov Models"
Jeremy Bradley (Imperial College London, UK)
"Discrete and Hybrid Methods in Systems Biology"
Oded Maler (VERIMAG, FR)
"ODE Analysis of Biological Systems"
Ion Petre (Abo Akademi, FI)
"Model Checking of Biological Models"
Lubos Brim (Masaryk Univ., CZ)
"Fluid Model Checking"
Luca Bortolussi (Univ. Trieste, IT)
"Checking Stability of Hybrid Systems"
Andreas Podelski (Univ. Freiburg, DE)
"Topological Quantum Computing"
Jiannis Pachos (Univ. Leeds, UK)
All participants will receive a copy of a tutorial book published by
Springer as a volume in the Lecture Notes in Computer Science series.
LOCATION
^^^^^^^^
SFM-13:DS will be held in the medieval hilltop town of Bertinoro.
This town is in Emilia Romagna, about 70 km south-east of Bologna,
at an elevation of about 230 m. It can be reached in a couple of
hours from the international airport "G. Marconi" of Bologna by
shuttle (from the airport to the railway station) + train (from
Bologna to Forli`) + bus/taxi (from the railway station to Bertinoro).
The closest airport is the "L. Ridolfi" airport of Forli`, which is
13 km away.
Bertinoro is close to many splendid locations such as Urbino,
Gradara, San Leo, and the Republic of San Marino, as well as some
less well-known locations like the thermal springs of Fratta Terme.
Bertinoro can also be a base for visiting some of the better-known
Italian locations such as Bologna, Rimini, Ravenna, Ferrara, Venezia,
Padova, Verona, Firenze, Pisa, and Siena.
Bertinoro itself is picturesque, with its narrow streets and
walkways winding around the central peak. The school will be held
at the Centro Residenziale Universitario (CRU), an ex-episcopal
fortress that has been converted by the University of Bologna into
a modern conference center with computing facilities and Internet
access. From the fortress, it is possible to enjoy a beautiful vista
stretching from the Apennines to the Adriatic coast and the Alps
over the Po Valley.
ORGANIZATION
^^^^^^^^^^^^
Scientific directors:
* Marco Bernardo (University of Urbino, IT)
* Erik de Vink (Eindhoven University of Technology, NL)
* Alessandra Di Pierro (University of Verona, IT)
* Herbert Wiklicky (Imperial College London, UK)
Secretary:
* Monica Michelacci (CRU Bertinoro, IT)
APPLICATION
^^^^^^^^^^^
Prospective participants should send by 21 March 2013
the application form, available on the school website,
to the two e-mail addresses below:
Marco Bernardo
marco.bernardo AT uniurb.it
Monica Michelacci
mmichelacci AT ceub.it
The registration fee is 600 euros and includes the school material.
The accommodation fee is 350 euros and covers the period June 16-23
(7 nights), double room (to share with another participant),
half board (breakfast and lunch, dinner of June 16 included,
lunch of June 23 excluded).
The reduced accommodation fee for the participants who do not
need a room is 100 euros and covers the period June 17-22
(6 lunches).
A very limited number of grants is available to cover part
of the registration fee (no grant can be requested to cover
the accommodation fee or the travel expenses).
Notification of accepted/rejected applications and grant requests
will be communicated by March 31.
Registration to the school is due by April 20.
No refund is possible for cancellation after May 15.
--
Caml-list mailing list. Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs
* *
* SFM-13:DS *
* *
* 13th International School on *
* Formal Methods for the Design of *
* Computer, Communication and Software Systems: *
* Dynamical Systems *
* *
* Bertinoro (Italy), 17-22 June 2013 *
* *
* http://www.sti.uniurb.it/events/sfm13ds/ *
* *
***********************************************************
* CALL FOR PARTICIPATION *
* (deadline: 21 March 2013) *
***********************************************************
GENERAL INFORMATION ABOUT SFM
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Formal methods are emerging in computer science as a prominent
approach to the rigorous design of computer, communication and
software systems.
The aim of the SFM series is to offer a good spectrum of
current research in foundations as well as applications of
formal methods, which can be of interest for graduate students
and young researchers who intend to approach the field.
This year SFM is an offspring of the workshops QAPL and MLQA
and is devoted to dynamical systems. It covers topics such as
chaotic dynamics, information theory, systems biology, hybrid systems,
quantum computing, and automata-based models and model checking.
COURSES AND LECTURERS
^^^^^^^^^^^^^^^^^^^^^
The school features the following lectures:
"Introduction to Dynamical Systems"
Herbert Wiklicky (Imperial College London, UK)
"Introduction to Chaotic Dynamics and Fractals"
Abbas Edalat (Imperial College London, UK)
"Information-Theoretic Security Analysis"
Boris Koepf (IMDEA Software, ES)
"Quantum Information Theory"
Renato Renner (ETH Zurich, CH)
"Quantitative Automata-Based Models and Model Checking"
Joost-Pieter Katoen (RWTH Aachen, DE)
"Fluid Analysis of Markov Models"
Jeremy Bradley (Imperial College London, UK)
"Discrete and Hybrid Methods in Systems Biology"
Oded Maler (VERIMAG, FR)
"ODE Analysis of Biological Systems"
Ion Petre (Abo Akademi, FI)
"Model Checking of Biological Models"
Lubos Brim (Masaryk Univ., CZ)
"Fluid Model Checking"
Luca Bortolussi (Univ. Trieste, IT)
"Checking Stability of Hybrid Systems"
Andreas Podelski (Univ. Freiburg, DE)
"Topological Quantum Computing"
Jiannis Pachos (Univ. Leeds, UK)
All participants will receive a copy of a tutorial book published by
Springer as a volume in the Lecture Notes in Computer Science series.
LOCATION
^^^^^^^^
SFM-13:DS will be held in the medieval hilltop town of Bertinoro.
This town is in Emilia Romagna, about 70 km south-east of Bologna,
at an elevation of about 230 m. It can be reached in a couple of
hours from the international airport "G. Marconi" of Bologna by
shuttle (from the airport to the railway station) + train (from
Bologna to Forli`) + bus/taxi (from the railway station to Bertinoro).
The closest airport is the "L. Ridolfi" airport of Forli`, which is
13 km away.
Bertinoro is close to many splendid locations such as Urbino,
Gradara, San Leo, and the Republic of San Marino, as well as some
less well-known locations like the thermal springs of Fratta Terme.
Bertinoro can also be a base for visiting some of the better-known
Italian locations such as Bologna, Rimini, Ravenna, Ferrara, Venezia,
Padova, Verona, Firenze, Pisa, and Siena.
Bertinoro itself is picturesque, with its narrow streets and
walkways winding around the central peak. The school will be held
at the Centro Residenziale Universitario (CRU), an ex-episcopal
fortress that has been converted by the University of Bologna into
a modern conference center with computing facilities and Internet
access. From the fortress, it is possible to enjoy a beautiful vista
stretching from the Apennines to the Adriatic coast and the Alps
over the Po Valley.
ORGANIZATION
^^^^^^^^^^^^
Scientific directors:
* Marco Bernardo (University of Urbino, IT)
* Erik de Vink (Eindhoven University of Technology, NL)
* Alessandra Di Pierro (University of Verona, IT)
* Herbert Wiklicky (Imperial College London, UK)
Secretary:
* Monica Michelacci (CRU Bertinoro, IT)
APPLICATION
^^^^^^^^^^^
Prospective participants should send by 21 March 2013
the application form, available on the school website,
to the two e-mail addresses below:
Marco Bernardo
marco.bernardo AT uniurb.it
Monica Michelacci
mmichelacci AT ceub.it
The registration fee is 600 euros and includes the school material.
The accommodation fee is 350 euros and covers the period June 16-23
(7 nights), double room (to share with another participant),
half board (breakfast and lunch, dinner of June 16 included,
lunch of June 23 excluded).
The reduced accommodation fee for the participants who do not
need a room is 100 euros and covers the period June 17-22
(6 lunches).
A very limited number of grants is available to cover part
of the registration fee (no grant can be requested to cover
the accommodation fee or the travel expenses).
Notification of accepted/rejected applications and grant requests
will be communicated by March 31.
Registration to the school is due by April 20.
No refund is possible for cancellation after May 15.
--
Caml-list mailing list. Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs
2013-03-04
[Caml-list] ARiSVe 2013 final call for papers
Call For Papers
1st International Workshop on Automated Reasoning in Software Verification
http://arisve2013.lri.fr
Monday, June 10, 2013
Lake Placid, NY, USA
Affiliated with CADE-24
Aims and Scope
The focus of the workshop is application of automated reasoning in the
context of software verification, and, more generally, automation in
software verification. Relevant topics include but are not limited to:
* specifics of verification-related automated reasoning tasks;
* efficient translation of high-level verification conditions to
logical languages of automated reasoning tools;
* handling of the prover's feedback: proofs, models, answer terms;
* logical theories of interest for program verification, decision
procedures, integration into existing ATP and SMT systems;
* combination of automated and user-assisted verification;
* tool presentations, tool comparisons, and benchmarks;
* experience reports on verification of complex algorithms and
real-life software with the use of automated reasoning tools.
Paper Submission and Proceedings
All submissions are reviewed by the program committee. We expect
that one author of every accepted paper will present their work at
the workshop.
Submissions are limited to 6-12 pages in the LaTeX EasyChair format
easychair.cls (http://www.easychair.org/publications/easychair.zip).
Technical details may be included in an appendix to be read at the
reviewers' discretion. Tool presentation papers and experience
reports are welcome.
Papers should be submitted through EasyChair,
at http://www.easychair.org/conferences/?conf=arisve2013
Submissions must be in PDF format. Electronic version of proceedings
will be freely distributed from the workshop web site.
Important Dates
* Abstract submission deadline: March 8, 2013
* Submission deadline: March 15, 2013
* Notification: April 10, 2013
* Camera ready versions due: May 10, 2013
* Workshop: June 10, 2013
Invited Speaker
K. Rustan M. Leino (Microsoft Research)
Program Committee
* June Andronick (NICTA)
* Clark Barrett (New York University)
* Ernie Cohen (Microsoft Corp.)
* Loïc Correnson (CEA)
* Gidon Ernst (Ausburg University)
* Jean-Christophe Filliâtre (CNRS), co-chair
* Alwyn Goodloe (NASA)
* Matthias Horbach (Koblenz University)
* Vladimir Klebanov (Karlsruhe Institute of Technology)
* Konstantin Korovin (The University of Manchester)
* Rosemary Monahan (National University of Ireland)
* Andrei Paskevich (Université Paris-Sud), co-chair
* Silvio Ranise (Fondazione Bruno Kessler)
--
Caml-list mailing list. Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs
1st International Workshop on Automated Reasoning in Software Verification
http://arisve2013.lri.fr
Monday, June 10, 2013
Lake Placid, NY, USA
Affiliated with CADE-24
Aims and Scope
The focus of the workshop is application of automated reasoning in the
context of software verification, and, more generally, automation in
software verification. Relevant topics include but are not limited to:
* specifics of verification-related automated reasoning tasks;
* efficient translation of high-level verification conditions to
logical languages of automated reasoning tools;
* handling of the prover's feedback: proofs, models, answer terms;
* logical theories of interest for program verification, decision
procedures, integration into existing ATP and SMT systems;
* combination of automated and user-assisted verification;
* tool presentations, tool comparisons, and benchmarks;
* experience reports on verification of complex algorithms and
real-life software with the use of automated reasoning tools.
Paper Submission and Proceedings
All submissions are reviewed by the program committee. We expect
that one author of every accepted paper will present their work at
the workshop.
Submissions are limited to 6-12 pages in the LaTeX EasyChair format
easychair.cls (http://www.easychair.org/publications/easychair.zip).
Technical details may be included in an appendix to be read at the
reviewers' discretion. Tool presentation papers and experience
reports are welcome.
Papers should be submitted through EasyChair,
at http://www.easychair.org/conferences/?conf=arisve2013
Submissions must be in PDF format. Electronic version of proceedings
will be freely distributed from the workshop web site.
Important Dates
* Abstract submission deadline: March 8, 2013
* Submission deadline: March 15, 2013
* Notification: April 10, 2013
* Camera ready versions due: May 10, 2013
* Workshop: June 10, 2013
Invited Speaker
K. Rustan M. Leino (Microsoft Research)
Program Committee
* June Andronick (NICTA)
* Clark Barrett (New York University)
* Ernie Cohen (Microsoft Corp.)
* Loïc Correnson (CEA)
* Gidon Ernst (Ausburg University)
* Jean-Christophe Filliâtre (CNRS), co-chair
* Alwyn Goodloe (NASA)
* Matthias Horbach (Koblenz University)
* Vladimir Klebanov (Karlsruhe Institute of Technology)
* Konstantin Korovin (The University of Manchester)
* Rosemary Monahan (National University of Ireland)
* Andrei Paskevich (Université Paris-Sud), co-chair
* Silvio Ranise (Fondazione Bruno Kessler)
--
Caml-list mailing list. Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs
Subscribe to:
Posts (Atom)