Klaus Havelund | 30 Aug 16:23 2014

[fm-announcements] Second call for papers: NASA Formal Methods - NFM 2015


The 7th NASA Formal Methods Symposium


27 – 29 April 2015
Pasadena, California, USA


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


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


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.


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.


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


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
Susanne Graf, VERIMAG, France
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 Yvonne 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


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 Yvonne 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 
Slashdot TV.  
Video for Nerds.  Stuff that matters.
hol-info mailing list
hol-info <at> lists.sourceforge.net
Ramana Kumar | 21 Aug 19:52 2014


Hi all,

Yong Kiam showed me something very useful today, so I'd like to share it with you all. If you're using HOL with Poly/ML, then there are functions PolyML.SaveState.saveState and PolyML.SaveState.loadState, both of type string -> unit, which save the state of the REPL in a file (the string is the filename). This can be used in the middle of an interactive proof, in the middle of a long script file, to avoid the need to rebuild if the session is exited (accidentally or not).

Of course this doesn't help if there are logical reasons why things need to be rebuilt, but as long as those can be ignored...

Slashdot TV.  
Video for Nerds.  Stuff that matters.
hol-info mailing list
hol-info <at> lists.sourceforge.net
Gwen.Salaun | 18 Aug 17:40 2014

Postdoc Position on Verification of Asynchronously Communicating Systems, Inria/LIG, Grenoble, France

The Convecs team (Inria Grenoble Rhône-Alpes research center / LIG
laboratory) recruits a postdoc. More information at:


Applications should be addressed directly to Gwen Salaün, preferably
by e-mail. Applications received after October 10th, 2014 might not be
considered if a candidate has been selected already. 

hol-info mailing list
hol-info <at> lists.sourceforge.net
Kristin Yvonne Rozier | 16 Aug 07:23 2014

[fm-announcements] Call for Highlights: Aerospace America Intelligent Systems Year In Review


Please consider submitting a highlight about your work! It is only 150 
words and it would really help to call attention to the important role 
of formal methods in the future of aerospace!


                       Call for Highlights

             Intelligent Systems 2014 Year In Review
                   Aerospace America magazine

                   Due date: August 25, 2014 (firm)

This is a call for submissions for the "Year In Review" December, 2014 
issue of Aerospace America magazine. We are looking for summaries of 
interesting aerospace applications of intelligent systems, of 
approximately 150 words in length, with an accompanying graphic if 
possible. Each highlight will be integrated within an overall narrative, 
so key organizations/affiliations should be identified within the text 
to enable proper credit to be given; including a URL for further 
information on your work is required. The AIAA Intelligent Systems 
Technical Committee will select, from among all submissions received, 
six that will be highlighted in the year-end issue of Aerospace America 

Deadline: Monday, August 25, 2014 (firm)
Submit through EasyChair: https://easychair.org/conferences/?conf=yir2014

* 150 words
* describing an advancement in research relating to aerospace 
intelligent systems
* describing work that occurred or is projected to occur between January 
and December, 2014
* identifying key organizations/affiliations
* including a URL for further information and a word or phrase to 
hyperlink it to in the onine version of the article (Please list the 
word, phrase, or lab name to be hyperlinked after the highlight text, 
with the desired URL.)
* with an accompanying graphic, if possible: include after the highlight 
text a URL for a high-resolution JPG; include photo credit and caption

* Submission Deadline: August 25, 2014 (firm)
* Notification of selection for Aerospace America article: September 1, 2014
* Proofs go out for author approval of AIAA ISTC newsletter: October 1, 2014
* Aerospace America article is published: December 1, 2014
* AIAA ISTC highlight newsletter is published: December 1, 2014

This article will cover the most important developments this year in 
aerospace intelligent systems. Breakthroughs, setbacks, and industry 
trends that have occurred during the past year, the reasons they are 
important, and their impact on the aerospace community are also relevant.

More information on what types of aerospace systems qualify as 
intelligent is available here: 

Aerospace America reaches 40,000 people in a broad cross section of 
disciplines. highlights should be written so that all of them are able 
to understand the content, without acronyms if possible.

The AIAA Intelligent Systems Technical Committee (ISTC) is concerned 
with the application of Intelligent System (IS) technologies and methods 
to aerospace systems, the verification and validation of these systems, 
and the education of the AIAA membership in the use of IS technologies 
in aerospace and other technical disciplines. See the Intelligent 
Systems Technical Committee website for more information on our 
technology focus: https://info.aiaa.org/tac/ISG/ISTC/default.aspx.

Previous years' print articles are available at 

This year there will be two versions: a paper article with authors' 
designated hyperlink text bolded and an online article with the provided 
URL linked. Also, with author permission, all submitted highlights (not 
just the six selected for the article) will be included on the AIAA ISTC 
website and newsletter. Requests for permission and approval of 
camera-ready versions will go out on October 1, 2014.

            /\                       \ \_____
           /  \                   ###[==_____>
          /    \                     /_/      __
         /  __  \                             \ \_____
         | (  ) |                          ###[==_____>
        /| /\/\ |\                            /_/
       / | |  | | \
      /  |=|==|=|  \       Kristin Yvonne Rozier, Ph.D.
    /    | |  | |    \       Research Computer Scientist
   / USA | ~||~ |NASA \    NASA Ames Research Center
  |______|  ~~  |______|     Phone: (650) 604-3197
         (__||__)            Fax:   (650) 604-3594
         /_\  /_\
         !!!  !!!          http://ti.arc.nasa.gov/profile/kyrozier/

Any opinions expressed in this email are my own.
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 

Mohamed yousri soliman | 13 Aug 22:12 2014

Integration from neg-infinity to pos-infinity, real functions

Dear All,

I would like to know if the following definition in HOL Light

 `real_integral {x:real| T} f `

is equivalent to   int_{\-inf}^{\inf} f(x)  dx.

Note: math formula written in latex.

hol-info mailing list
hol-info <at> lists.sourceforge.net
Jiaqi Tan | 16 Aug 01:44 2014

How to handle what looks like syntactic rewrites in subgoal


I am using the Hoare logic in examples/machine-code, and I encountered this subgoal in a proof I am working on:

val msf1111 =
   ([([``SPEC x (cond ms * p') {(offset,ins)} q``,
       ``c = {(offset,ins)}``,
       ``p = cond ms * p'``],
      ``(p * r = cond ms * p') ∧ (c = {(offset,ins)}) ∧
  SPEC x (cond ms * p') {(offset,ins)} (q * r)``)],
    fn): goal list * validation

It seems like the first and second conjuncts "(p * r = cond ms * p')" and "(c = {(offset,ins)})" in the goal term are just syntactic rewrites that can be rewritten into the third conjunct, "SPEC x (cond ms * p') {(offset,ins)} (q * r)".

I am trying to prove the goal using the SPEC_FRAME theorem (Hoare logic frame rule, "|- ∀x p c q. SPEC x p c q ⇒ ∀r. SPEC x (p * r) c (q * r)"), but I can't get the goal to match the form in SPEC_FRAME because of the first two conjuncts ("(p * r = cond ms * p')" and "(c = {(offset,ins)})") in the goal term. Is there any way to force the first two conjuncts to be rewritten into the pre- and post-conditions of the SPEC term in the goal term so that I can use the SPEC_FRAME theorem to prove the goal?

Or am I misunderstanding the meaning of the first two conjuncts ("(p * r = cond ms * p')" and "(c = {(offset,ins)})") in the goal term?

Thank you!

Jiaqi Tan

hol-info mailing list
hol-info <at> lists.sourceforge.net
Robert Künnemann | 11 Aug 10:41 2014

Matrix multiplication in HOL

Hello everyone,

I've got two questions:

1. Can anyone point me to a theory in HOL formalizing matrx multiplication?

2. I need to formalize a linear-feedback shift register. They are 
usually expressed in finite field arithmetic as a polynomial mod 2. So 
far I've only found a theory for polynomials over \mathbb{R}. Am I right 
that modelling the LSFR via wordslib is the easiest way?

Cheers, Robert


Robert Künnemann, Ph.D.
Security in Information Technology, TU Darmstadt
Mornewegstraße 30, Room 4.1.05, D64293 Darmstadt
Phone: +49 6151 16 75532

Geoff Sutcliffe | 1 Aug 13:44 2014




25th International Conference on Automated Deduction (CADE-25)
Berlin, Germany, 1-7 August 2015


Submission deadlines:

   14 November 2014 (workshops/tutorials/competitions)
16/23 February 2015 (papers)

CADE is the major international forum at which research on all aspects of
automated deduction is presented. The 25th jubilee edition will feature
a special session on the past, present, and future of automated deduction

  Ursula Martin      University of Oxford
  Frank Pfenning     Carnegie Mellon University
  David Plaisted     University of North Carolina at Chapel Hill
  Andrei Voronkov    University of Manchester

as invited speakers. In addition, there will be invited presentations by

  Ulrich Furbach     University of Koblenz
  Edward Zalta       Stanford University


Workshop proposals for CADE-25 are solicited. Both well-established
workshops and newer ones are encouraged. Similarly, proposals for workshops
with a tight focus on a core automated reasoning specialization, as well as
those with a broader, more applied focus, are very welcome.

Please provide the following information in your application document:

+ Workshop title.
+ Names and affiliations of organizers.
+ Proposed workshop duration (from half a day to two days) and preferred
+ Brief description of the goals and the scope of the workshop. Why is the
  workshop relevant for CADE?
+ Is the workshop new or has it met previously? In the latter case
  information on previous meetings should be given (e.g., links to the
  program, number of submissions, number of participants).
+ What are the plans for publication?


Tutorial proposals for CADE-25 are solicited. Tutorials are expected to be
half-day events, with a theoretical or applied focus, on a topic of interest
for CADE-25. Proposals should provide the following information:

+ Tutorial title.
+ Names and affiliations of organizers.
+ Brief description of the tutorial's goals and topics to be covered.
+ Whether or not a version of the tutorial has been given previously.

CADE will take care of printing and distributing notes for tutorials that
would like this service.


The CADE ATP System Competition (CASC), which evaluates automated theorem
proving systems for classical logics, has become an integral part of the
CADE conferences.

Further system competition proposals are solicited. The goal is to foster
the development of automated reasoning systems in all areas relevant for
automated deduction in a broader sense. Proposals should include the
following information:

+ Competition title.
+ Names and affiliations of organizers.
+ Duration and schedule of the competition.
+ Room/space requirements.
+ Description of the competition task and the evaluation procedure.
+ Is the competition new or has it been organized before?
  In the latter case information on previous competitions should be given.
+ What computing resources are required and how will they be provided?


High-quality submissions on the general topic of automated deduction,
including foundations, applications, implementations, and practical
experiences are solicited.

* Logics of interest include propositional, first-order, equational,
  higher-order, classical, description, modal, temporal, many-valued,
  constructive, other non-classical, meta-logics, logical frameworks, type
  theory, set theory, as well as any combination thereof.

* Paradigms of interest include theorem proving, model building, constraint
  solving, computer algebra, model checking, proof checking, and their

* Methods of interest include resolution, superposition, completion,
  saturation, term rewriting, decision procedures, model elimination,
  connection methods, tableaux, sequent calculi, natural deduction, as
  well as their supporting algorithms and data structures, including
  matching, unification, orderings, induction, indexing techniques, proof
  presentation and explanation, proof planning.

* Applications of interest include program analysis, verification and
  synthesis of software and hardware, formal methods, computational logic,
  computer mathematics, natural language processing, computational
  linguistics, knowledge representation, ontology reasoning, deductive
  databases, declarative programming, robotics, planning, and other areas
  of AI.

Submissions can be made in the categories regular papers and system
descriptions. The page limit in Springer LNCS style is 15 pages for regular
papers and 10 pages for system descriptions. Submissions must be unpublished
and not submitted for publication elsewhere. They will be judged on
relevance, originality, significance, correctness, and readability. System
descriptions should contain a link to a working system and will also be
judged on usefulness and design. Proofs of theoretical results that do not
fit in the page limit, executables of systems, and input data of experiments
should be made available, via a reference to a website or in an appendix of
the paper. Reviewers will be encouraged to consider this additional
material, but submissions must be self-contained within the respective page
limit; considering the additional material should not be necessary to
assess the merits of a submission. The proceedings of the conference will
be published in the Springer LNCS/LNAI series. Formatting instructions and
the LNCS style files can be obtained at 


At every CADE conference the Program Committee selects one of the
accepted papers to receive the CADE Best Paper Award. The award
recognizes a paper that the Program Committee collegially evaluates as
the best in terms of originality and significance, having substantial
confidence in its correctness. Overall technical quality,
completeness, scholarly accuracy, and readability are also
considered. Characteristics associated with a best paper include, for
instance, introduction of a strong new technique or approach, solution
of a long-standing open problem, introduction and solution of an
interesting and important new problem, highly innovative application
of known ideas or existing techniques, and presentation of a new
system of outstanding power. Under exceptional circumstances, the
Program Committee may give two awards (ex aequo) or give no award.

At CADE-25 we also intend to award the best student paper (details
will follow).


Workshop/Tutorials/System Competitions:

Submission deadline:      14 November 2014
Notification:             28 November 2014


Abstract deadline:        16 February 2015
Submission deadline:      23 February 2015
Rebuttal phase:           15-18 April 2015
Notification:             26 April 2015
Final version:            17 May 2015

Workshops and Tutorials:  1 August to 3 August (morning) 2015
Competitions:             1 to 7 August 2015
Conference:               3 August (afternoon) to 7 August 2015


Proposals for workshops, tutorials, and system competitions should be
uploaded via


Papers should be submitted via



Conference Chair:
  Christoph Benzmüller   Freie Universität Berlin

Program Committee Co-Chairs:
  Amy Felty              University of Ottawa
  Aart Middeldorp        University of Innsbruck

Workshop, Tutorial, and Competition Co-Chairs:
  Jasmin Blanchette      Technische Universität München
  Andrew Reynolds        EPFL Lausanne

Publicity and Web Chair:
  Julian Röder           Freie Universität Berlin

Program Committee
  Carlos Areces          Universidad Nacional de Córdoba
  Alessandro Armando     University of Genova
  Christoph Benzmüller   Freie Universität Berlin
  Josh Berdine           Microsoft Research
  Jasmin Blanchette      Technische Universität München
  Marta Cialdea Mayer    Universita di Roma Tre
  Stephanie Delaune      CNRS
  Gilles Dowek           Inria
  Amy Felty              University of Ottawa
  Reiner Hähnle          Technical University of Darmstadt
  Stefan Hetzl           Vienna University of Technology
  Marijn Heule           The University of Texas at Austin
  Nao Hirokawa           JAIST
  Ullrich Hustadt        University of Liverpool
  Deepak Kapur           University of New Mexico
  Gerwin Klein           NICTA and UNSW
  Laura Kovács           Chalmers University of Technology
  Carsten Lutz           Universität Bremen
  Assia Mahboubi         Inria
  Aart Middeldorp        University of Innsbruck
  Albert Oliveras        Technical University of Catalonia
  Nicolas Peltier        CNRS
  Brigitte Pientka       McGill University
  Ruzica Piskac          Yale University
  André Platzer          Carnegie Mellon University
  Andrew Reynolds        EPFL Lausanne
  Christophe Ringeissen  LORIA-INRIA
  Renate Schmidt         University of Manchester
  Stephan Schulz         DHBW Stuttgart
  Georg Struth           University of Sheffield
  Geoff Sutcliffe        University of Miami
  Alwen Tiu              Nanyang Technological University
  Freek Wiedijk          Radboud University Nijmegen

hol-info mailing list
hol-info <at> lists.sourceforge.net
Klaus Havelund | 29 Jul 06:15 2014

[fm-announcements] RV 2014: Call for Participation


RV 2014: 14th International Conference on Runtime Verification

September 22 - September 25, 2014, Toronto, Canada



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.


  • 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


  • 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


The Fields Institute for Research in Mathematical Sciences

222 College Street, Toronto, Ontario, Canada



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:



  • 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


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


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


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.
hol-info mailing list
hol-info <at> lists.sourceforge.net
Ramana Kumar | 29 Jul 11:02 2014

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.
hol-info mailing list
hol-info <at> lists.sourceforge.net
Ramana Kumar | 24 Jul 17:04 2014

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.
hol-info mailing list
hol-info <at> lists.sourceforge.net