Klaus Havelund | 29 Jul 06:15 2014
Picon
Picon

[fm-announcements] RV 2014: Call for Participation


CALL FOR PARTICIPATION

RV 2014: 14th International Conference on Runtime Verification

September 22 - September 25, 2014, Toronto, Canada

http://rv2014.imag.fr


OVERVIEW

Runtime verification is concerned with monitoring and analysis of software and hardware system executions. Runtime verification techniques are important for system correctness, reliability, and robustness; they are complementary to conventional testing, and more practical than exhaustive formal verification. Runtime verification can be used prior to deployment, for testing, verification, and debugging purposes, and after deployment for ensuring reliability, safety, and security and for providing fault containment and recovery as well as online system repair. Topics of interest to the conference include:

  • specification languages
  • specification mining
  • program instrumentation
  • monitor construction techniques
  • logging, recording, and replay
  • fault detection, localization, containment, recovery and repair
  • program steering and adaptation
  • metrics and statistical information gathering
  • combination of static and dynamic analyses
  • program execution visualization
  • monitoring techniques for safety/mission-critical systems
  • monitoring distributed systems, cloud services, and big data applications
  • monitoring security and privacy policies

Application areas of runtime verification include safety/mission-critical systems, enterprise and systems software, autonomous and reactive control systems, health management and diagnosis systems, and system security and privacy.


INVITED TALKS


  • Kevin Driscoll
    Fellow at Honeywell Labs, USA
    Murphy Strikes Again
  • Assaf Schuster
    Professor of Computer Science, Computer Science Department, Technion, Israel
    Monitoring Big, Distributed, Streaming Data
  • Jeannette Wing
    President's Professor of Computer Science,
    Computer Science Department, Carnegie Mellon University, USA
    Formal Methods: An Industrial Perspective


INVITED TUTORIALS


  • Vijay K. Garg & Neeraj Mittal
    UT at Austin & UT at Dallas
    A Lattice-Theoretic Approach to Monitoring Distributed Computations
  • David Basin & Felix Klaedtke
    ETH-Zurich & NEC Labs, Europe
    Runtime Monitoring and Enforcement of Security Policies


VENUE


The Fields Institute for Research in Mathematical Sciences

222 College Street, Toronto, Ontario, Canada

http://www.fields.utoronto.ca/


REGISTRATION


Registration on line to Aug. 21, on site Sept. 22

Registration fees $575, after Aug. 21 $675

Student $350, after Aug. 21, $450


Fees include proceedings and 1x Conference banquet

Additional banquet tickets $80


Registration link:

http://www.fields.utoronto.ca/programs/scientific/14-15/RV2014/


ACCEPTED PAPERS


  • Pierre Fraigniaud, Sergio Rajsbaum and Corentin Travers. 
    On the Number of Opinions Needed for Fault-Tolerant Run-Time Monitoring in Distributed Systems
  • Simon Varvaressos, Kim Lavoie, Sebastien Gaboury and Sylvain Hallé.
    Multiple Ways to Fail: Generalizing a Monitor's Verdict for the Classification of Execution Traces
  • Clemens Ballarin.
    Two Generalisations of Roşu and Chen's Trace Slicing Algorithm A
  • Martin Hentschel, Richard Bubel and Reiner Hähnle.
    Symbolic Execution Debugger (SED) 
  • Jiannan Zhai, Nigamanth Sridhar and Jason Hallstrom.
    Supporting the Specification and Runtime Validation of Asynchronous Calling Patterns in Reactive Systems 
  • Emmanouil Koukoutos and Viktor Kuncak.
    Checking Data Structure Properties Orders of Magnitude Faster 
  • Maria Christakis, Patrick Emmisberger and Peter Müller.
    Dynamic Test Generation with Static Fields and Initializers 
  • Aravind Sukumaran-Rajam, Juan Manuel Martinez Caamano, Willy Wolff, Alexandra Jimborean and Philippe Clauss.
    Speculative Program Parallelization with Scalable and Decentralized Runtime Verification 
  • Christian Colombo and Yliès Falcone.
    Organising LTL Monitors over Distributed Systems with a Global Clock 
  • Erdal Mutlu, Vladimir Gajinov, Adrian Cristal, Serdar Tasiran and Osman Unsal.
    Dynamic Verification for Hybrid Concurrent Programming Models 
  • Hsi-Ming Ho, Joel Ouaknine and James Worrell.
    Online Monitoring of Metric Temporal Logic
  • David Basin, Germano Caronni, Sarah Ereth, Matúš Harvan, Felix Klaedtke and Heiko Mantel.
    Scalable Offline Monitoring 
  • David Basin, Felix Klaedtke, Srdjan Marinovic and Eugen Zalinescu.
    On Real-time Monitoring with Imprecise Timestamps 
  • Anand Yeolekar.
    Improving dynamic inference with variable dependence graph 
  • Ming Chai and Holger Schlingloff.
    Monitoring Systems with Extended Live Sequence Charts 
  • Laura Bozzelli and César Sánchez.
    Foundations of Boolean Stream Runtime Verification 
  • Mitra Tabaei Befrouei, Chao Wang and Georg Weissenbacher.
    Abstraction and Mining of Traces to Explain Concurrency-Bugs 
  • Stefan Mitsch and André Platzer.
    ModelPlex: Verified Runtime Validation of Verified Cyber-Physical System Models 
  • Johannes Geist, Kristin Y. Rozier and Johann Schumann.
    Runtime Observer Pairs and Bayesian Network Reasoners On-board FPGAs: Flight-Certifiable System Health Management for Embedded Systems 
  • Malte Isberner, Falk Howar and Bernhard Steffen
    The TTT Algorithm: A Redundancy-Free Approach to Active Automata Learning
  • Kim Lavoie, Corentin Leplongeon, Simon Varvaressos, Sebastien Gaboury and Sylvain Hallé.
    Portable Runtime Verification with Smartphones and Optical Codes 
  • Adel Dokhanchi, Bardh Hoxha and Georgios Fainekos
    On-Line Monitoring for Temporal Logic Robustness 
  • Jeff Huang, Cansu Erdogan, Yi Zhang, Brandon Moore, Qingzhou Luo, Aravind Sundaresan and Grigore Rosu.
    ROSRV: Runtime Verification for Robots 
  • Qingzhou Luo, Yi Zhang, Choonghwan Lee, Dongyun Jin, Patrick Meredith, Traian Serbanuta and Grigore Rosu.
    RV-Monitor: Efficient Parametric Runtime Verification with Simultaneous Properties 
  • Duc Hiep Chu, Joxan Jaffar and Vijayaraghavan Murali.
    Lazy Symbolic Execution for Enhanced Learning 
  • Kuei Sun, Daniel Fryer, Ashvin Goel, Dai Qin and Angela Demke Brown.
    Robust Consistency Checking for Modern Filesystems 
  • Ayoub Nouri, Balaji Raman, Marius Bozga, Axel Legay and Saddek Bensalem.
    Faster Statistical Model Checking by Means of Abstraction and Learning


CHAIRS AND ORGANIZERS


  • General Chair: Sebastian Fischmeister (University of Waterloo, Canada).
  • PC co-Chairs: 
    • Borzoo Bonakdarpour (McMaster University, Canada)
    • Scott Smolka (Stony Brook Universtiy, USA)
  • Tools Track Chair: Ezio Bartocci (TU Vienna, Austria)
  • Runtime Monitoring Competition Co-Chairs:
    • Ezio Bartocci (TU Vienna, Austria)
    • Borzoo Bonakdarpour (McMaster University, Canada)
    • Ylies Falcone (Université Joseph Fourier, France)
  • Publicity Chair: Ylies Falcone (Université Joseph Fourier, France)
  • Local Arrangements Chair: Patrick Lam (University of Waterloo, Canada)


FURTHER INFORMATION


More information about RV2014 is available from the conference web site:

http://rv2014.imag.fr

---
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 
------------------------------------------------------------------------------
Infragistics Professional
Build stunning WinForms apps today!
Reboot your WinForms applications with our WinForms controls. 
Build a bridge from your legacy apps to the future.
http://pubads.g.doubleclick.net/gampad/clk?id=153845071&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Ramana Kumar | 29 Jul 11:02 2014
Picon
Picon

quieter output from bin/build

Is there some way to turn off the "Saved theorem" etc. messages during a build of HOL? I notice there's a "--quiet" option for Holmake (although not for bin/build), but it seems not to suppress very much.
------------------------------------------------------------------------------
Infragistics Professional
Build stunning WinForms apps today!
Reboot your WinForms applications with our WinForms controls. 
Build a bridge from your legacy apps to the future.
http://pubads.g.doubleclick.net/gampad/clk?id=153845071&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Ramana Kumar | 24 Jul 17:04 2014
Picon
Picon

math mode printing of strings

By default the munger doesn't do anything special to strings; the usual pretty-printing behaviour is to print the elements of the string without any separators between double-quotes. In math mode, the contents of the string thus are treated as LaTeX variables and appear in italics with too much space.

Any ideas on a good way to make the munger wrap the contents of a string, perhaps with a new \HOLString command?

My guess is this probably requires removing whatever rule pretty-prints strings and putting in a new one, but if there's anything less heavy-weight that could be done I'd be happy to know about it.
------------------------------------------------------------------------------
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
Ramana Kumar | 24 Jul 14:15 2014
Picon
Picon

tweaking printing of []

HOL's pretty-printer usually prints the empty list as "[]", which I believe is produced by two separate tokens (one for each bracket) via a "listform" parsing/printing rule.

In LaTeX math mode (generated using HOL's math mode munger) "[]" does not look nice: it needs a bit of space inside. What would be the best approach to making the printer generate such space? Could I, perhaps, override the empty list (but not other lists) with a special token that I can then override to some custom LaTeX? Or perhaps there's a better way?
------------------------------------------------------------------------------
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
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
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

------------------------------------------------------------------------------
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
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
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

------------------------------------------------------------------------------
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
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

Gmane