Apr 052018

VORTEX 2018, ECOOP and ISSTA, Amsterdam, July 16-21, 2018


Runtime verification (RV) is an approach to software verification concerned with monitoring and analysis of software and hardware under execution. Recently, RV has gained more traction as an effective and promising approach to ensure software reliability, bridging a gap between formal verification and conventional testing; monitoring a system at runtime offers additional opportunities for addressing error recovery, self-adaptation, and other issues that go beyond software reliability. The goal of VORTEX is to bring together researchers working on runtime verification for topics covering either theoretical, or practical aspects, or, preferably, both, with emphasis on object-oriented languages, and systems.

Topics of interest include, but are not limited to, the following ones:

* behavioural types for RV
* combination of static and dynamic analyses
* industrial applications
* language support for RV
* monitor construction and synthesis techniques
* monitoring concurrent/distributed systems
* monitoring oriented programming
* program adaptation
* runtime enforcement, fault detection, recovery and repair
* RV for safety and security
* RV for the Internet of Things
* specification formalisms and formal underpinning of RV
* specification mining
* tool development

Contributions will be formally reviewed by at least three reviewers, and selection will be based on originality, relevance, technical accuracy, and the potential to generate interesting discussions.

Important Dates

Paper submission: May 16, 2018 23:59 AoE (UTC-12h)
Notification: June 14, 2018

Submission Instructions

Submissions must be unpublished work, in English, formatted in PDF with acmart sigplan style (http://www.sigplan.org/Resources/Author), and are allowed to be position papers or surveys (max 6 pages), short papers (max 3 pages) presenting preliminary ongoing scientific work, or long papers (max 6 pages) providing more consolidated research contributions.

Papers must be submitted electronically via EasyChair at
https://easychair.org/conferences/?conf=vortex2018 .

Proceedings and Special Issue

Accepted papers will, upon agreement by the authors, be published in the ACM Digital Library. Depending on the quality of submissions, authors of selected papers will be invited after the workshop to submit an extended version for a special issue hosted by a prime journal in the field.

Program Committee

– Davide Ancona, University of Genova, Italy (co-chair)
– Gordon Pace, University of Malta, Malta (co-chair)

– Wolfgang Ahrendt, Chalmers University of Technology, Sweden
– Cyrille Artho, KTH Royal Institute of Technology, Sweden
– Ezio Bartocci, Technische Universität Wien, Austria
– Borzoo Bonakdarpour, Iowa State University, USA
– Ylies Falcone, Univ. Grenoble Alpes, Inria, France
– Klaus Havelund, NASA/Caltech Jet Propulsion Laboratory, USA
– Reiner Hahnle, Technical University of Darmstadt, Germany
– Jean-Baptiste Jeannin, Carnegie Mellon University, USA
– Martin Leucker, University of Lubeck, Germany
– Rumyana Neykova, Imperial College London, UK
– Luca Padovani, University of Turin, Italy
– Antonio Ravara, New University of Lisbon, Portugal
– Giles Reger, University of Manchester, UK
– Gerardo Schneider, University of Gothenburg, Sweden
– Volker Stolz, Hogskulen pa Vestlandet, Norway
– Cesar Sanchez, IMDEA Software Institute, Spain
– Frank S. de Boer, Centrum Wiskunde & Informatica, Leiden University, Netherlands
– Oleg Sokolsky, University of Pennsylvania, USA

Oct 252017

I’m at ISSRE 2017 in Toulouse, France, for the presentation of our paper on Interactive Runtime Verification and attending the talks of the day.

Our paper on Interactive Runtime Verification (i-RV) can be downloaded here.

Verde, our open-source tool for i-RV, can be retrieved and experimented with our interactive tutorial by following this link. Our interactive tutorial illustrates how i-RV can be used to more effectively debug C programs leveraging runtime verification.

Jul 232017


Topic E3: Model-based Design and Verification for Embedded Systems

at DATE 2018,
Dresden, GE
March 19 – 23, 2018

DATE 2018, will take place from 19 to 23 March, 2018, at the International Congress Center in Dresden, Germany.

The conference addresses all aspects of research into technologies for electronic and embedded systems engineering. An important part of the conference  is devoted to modeling, analysis, design and deployment of embedded software.

We invite you to submit papers to Topic E3: Model-based Design and Verification for Embedded Systems.

Main topics of interest:

Verification techniques for embedded and cyber-physical systems ranging from simulation, testing, model-checking, SAT and SMT-based reasoning, compositional analysis and analytical methods. Modeling, analysis and optimization of non-functional and performance aspects such as timing, memory usage, QoS and reliability. Model-based design of software architectures and deployment. Theories, languages and tools supporting model-based design flows covering software, control and physical components. Monitoring and run-time verification of embedded systems.

Topic Chair: Petru Eles, Linköping University, SE
Topic Co-Chair: Borzoo Bonakdarpour, University of Waterloo, CA,

Topic Subcommittee Members:

  • Sudipta Chattopadhyay, Singapore University of Technology and Design (SUTD), SG
  • Ylies Falcone, University Grenoble Alpes, FR
  • Florence Maraninchi, Verimag, FR
  • Kristin Rozier, Iowa State University, US
  • Lothar Thiele, ETH Zurich, CH

Please note:

May 202017


 26th ACM SIGSOFT International Symposium on Software Testing and Analysis


 24th International SPIN Symposium on Model Checking of Software


 July 10-14, 2017, Santa Barbara, California, USA

ISSTA is the leading research symposium on software testing and analysis, bringing together academics, industrial researchers, and practitioners to exchange new ideas, problems, and experiences on how to analyze and test software systems.
The SPIN symposium brings together researchers and practitioners interested in automated, tool-based techniques to analyze software systems and models of software systems for verification and validation purposes.
  *** VENUE ***

University of California, Santa Barbara (www.ucsb.edu)


Registration is open! Early registration until June 9.



ISSTA list of accepted papers:

SPIN list of accepted papers:

    Christopher Kruegel, UCSB
    Armando Solar-Lezama, MIT
    Domagoj Babic, Google
    Byron Cook, Amazon Web Services
    Gerard Holzmann, Nimble Research

ISSTA Doctoral Symposium


ISSTA Demonstrations track


TECPS 2017: Workshop on Testing Embedded and Cyber-Physical Systems


RERS Challenge 2017: Rigorous Examination of Reactive Systems


Dec 122016

SPIN 2017

24th International Symposium on Model Checking of Software

Santa Barbara, CA, USA, July 13-14, 2017


Collocated with ISSTA

The SPIN symposium aims at bringing together researchers and practitioners interested in automated tool-based techniques for the analysis of software as well as models of software, for the purpose of verification and validation. The symposium specifically focuses on concurrent software, but does not exclude analysis of sequential software. Submissions are solicited on theoretical results, novel algorithms, tool development, empirical evaluation, and education.

History: The SPIN symposium originated as a workshop focusing on explicit state model checking, specifically as related to the Spin model checker. However, over the years it has evolved to a broadly scoped symposium for software analysis using any automated techniques, including model checking, automated theorem proving, and symbolic execution.

SPIN 2017 will be organized as an ACM SIGSOFT event, collocated with the International Symposium on Software Testing and Analysis (ISSTA 2017): http://conf.researchr.org/home/issta-2017. In addition there will be a one-day Rigorous Examination of Reactive Systems verification challenge Workshop (RERS 2017): http://www.rers-challenge.org/2017. An overview of the previous SPIN symposia (and early workshops) can be found at: http://spinroot.com/spin/symposia.

Topics of interest include, but are not limited to:

  • Formal verification techniques for automated analysis of software
  • Formal analysis for modeling languages, such as UML/state charts
  • Formal specification languages, temporal logic, design-by-contract
  • Model checking
  • Automated theorem proving, including SAT and SMT
  • Verifying compilers
  • Abstraction and symbolic execution techniques
  • Static analysis and abstract interpretation
  • Combination of verification techniques
  • Modular and compositional verification techniques
  • Verification of timed and probabilistic systems
  • Automated testing using advanced analysis techniques
  • Combination of static and dynamic analyses
  • Derivation of specifications, test cases, or other useful material via formal analysis
  • Case studies of interesting systems or with interesting results
  • Engineering and implementation of software verification and analysis tools
  • Benchmark and comparative studies for formal verification and analysis tools
  • Formal methods education and training
  • Insightful surveys or historical accounts on topics of relevance to the symposium

Submission Guidelines

The contributions to SPIN 2017 will be published as ACM Proceedings, and should be submitted in the ACM Conference Format: https://www.acm.org/publications/proceedings-template.

With the exception of survey and history papers, submissions must be original and should not have been published previously or be under consideration for publication while being evaluated for this symposium.

We are soliciting two categories of papers:

  • Full Research Papers describing fully developed work and complete results (10 pages);
  • Short Papers presenting tools, technology, experiences with lessons learned, new ideas, work in progress with preliminary results, and novel contributions to formal methods education (4 pages).

Papers should be submitted via the EasyChair SPIN 2017 submission website: https://easychair.org/conferences/?conf=spin2017.

Best Paper awards will be given and announced at the conference.

A selection of papers will be invited to a special issue of the International Journal on Software Tools for Technology Transfer (STTT).

Important Dates

  • Paper Submission: February 10, 2017 (23:59:59 Anywhere on Earth)
  • Author Notification : April 15, 2017
  • Camera-Ready Paper: May 20, 2017
  • Symposium : July 13-14, 2017


  • Hakan Erdogmus, Program Co-Chair, Carnegie Mellon University, USA
  • Klaus Havelund, Program Co-Chair, NASA/Caltech Jet Propulsion Laboratory, USA
  • Corina Pasareanu, Awards Chair, NASA Ames Research Center, USA
  • Yliès Falcone, Publicity Chair, Univ. Grenoble Alpes, Inria, France

Program Committee

  • Erika Abraham, RWTH Aachen University, Germany
  • Christel Baier, Technical University of Dresden, Germany
  • Tom Ball, Microsoft Research, USA
  • Ezio Bartocci, Vienna University of Technology, Austria
  • Dirk Beyer, Ludwig-Maximilians-Universität München (LMU Munich), Germany
  • Armin Biere, Johannes Kepler University, Austria
  • Dragan Bosnacki, Eindhoven University of Technology, Netherlands
  • Zmago Brezocnik, University of Maribor, Slovenia
  • Sagar Chaki, Software Engineering Institute CMU, USA
  • Alessandro Cimatti, Fondazione Bruno Kessler, Italy
  • Lucas Cordeiro, University of Oxford, UK
  • Patrice Godefroid, Microsoft Research, USA
  • Susanne Graf, VERIMAG Laboratory, France
  • Radu Grosu, Vienna University of Technology, Austria
  • Arie Gurfinkel, University of Waterloo, USA
  • Gerard Holzmann, NASA/Caltech Jet Propulsion Laboratory, USA
  • Sarfraz Khurshid, The University of Texas at Austin, USA
  • Kim Larsen, Aalborg University, Denmark
  • Stefan Leue, University of Konstanz, Germany
  • Alice Miller, University of Glasgow, Scotland
  • Corina Pasareanu, NASA Ames Research Center, USA
  • Doron Peled, Bar Ilan University, Israel
  • Neha Rungta, NASA Ames Research Center, USA
  • Theo Ruys, RUwise, Netherlands
  • Scott Smolka, Stony Brook University, USA
  • Scott Stoller, Stony Brook University, United States
  • Jun Sun, Singapore University of Technology and Design, Singapore
  • Oksana Tkachuk, NASA Ames Research Center, USA
  • Stavros Tripakis, University of California, Berkeley, USA
  • Willem Visser, Stellenbosch University, South Africa
  • Farn Wang, National Taiwan University, Taiwan
  • Michael Whalen, University of Minnesota, USA
  • Anton Wijs, Eindhoven University of Technology, Netherlands

Steering Committee

  • Dragan Bosnacki, Eindhoven University of Technology, Netherlands
  • Susanne Graf, Verimag, France
  • Gerard Holzmann, NASA/Caltech Jet Propulsion Laboratory, United States
  • Stefan Leue, University of Konstanz, Germany
  • Willem Visser, Stellenbosch University, South Africa
Nov 292016

SAC-SVT 2017

Software Verification and Testing 2017
A Track of the ACM Symposium on Applied Computing

Marrakech, Morocco, April 3 – 7, 2017



For the past thirsty years, the ACM Symposium on Applied Computing has been a primary gathering forum for applied computer scientists, computer engineers, software engineers, and application developers from around the world. SAC 2017 is sponsored by the ACM Special Interest Group on Applied Computing (SIGAPP), and will be hosted by the University of Quebec (Montreal, Canada), University Cadi Ayyad (Marrakech, Morocco), Mohamed V University of Rabat – Mohammadia School Of Engineers (Rabat, Morocco) and National School of Applied Sciences (Kenitra, Morocco).
Symposium on Applied Computing been a primary gathering forum for applied computer scientists, computer engineers, software engineers, and application developers from around the world over the past thirty years.
The Software Verification and Testing track aims at contributing to the challenge of improving the usability of formal methods in software engineering. The track covers areas such as formal methods for verification and testing, based on theorem proving, model checking, static analysis, and run-time verification. These areas include a broad range of topics, 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

Registration Information

Please note the following important dates regarding registration.

Author Registration

Friday, December 16, 2016

Early Registration

Friday, February 3, 2017


1 day during April 3 – 7, 2017


For authors. 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.

Accepted Papers

The following papers were accepted by the SAC-SVT 2017 Programme Committee.

  • Mohamed Amine Aouadhi, Benoît Delahaye and Arnaud Lanoix.
    Moving from Event-B to Probabilistic Event-B
  • Huu-Vu Nguyen and Tayssir Touili.
    CARET Model Checking For Pushdown Systems
  • Rudolf Ramler, Thomas Wetzlmaier and Claus Klammer.
    An Empirical Study on the Application of Mutation Testing for a Safety-Critical Industrial Software System 
  • Thibaud Antignac, Mukelabai Mukelabai and Gerardo Schneider.
    Specification, Design and Verification of an Accountability-Aware Surveillance Protocol
  • Davide Basile, Felicita Di Giandomenico and Stefania Gnesi.
    Statistical Model Checking of an Energy-Saving Cyber-Physical System in the Railway Domain
  • Jeongho Kim and Eunseok Lee.
    History-based Test Case Prioritization for Failure Information
  • Yunus Kiliç and Hasan Sözer.
    Generating Runtime Verification Specifications based on Static Code Analysis Alerts
  • Pedro Delgado-Pérez, Inmaculada Medina-Bulo, Sergio Segura, Antonio García-Domínguez and Juan José Domínguez-Jiménez.
    GiGAn: Evolutionary Mutation Testing for C++ Object-Oriented Systems
  • András Márki and Birgitta Lindström.
    Mutation Tools for Java

Venue and Travel Information

Information about the venue and how to travel to Marrakesh is available on SAC 2017 Website at: