DIFTS14 | 15 Jul 09:13 2014
Picon

DIFTS14 - SECOND Call for Papers

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

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

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

Lausanne, Switzerland
October 20, 2014

  
IMPORTANT DATES

Abstract submission:        July 28, 2014
Paper submission:           August 4, 2014
Author notification:        September 1, 2014

  
DIFTS (Design and Implementation of Formal Tools and
Systems) workshop
emphasizes insightful experiences in formal tools and
systems design.
The workshop provides an opportunity for discussing
(Continue reading)

DIFTS14 | 15 Jul 09:16 2014
Picon

DIFTS14 - SECOND Call for Papers

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

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

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

Lausanne, Switzerland
October 20, 2014

  
IMPORTANT DATES

Abstract submission:        July 28, 2014
Paper submission:           August 4, 2014
Author notification:        September 1, 2014

  
DIFTS (Design and Implementation of Formal Tools and
Systems) workshop
emphasizes insightful experiences in formal tools and
systems design.
The workshop provides an opportunity for discussing
(Continue reading)

Alwen Tiu | 17 Jul 16:23 2014
Picon

Call for Papers: CPP 2015 -- Certified Programs and Proofs

[Apologies if you received this more than once]

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

The 4th ACM SIGPLAN Conference on
Certified Programs and Proofs (CPP 2015)

Mumbai, India, 12 - 14 January 2015

http://cpp2015.inria.fr

Co-located with POPL 2015 (http://popl.mpi-sws.org/2015/)


Call for Papers
===============

CPP is an international forum on theoretical and practical topics in
all areas, including computer science, mathematics, and education,
that consider certification as an essential paradigm for their
work. Certification here means formal, mechanized verification of some
sort, preferably with production of independently checkable
certificates.

CPP 2015 is the fourth in the CPP conference series and will be co-located
with POPL 2015 in Mumbai from 12 - 14 January 2015.

Important dates
---------------
Abstract submission:     3 October 2014, anywhere on Earth (11:59 pm, UTC-12)
Full paper submission:    10 October 2014, anywhere on Earth (11:59 pm, UTC-12)
Notification:         29 November 2014
Camera-ready deadline:    15 December 2014
Conference dates:    12 - 14 January 2015


Scope
-----
Suggested, but not exclusive, specific topics of interest for
submissions include:

- certified or certifying programming, compilation, linking, OS
  kernels, runtime systems, and security monitors;
- program logics, type systems, and semantics for certified code;
- certified decision procedures, mathematical libraries, and
  mathematical theorems;
- proof assistants and proof theory;
- new languages and tools for certified programming;
- program analysis, program verification, and proof-carrying code;
- certified secure protocols and transactions;
- certificates for decision procedures, including linear algebra,
  polynomial systems, SAT, SMT, and unification in algebras of
  interest;
- certificates for semi-decision procedures, including equality,
  first-order logic, and higher-order unification;
- certificates for program termination;
- logics for certifying concurrent and distributed programs;
- higher-order logics, logical systems, separation logics, and logics
  for security;
- teaching mathematics and computer science with proof assistants.


Submission instructions
-----------------------
Submitted papers should not exceed 12 pages in the ACM SIGPLAN
Proceedings format. Shorter papers are welcome and will be given equal
consideration. The proceedings of the conference will be published
by the ACM. Templates for ACM SIGPLAN format can be found on the
ACM SIGPLAN website:

http://www.sigplan.org/Resources/Author.

Papers should be submitted in PDF format, through the EasyChair
submission page:

https://www.easychair.org/conferences/?conf=cpp2015

Each submission must be written in English and provide sufficient
detail to allow the program committee to assess the merits of the
paper. It should begin with a succinct statement of the issues, a
summary of the main results, and a brief explanation of their
significance and relevance to the conference, all phrased for the
non-specialist. Technical and formal developments directed to the
specialist should follow. Whenever appropriate, the submission should
come along with a formal development, using whatever prover, e.g.,
Agda, Coq, Elf, HOL, HOL-Light, Isabelle, Matita, Mizar, NQTHM, PVS,
Vampire, etc. References and comparisons with related work should be
included. Papers not conforming to the above requirements concerning
format and length may be rejected without further consideration.

The results must be unpublished and not submitted for publication
elsewhere, including the proceedings of other published conferences or
workshops. The PC chairs should be informed of closely related work
submitted to a conference or journal in advance of
submission. Original formal proofs of known results in mathematics or
computer science are among the targets. One author of each accepted
paper is expected to present it at the conference.


Program Committee
-----------------
Andreas Abel, Chalmers and Gothenburg University, Sweden
June Andronick, NICTA and UNSW, Sydney, Australia
Nick Benton, Microsoft Research, Cambridge, UK
Lennart Beringer, Princeton University, USA
James Brotherston. University College London, UK
Kaustuv Chaudhuri, Inria, Saclay, France
Amy Felty, University of Ottawa, Canada
Chung-Kil Hur , Seoul National University, Korea
Naoki Kobayashi, University of Tokyo, Japan
Xavier Leroy (co-chair), Inria, Paris-Rocquencourt, France
Leonardo de Moura , Microsoft Research, Redmond, USA
Magnus Myreen , University of Cambridge, UK
Vivek Nigam, Federal University of Paraíba, Brasil
Tobias Nipkow, Technische Universität München. Germany
Christine Paulin-Mohring, Université Paris-Sud, France
Natarajan Raja, Tata Institute of Fundamental Research, Mumbai, India
Gert Smolka, Saarland University, Germany
Alwen Tiu (co-chair), Nanyang Technological University, Singapore
Stephanie Weirich , University of Pennsylvania, USA
------------------------------------------------------------------------------
Want fast and easy access to all the code in your enterprise? Index and
search up to 200,000 lines of code with a free copy of Black Duck
Code Sight - the same software that powers the world's largest code
search on Ohloh, the Black Duck Open Hub! Try it now.
http://p.sf.net/sfu/bds
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Klaus Havelund | 17 Jul 08:25 2014
Picon
Picon

[fm-announcements] Call for Papers: NASA Formal Methods (NFM) 2015


CALL FOR PAPERS

The 7th NASA Formal Methods Symposium

http://www.NASAFormalMethods.org/nfm2015

27 - 29 April 2015
Pasadena, California, USA

THEME

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

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

TOPICS

Topics of interest include, but are not limited to:

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

IMPORTANT DATES

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

LOCATION AND COST

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

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

SUBMISSION DETAILS

There are two categories of submissions:

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

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

PC CHAIRS

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

PROGRAMME COMMITTEE

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

STEERING COMMITTEE

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

---
To opt-out from this mailing list, send an email to

fm-announcements-request <at> lists.nasa.gov

with the word 'unsubscribe' as subject or in the body. You can also make the request by contacting

fm-announcements-owner <at> lists.nasa.gov 
------------------------------------------------------------------------------
Want fast and easy access to all the code in your enterprise? Index and
search up to 200,000 lines of code with a free copy of Black Duck
Code Sight - the same software that powers the world's largest code
search on Ohloh, the Black Duck Open Hub! Try it now.
http://p.sf.net/sfu/bds
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
David Sanan | 10 Jul 16:02 2014
Picon

how to provide a witness of a forall quantifier to generate a counterexample?

Hi all,


I am trying to prove this goal and n=1 in assumption 2 is a counterexample leading to ¬(¬TCn R n x x ∨ ∃n'.
TCn R n' x x ∧ n' < n), where TCn is the NRC relation without reflexivity and  ∀n. TCn R n x y  ⇒ n>0.

F
------------------------------------
  0.  unique_suc R
  1.  R⁺ x x
  2.  ∀n. ¬TCn R n x x ∨ ∃n'. TCn R n' x x ∧ n' < n
  3.  TCn R m x x

Is it possible to provide a witness to produce a counterexample?

Many thanks,
David.
------------------------------------------------------------------------------
Open source business process management suite built on Java and Eclipse
Turn processes into business applications with Bonita BPM Community Edition
Quickly connect people, data, and systems into organized workflows
Winner of BOSSIE, CODIE, OW2 and Gartner awards
http://p.sf.net/sfu/Bonitasoft
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
SYNASC 2014 | 1 Jul 11:08 2014
Picon

[Extended deadlines] CFP for workshops in conjunction with SYNASC 2014

Call for Papers for Workshops in conjunction with
-------------------------------------------------

                       SYNASC 2014

              16th International Symposium on
   Symbolic and Numeric Algorithms for Scientific Computing
         September 22-25, 2014, Timisoara, Romania
           	  http://synasc.ro/2014
	      http://synasc14.info.uvt.ro

Extended deadlines:
-------------------

Submission of papers (extended): 11 July 2014
Notification of acceptance: 31 July 2014

 * Workshop on HPC research services (HPCReS)
           http://host.hpc.uvt.ro/events/hpcres-2014-international-workshop-on-hpc-research-services/ 

 * Workshop on Management of Resources and Services in Cloud and Sky Computing (MICAS)
           http://amicas.hpc.uvt.ro/micas-2014
------------------------------------------------------------------------------------

Submission of papers (extended): 15 July 2014
Notification of acceptance: 30 July 2014

 * Workshop on Computational Topology in Image Context (CTIC)
           http://ctic2014.synasc.ro/index.html

-------------------------------------------------------------------------------------
Submission of papers (extended): 21 July 2014 
Notification of acceptance: 17 August 2014

 * Workshop on Agents for Complex Systems (ACSys)
           http://synasc.ro/2014/workshops/acsys-2014 

 * Workshop on GIC and Hydrologic Modeling (HydroGIS)    
           http://synasc.ro/2014/workshops/hydrogis-2014

 * Workshop on Iterative Approximation of Fixed Points (IAFP)
           http://synasc.ro/2014/workshops/iafp-2014

 * Workshop on Natural Computing and Applications (NCA)
           http://synasc.ro/2014/workshops/nca-2014

-----------
SYNASC 2014
West University of Timisoara
Department of Computer Science
Bd. V. Parvan 4, 300223 Timisoara, Romania
tel: + (40) 256 592195, +(40) 256 592389
fax: + (40) 256 592316, +(40) 256 592380
e-mail: synasc14 <at> synasc.ro

------------------------------------------------------------------------------
Open source business process management suite built on Java and Eclipse
Turn processes into business applications with Bonita BPM Community Edition
Quickly connect people, data, and systems into organized workflows
Winner of BOSSIE, CODIE, OW2 and Gartner awards
http://p.sf.net/sfu/Bonitasoft
Tsung-Yi Ho | 3 Jul 09:00 2014
Picon

Call for Participat​ion - ACM Student Research Competitio​n at ICCAD 2014

[Apologies if you receive multiple copies of this email]

ACM Student Research Competition at ICCAD 2014 (SRC <at> ICCAD'14)

DEADLINE: August 15, 2014 
Online Submission: https://www.easychair.org/conferences/?conf=srciccad14
 
Sponsored by Microsoft Research, the ACM Student Research Competition is an internationally recognized venue enabling undergraduate and graduate students who are ACM members to:

  • Experience the research world -- for many undergraduates this is a first!
  • Share research results and exchange ideas with other students, judges, and conference attendees
  • Rub shoulders with academic and industry luminaries
  • Understand the practical applications of their research
  • Perfect their communication skills
  • Receive prizes and gain recognition from ACM and the greater computing community.

The ACM Special Interest Group on Design Automation (ACM SIGDA) is organizing such an event in conjunction with the International Conference on Computer Aided Design (ICCAD). Authors of accepted submissions will get travel grants from ACM/Microsoft to attend the event at ICCAD. The event consists of several rounds, as described at http://www.acm.org/src/participate.html and http://www.acm.org/src/about.html , where you can also find more details on student eligibility and timeline.
 
The first-place winner in the graduate category at SRC <at> ICCAD'13, Aadithya Karthik (University of California, Berkeley), also won first place in the 2014 ACM SRC Grand Finals: http://src.acm.org.
 
Details on abstract submission:
Research projects from all areas of design automation are encouraged. The author submitting the abstract must still be a student at the time the abstract is due. Each submission should be made on the EasyChair submission site. Please include the author's name, affiliation, postal address, and email address; research advisor's name; ACM student member number; category (undergraduate or graduate); research title; and an extended abstract (maximum 2 pages or 800 words) containing the following sections:

  • Problem and Motivation: This section should clearly state the problem being addressed and explain the reasons for seeking a solution to this problem.
  • Background and Related Work: This section should describe the specialized (but pertinent) background necessary to appreciate the work. Include references to the literature where appropriate, and briefly explain where your work departs from that done by others. Reference lists do not count towards the limit on the length of the abstract.
  • Approach and Uniqueness: This section should describe your approach in attacking the problem and should clearly state how your approach is novel.
  • Results and Contributions: This section should clearly show how the results of your work contribute to computer science and should explain the significance of those results. Include a separate paragraph (maximum of 100 words) for possible publication in the conference proceedings that serves as a succinct description of the project.
  • Single paper summaries (or just cut & paste versions of published papers) are inappropriate for the ACM SRC. Submissions should include at least one year worth of research contributions, but not subsuming an entire doctoral thesis load.

Note that this event is different than other ACM/SIGDA sponsored or supported events at DAC or ICCAD: YSSP brings together seniors and 1st year graduate students at DAC, UBooth features demos from research groups, DASS allows graduate students to get up to speed on lectures on design automation, while the PhD Forum showcases post-proposal PhD research at DAC and the CADathlon allows graduate students to compete in a programming contest at ICCAD. The ACM Student Research Competition allows both graduate and undergraduate students to discuss their research with student peers, as well as academic and industry researchers, in an informal setting, while enabling them to attend DAC and compete with other ACM SRC winners from other computing areas in the ACM Grand Finals. Travel grant recipients cannot receive travel support from any other ICCAD or ACM/SIGDA sponsored program.
 
Online Submission - EasyChair:
https://www.easychair.org/conferences/?conf=srciccad14
 
Important dates:
Abstract submission deadline:  August 15, 2014 
Acceptance notification: September 15, 2014
Poster session at ICCAD: Monday, November 3, 2014
Presentation session at ICCAD: Tuesday, November 4, 2014
Award winners announced at ACM SIGDA Dinner: Tuesday, November 4, 2014
Grand Finals winners honored at ACM Awards Banquet: June 2015
 
Requirement:
Students submitting and presenting their work at SRC <at> ICCAD'14 are required to be members of both ACM and ACM SIGDA.
 
Organizers:
Miroslav Velev (Aries Design Automation, U.S.A.)
Tsung-Yi Ho (National Cheng Kung University, Taiwan)


--
Tsung-Yi Ho, Ph.D.,
Associate Professor,
Department of Computer Science and Information Engineering,
National Cheng Kung University,
No. 1, University Rd.,
Tainan, Taiwan 70101.
Phone: 886-6-2757575 ext. 62552   Fax: 886-6-2747076
Email: tyho <at> csie.ncku.edu.tw
Website: http://eda.csie.ncku.edu.tw

------------------------------------------------------------------------------
Open source business process management suite built on Java and Eclipse
Turn processes into business applications with Bonita BPM Community Edition
Quickly connect people, data, and systems into organized workflows
Winner of BOSSIE, CODIE, OW2 and Gartner awards
http://p.sf.net/sfu/Bonitasoft
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
lina.ye | 4 Jul 14:27 2014
Picon
Picon

Call for Participation: SEFM 2014

Our apologies if you have received multiple copies.

*************************************
*      Call for Participation       *
*************************************

12th International Conference on Software Engineering and Formal Methods
Grenoble, France

September 1-5, 2014

http://sefm2014.inria.fr/

*************************************

***** Dates *****

- Workshops: September 1-2, 2014
- Conference: September 3-5, 2014

***** Keynote Speakers *****

- Xavier Leroy "Formal proofs of code generation and verification
tools" (9:00-10:00, Spetember 3, 2014)

- Joost-Pieter Kaoten "Model Checking Gigantic Markov Models"
(9:00-10:00, Spetember 4, 2014)

- Patrice Godefroid "500 Machine-Years of Software Model Checking and
SMT Solving" (9:00-10:00, Spetember 5, 2014)

***** Conference Program *****

Eight exciting sessions of best research & practice papers presenting
current researches and applications of software engineering and formal
methods.

For more details, please check http://sefm2014.inria.fr/program/  

***** Worshops *****

Five colocated workshops gathering both local and international,
academic and industrial professionals, for promising discussions

- HOFM 2014: Human-Oriented Formal Methods 2014 (September 1, 2014)

- MoKMaSD 2014 : 3RD INTERNATIONAL SYMPOSIUM ON Modelling and
Knowledge Management applications : Systems and Domains (September 2,
2014)

- OpenCert 2014 : 8th International Workshop on Foundations and
Techniques for Open Source Software Certification (September 1, 2014)

- SaFoMe 2014 : 1st International Workshop on Safety and Formal
Methods (September 1, 2014)

- WS-FMDS 2014 : 4th Workshop on Formal Methods in the Development of
Software (September 2, 2014)

For more details, please see http://sefm2014.inria.fr/workshops/

***** Registration Fees *****

Early Registration: Up to 20 July, 2014

- workshop 1 day: 70 (student); 90 (full)
- workshop 2 days: 130 (student); 160 (full)
- conference: 330 (student); 370 (full)

Late Registration: From 21 July, 2014

- workshop 1 day: 100 (student); 120 (full)
- workshop 2 days: 160 (student); 190 (full)
- conference: 380 (student); 420 (full)

 
Register Now at http://sefm2014.inria.fr/registration/

*************************************

------------------------------------------------------------------------------
Open source business process management suite built on Java and Eclipse
Turn processes into business applications with Bonita BPM Community Edition
Quickly connect people, data, and systems into organized workflows
Winner of BOSSIE, CODIE, OW2 and Gartner awards
http://p.sf.net/sfu/Bonitasoft
Juan Boubeta Puig | 1 Jul 17:35 2014
Picon

Invitation to submit a chapter proposal on SOA 2.0

Dear colleague,

Due to your expertise in the topics related to the book Service-Oriented Architecture in the Era of Big Data, we kindly invite you to submit a chapter proposal.

You can find all the details of the call for chapter at http://www.igi-global.com/publish/call-for-papers/call-details/1386; please find also attached a pdf with the main information of the call for chapter including the editorial board.

If you are interested in submitting the chapter please submit it through the “Propose a chapter” button in http://www.igi-global.com/publish/call-for-papers/call-details/1386 no later than July the 25th.

If you have any colleague which might be interested in submitting a proposal, please do not hesitate to forward him the call for chapters. 

We will be looking forward to your contribution,

Regards,

Juan & Guadalupe
(Guest Editors)

--
Juan Boubeta Puig
Grupo UCASE de Ingeniería del Software / UCASE Software Engineering Research Group
Departamento de Ingeniería Informática / Department of Computer Science and Engineering
Escuela Superior de Ingeniería / School of Engineering
Universidad de Cádiz / University of Cádiz
C/ Chile nº 1
11002 - Cádiz (Spain)
Tel (+34) 956 015692  


------------------------------------------------------------------------------
Open source business process management suite built on Java and Eclipse
Turn processes into business applications with Bonita BPM Community Edition
Quickly connect people, data, and systems into organized workflows
Winner of BOSSIE, CODIE, OW2 and Gartner awards
http://p.sf.net/sfu/Bonitasoft
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
lina.ye | 4 Jul 17:11 2014
Picon
Picon

ACM SAC 2015: Software Verification and Testing Track - Second CfP

==================================================
30th Annual ACM Symposium on Applied Computing
Software Verification and Testing Track
April 13 - 17, 2015, Salamanca, Spain

More information:
http://fmt.cs.utwente.nl/conferences/sac-svt2015/ and
http://www.acm.org/conferences/sac/sac2015/
===================================================

Important dates
---------------
* September 12, 2014: Submission of regular papers
* November 17, 2014: Notification of paper acceptance/rejection
* December 8, 2013: Camera-ready copies of accepted papers

ACM Symposium on Applied Computing
----------------------------------
The ACM Symposium on Applied Computing (SAC) has gathered scientists
from different areas of computing over the past twenty-nine
years. The forum represents an opportunity to interact with different
communities sharing an interest in applied computing.

SAC 2015 is sponsored by SIGAPP and will be held at the UNESCO world
heritage city of Salamanca in Spain.

Software Verification and Testing Track
---------------------------------------
We invite authors to submit new results in formal verification and
testing, as well as development of technologies to improve the
usability of formal methods in software engineering. Also welcome are
detailed descriptions of applications of mechanical verification to
large scale software. Possible topics include, but are not limited to:

- model checking
- theorem proving
- correct by construction development
- model-based testing
- verification-based testing
- symbolic execution
- static and run-time analysis
- abstract interpretation
- analysis methods for dependable systems
- software certification and proof carrying code
- fault diagnosis and debugging
- verification of large scale software systems
- real world applications and case studies applying software verification

Submissions Guidelines
----------------------
Paper submissions must be original, unpublished work. Submissions
should be in electronic format, via the START site:
http://www.acm.org/conferences/sac/sac2015/Paper-SubmissionUploadPage.htm

Author(s) name(s) and address(es) must not appear in the body of the
paper, and self-reference should be avoided and made in the third
person. Submitted paper will undergo a blind review process. Authors
of accepted papers should submit an editorial revision of their papers
that fits within six two-column pages (an extra two pages, to a total
of eight pages, may be available at a charge). Please comply to this
page limitation already at submission time. Accepted papers will be
published in the ACM SAC 2015 proceedings.

Paper registration is required, allowing the inclusion of the
paper/poster in the conference proceedings. An author or a proxy
attending SAC MUST present the paper. This is a requirement for the
paper/poster to be included in the ACM/IEEE digital library. No-show
of scheduled papers and posters will result in excluding them from the
ACM/IEEE digital library.

A special issue of Science of Computer Programming has been
confirmed. Selected papers will be invited for submission, and will be
peer-reviewed according to the standard policy of Science of Computer
Programming.

Student Research Competition
----------------------------
As before, SAC 2015 organises a Student Research Competition (SRC)
Program to provide graduate students the opportunity to meet and
exchange ideas with researchers and practitioners in their areas of
interest. Guidelines and information about the SRC program can be
found at http://www.acm.org/conferences/sac/sac2015/. Submission to
the SRC program should be in electronic form via the following website
http://www.acm.org/conferences/sac/sac2015/SRC-SubmissionUploadPage.htm

Program Committee 
-----------------
Laura Brandan Briones, National University of Cordoba, Argentina
Maximiliano Cristiá, Universidad Nacional de Rosario, Argentina
Marco Faella, University of Naples, Italy
Ylies Falcone, University of Grenoble Alpes, France
Tingting Han, University of London, UK
Fabrice Kordon, University Pierre et Marie Curie, France
Stefan Leue, University of Konstanz, Germany
Shaoying Liu, Hosei University, Japan
Malte Lochau, Darmstadt University, Germany
Annabelle McIver, Macquarie University, Australia
Mercedes Merayo, Universidad Complutense de Madrid, Spain
Dominique Mery, University of Lorraine, France
Mohammad Mousavi, Halmstad University, Sweden
Brian Nielsen, Aalborg University, Denmark
Jun Pang, University of Luxembourg, Luxembourg
Corina Pasareanu, NASA Ames, USA
Wishnu Prasetya, Utrecht University, The Netherlands
Marjan Sirjani, Reykjavik University, Iceland
Hasan Sözer, Özyegin University, Turkey
Tanja Vos, Valencia University, Spain
Anton Wijs, Eindhoven University of Technology, The Netherlands
Liu Yang, Nanyang Technological University, Singapore
Gianluigi Zavattaro, University of Bologna, Italy
Lijun Zhang, Chinese Academy of Sciences, China

Program Committee Chairs
-----------------
Gwen Salaün, University of Grenoble Alpes, France
Marielle Stoelinga, University of Twente, Netherlands

------------------------------------------------------------------------------
Open source business process management suite built on Java and Eclipse
Turn processes into business applications with Bonita BPM Community Edition
Quickly connect people, data, and systems into organized workflows
Winner of BOSSIE, CODIE, OW2 and Gartner awards
http://p.sf.net/sfu/Bonitasoft
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
DIFTS14 | 25 Jun 16:18 2014
Picon

DIFTS14 - FIRST Call for Papers

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

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

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

Lausanne, Switzerland
October 20, 2014

  
IMPORTANT DATES

Abstract submission:        July 28, 2014
Paper submission:           August 4, 2014
Author notification:        September 1, 2014

  
DIFTS (Design and Implementation of Formal Tools and
Systems) workshop
emphasizes insightful experiences in formal tools and
systems design.
The workshop provides an opportunity for discussing
engineering aspects and
various design decisions required to put formal tools and
systems into
practical use. In the past, we have invited speakers who
have shared their
deep insights and discussed the practices followed in the
Industry towards
adopting formal methods. It provides a forum for sharing
challenges and
solutions that are original with ground breaking results.

The DIFTS workshop is co-located with FMCAD14 and
MEMOCODE14.

TOPICS OF INTEREST

DIFTS takes a broad view of the formal tools/systems area,
and solicits
contributions from domains including, but not restricted
to, decision
procedures, verification, testing, validation, diagnosis,
debugging, and
synthesis. This workshop encourages and appreciates system
development
activities, and facilitates transparency in the
experimentation. It will also
serve as a platform to discuss open problems and future
challenges in
practicing formal methods.

INVITED SPEAKERS

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

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

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

  
SUBMISSION

The workshop specifically solicits contributions with
substantial engineering
details that often do not get published but have
significant practical impact.

Papers in the following two categories are solicited: (a)
system category
(10 pages, double column, 11pt), and (b) tool category (8
pages, double
column, 11pt).

In the system category, we invite papers that have
original ideas accompanied
with novel integration techniques, adequate
design/implementation details,
important design choices made and explored, and good
experimental results.

In the tool category, we invite papers that focus
primarily on the engineering
aspects of some known/popular algorithm, with significant
emphasis on the
design/implementation details, and various design choices
made to advance
current state-of-the-art approaches.

The page limit for submissions in the system category is
10 pages in double
column format and for submissions in the tool category is
8 pages in double
column format.

Submission of papers should be made electronically in PDF
format via EasyChair.

  
EVALUATION

To keep maintain uniformity and fairness in the reviewing
process, the program
committee will evaluate the technical contribution of each
submission based on
the following guidelines: the paper should provide enough
details for others to
reproduce the results; and should solve a clearly-stated
problem that is
significant and has wide interest; and the paper should
provide enough
motivation for the design choices made. Overall, the paper
should also clearly
identify what the main contributions of the work are.

PUBLICATION

All accepted contributions will be included in informal
proceedings.
High quality submissions will be considered for a special
issue
of journals such as  FMSD (Formal Methods in System
Design) or
IEEE TC (Transactions on Computers).

  
ORGANIZATION

PROGRAM CHAIRS

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

PROGRAM COMMITTEE

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

WEBMASTERS

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

------------------------------------------------------------------------------
Open source business process management suite built on Java and Eclipse
Turn processes into business applications with Bonita BPM Community Edition
Quickly connect people, data, and systems into organized workflows
Winner of BOSSIE, CODIE, OW2 and Gartner awards
http://p.sf.net/sfu/Bonitasoft

Gmane