The 3rd World Congress on Formal Methods will take place during the week of 7-11 October 2019 in Porto, Portugal. It will bring together major conferences on formal methods, including the flagship FM symposium, and many satellite workshops.

Complementing the academic program, the Industry Day targets industrial development of formal methods, and the FM Tool Exhibition will provide a forum for developers of academic or industrial tools that support the use of formal methods in different stages of system and software development.

Tool Exhibitors
  • Carnegie Mellon University
    Tool Presenters When Description
    Oct 11
    		 Self-driving cars, autonomous robots, modern airplanes, or robotic surgery: we increasingly entrust our lives to computers and therefore should strive for nothing but the highest safety standards – mathematical correctness proof. Proofs for such cyber-physical systems can be constructed with the KeYmaera X prover. As a hybrid systems and hybrid games theorem prover, KeYmaera X analyzes the control program and the physical behavior of the controlled system together. KeYmaera X implements differential dynamic logic (dL), a logic for specifying and verifying properties of hybrid systems with mixed discrete, continuous, and adversarial dynamics. KeYmaera X features a minimal core of just 1700 lines of code that isolates all soundness-critical reasoning. Such a small and simple prover core makes it much easier to trust verification results. Pre-defined and custom tactics built on top of the core drive automated proof search. KeYmaera X comes with a web-based front-end that provides a clean interface for both interactive and automated proving, highlighting the most crucial parts of a verification activity.
  • CEA List
    Tool Presenters When Description
    Oct 9
    		 Frama-C is an open-source industrial-strengh extensible and collaborative framework for code analysis of C programs. Its open-source distribution includes 28 plug-ins for analyses and program transformations of C source code possibly annotated with formal annotations written in the ACSL specification language. It notably includes the deductive verification tool WP that aims at proving functional properties, the abstract interpreter Eva that is suitable for checking the absence of undefined behaviors at compile time and the runtime verification tool E-ACSL that generates monitors in order to detect invalid ACSL annotations and undefined behaviors at runtime.
  • Checkmarx
    Tool Presenters When Description
    Oct 9
    		 CxSAST – Checkmarx CxSAST is part of the Checkmarx Software Exposure Platform addressing software security risk across the entire SDLC. CxSAST is a flexible and accurate static analysis solution used to identify hundreds of security vulnerabilities in both custom code and open source components. It is used by development, DevOps, and security teams to scan source code early in the SDLC across over 25 coding and scripting languages.
  • ClearSy
    Tool Presenters When Description
    Oct 7-11
    		 The CLEARSY Safety Platform is aimed at easing the development and the deployment of safety critical applications, up to SIL4. It relies on the smart integration of formal methods (including mathematical proof), redundant code generation and compilation, and a hardware platform that ensures a safe execution of the software.
  • FBK Trento
    Tool Presenters When Description
    Oct 11
    		 nuXmv, xSAP, and OCRA form a collection of tools developed in FBK to support various model-based design activities with formal methods: nuXmv implements state-of-the-art SAT/SMT-based algorithms for model checking and temporal logic analysis; xSAP provides functionalities for model-based safety analysis; and OCRA supports contract-based analysis of architectural models. The three tools have been used in an integrated tool chain as back-end of higher-level model-based design tools such as COMPASS and CHESS, and evaluated in various industrial case studies.
  • Microsoft Research, Inria
    Tool Presenters When Description
    Oct 10-11 (+private demos on other days on request)
    		 TLA+ is a formal specification language, mainly intended for concurrent and distributed algorithms and systems. It is supported by the TLA+ Toolbox that integrates an IDE for editing TLA+ specifications and PlusCal algorithms, the syntactic and semantic analyzer, the TLC model checker, and (optionally) the TLA+ Proof System. The model checker can be run locally on the machine that the Toolbox is running on as well as remotely on a cluster or in the cloud. The tools are mainly developed and maintained by Microsoft Research and Inria. The presentation will present the functionality of the TLA+ tools and their application to the verification of simple case studies.
  • NASA Langley Research, National Institute of Aerospace
    Tool Presenters When Description
    Oct 9-11
    		 This tool demonstration presents VSCode-PVS, a modern integrated development envi- ronment for the Prototype Verification System (PVS). The new environment integrates the editing and proof management functionalities of PVS in Visual Studio Code, a popular code editor widely used by software developers. VSCode-PVS provides functionalities that developers expect to find in modern verification tools, but are not available in the standard Emacs front-end of PVS, such as auto-completion, point-and-click navigation of definitions, live diagnostics for errors, and literate programming. The main features of VSCode-PVS will be demonstrated through a set of examples based on publicly available specifications developed by NASA.
  • Newcastle University, SYSTRA UK
    Tool Presenters When Description
    Oct 9-11
    		 SafeCap is a platform for applying static formal verification to railway signalling. In cooperation with Siemens Rail Automation UK we have developed a industrial strength extension for processing and verifying UK standard of control tables. Separately, in cooperation with Systra UK, we have developed an extension for translation of signalling computer software into symbolic transition systems and verification of safety principles via inductive safety invariant. In the demo we shall demonstrate the generic part of the tool with the applications to verification of synthetic data sets and transition systems, further we shall demonstrate the functionality of control tables and signalling data verification. We shall also present and offer to share a number of public domain railway case studies comprising node/edge layout models, control tables and signalling data
  • Prover
    Tool Presenters When Description
    Oct 11
    		 Prover SL CE (PSL) is a state-of-the-art SAT-based model-checker, and the result of Prover’s 30-year-long experience in applying formal verification in industry. PSL is used around the world on large industrial models to certify the safety of mission-critical systems, especially in the railway domain. Our newest multi-core support (Turbo-Threads) allows PSL to handle even larger systems and provides impressive speed-ups. Recently, we have added support for IEEE754 floating point. We are also working on using artificial intelligence techniques to adapt PSL’s search strategy to specific problems, and we have already obtained significant performance gains that add up to what is delivered by turbo-threading.
    Prover Certifier is a product built on top of PSL, based on diversification and equivalence-checking, that can produce complete safety evidence for CENELEC EN50128 SIL 4 certification using formal verification. Prover Certifier has seen many successful applications around the world; it can be used as a standalone solution or linked to our interlocking design automation solution, Prover Trident
    The main input to both PSL and Prover Certifier is an HLL model. HLL is itself a declarative, stream-based language, suitable for modeling and expressing temporal properties of discrete-time sequential systems. HLL is soon to become an open industry standard. Using one of our many translators, you can automatically translate computer programs or relay systems to HLL in order to investigate and prove them mathematically.
  • Univ. Düsseldorf
    Tool Presenters When Description
    Oct 11
    		 The ProB animator, constraint solver and model checker: ProB is an animator, constraint solver and model checker for the B-Method It allows fully automatic animation of B specifications, and can be used to systematically check a specification for a wide range of errors. The constraint-solving capabilities of ProB can also be used for model finding, deadlock checking and test-case generation. In this tool exhibition we focus on recent developments of ProB: – the ProB Jupyter kernel for interactive notebooks for documentation; – the new Java FX user interface, along with new visualization techniques (e.g., based on SVG graphics); – a summary of new features in the ProB kernel (regular expressions, memoization, …) and the model checking backend (use of LTSmin, …); – a summary of recent industrial applications and T2 tool qualifications.
  • Univ. of Genoa, Univ. of Sassari
    Tool Presenters When Description
    Oct 10-11
    		 In the context of safety- and security-critical Cyber-Physical Systems (CPSs), checking the sanity of functional requirements is an important, yet challenging task. It is largely recognized that a flaw in the requirements specification can lead to delays, additional expenses and, possibly, the failure of the project. Nonetheless, due to the intrinsic difficulty of dealing with natural language sentences, requirements are often checked manually, an error-prone and time-consuming activity. Given the increasing demand and complexity of CPSs, and the need to reduce time-to-market and costs, practical solutions to enable automated verification of requirements are in order. Formal methods provides a viable solution, but they often requires overburdening formalization and a high degree of expertise. As a trade-off between formalization and usability, a recurrent solution in the literature is the use of Property Specification Patterns (PSPs), English-like structured natural sentences that provides a direct mapping to one or more logics. ReqV is a tool developed in the context of the H2020 EU CERBERO project that leverage on PSPs to tackle the problem stated before. We extended PSPs by considering Boolean as well as atomic numerical assertions of the form x =∗ c, where X is a variable of the system, c ∈ R is a constant real number and the operator =∗∈ {<, <=, =, >=, >} have the usual interpretation. Furthemore, we presented an encoding to reduce the inner consistency of extended PSPs, i.e., logical errors in the specification that prevents any possible system to satisfy all requirements, to the Linear Temporal Logic (LTL) satisfiability problem. We also extended the previous work with a new algorithm to find a minimum set of conflicting requirements in case of inconsistency, and we collected all these functionalities in a Java library called SpecPro4. ReqV exploits these capabilities to provide an easy-to-use interface for the verification of requirements. Its goal is to enable users with no background knowledge of formal methods and logical languages to write requirements in PSP forms and check their consistency. ReqV also aims at minimizing the setup process for the user, and therefore it is developed as a web application that can easily be accessed with a browser.
  • Univ. of Oslo
    Tool Presenters When Description
    Oct 9-11
    		 RailCons is a research project that has been running for 4 years and will end in August 2019. This project was funded partially the Norwegian Research Council and by the company Railcomplete, where one PhD student was hired to do research on “Automated Methods and Tools for Ensuring Consistency of Railway Designs”. There have been produced five related tools/prototypes, three of these have been already presented at iFM, SEFM, FMCAD (with two Best Paper Awards), the forth one will be presented at FM’19, and the fifth is being submitted to iFM’19. More info exists on the project’s webpage (including videos, posters, papers, slides).
  • Uppsala University, Aalborg University
    Tool Presenters When Description
    Oct 10-11
    		 Uppaal is a suite of tools for formal verification, model-based testing, performance analysis and synthesis of real-time systems. The suite originates from academic papers and experiments, it has become popular in teaching and found its way into a number of industrial applications, such as communication protocols, embedded systems, consumer electronics and automotive designs. At the core the tools use extended timed automata specification as a model to simulate, validate, verify properties, find optimal solutions, interactively visualize the behavior and diagnostic traces, generate test cases in native programming languages, estimate time and cost of operation, and find and optimize control strategies for steering the system in adverse environments. The demonstration shows the principles behind the tools and some instances of specific applications.

Call for Tools

The tool exhibition will be located in a central lobby of the main conference building, facilitating informal exchanges with conference participants. Tools can be exhibited during all or part of the week, with a particular focus on the industry day on October 11. Exhibitors are requested to provide their hardware equipment and to ensure the presence of at least one person at their stands during the days they choose to exhibit their tool.

Financial conditions
  • Academic tool developers: free with registration of the exhibitors.
  • Industrial tool developers: included with sponsorship of FM’19 World Congress and registration of the exhibitors (basic sponsoring starts at €500, higher levels of sponsoring include registrations of participants).
Submisson

In order to submit a proposal for a tool to be exhibited, please send a title, short description, and URL describing the tool(s) by June 30, 2019, to the Tool Exhibition Chairs:

Informal enquiries are welcome.