{"id":2101,"date":"2019-05-23T11:07:10","date_gmt":"2019-05-23T11:07:10","guid":{"rendered":"http:\/\/formalmethods2019.inesctec.pt\/?page_id=2101"},"modified":"2020-10-09T10:42:52","modified_gmt":"2020-10-09T10:42:52","slug":"fm19-tool-exhibition","status":"publish","type":"page","link":"http:\/\/formalmethods2019.inesctec.pt\/fm19-tool-exhibition\/","title":{"rendered":"FM&#8217;19 Tool Exhibition"},"content":{"rendered":"<p><a href=\"http:\/\/www.fmeurope.org\/\"><img loading=\"lazy\" class=\"alignright wp-image-560\" src=\"http:\/\/formalmethods2019.inesctec.pt\/wp-content\/uploads\/2018\/07\/fme.png\" alt=\"\" width=\"97\" height=\"108\"><\/a> The <a href=\"http:\/\/formalmethods2019.inesctec.pt\/\">3rd World Congress on Formal Methods<\/a> will take place during the week of <strong>7-11 October 2019<\/strong> in <strong>Porto<\/strong>, Portugal. It will bring together major conferences on formal methods, including the flagship <a href=\"http:\/\/formalmethods2019.inesctec.pt\/?page_id=565\">FM symposium<\/a>, and many satellite workshops.<\/p>\n<p>Complementing the academic program, the <a href=\"http:\/\/formalmethods2019.inesctec.pt\/?page_id=353\">Industry Day<\/a> targets industrial development of formal methods, and the <strong>FM Tool Exhibition<\/strong> will provide a forum for developers of academic or industrial <strong>tools<\/strong> that support the use of formal methods in different stages of system and software development.<\/p>\n<h6>Tool Exhibitors<\/h6>\n<ul>\n<li>\n<div style=\"font-variant: small-caps;\">Carnegie Mellon University<\/div>\n<div style=\"margin-bottom: 1em;\"><\/div>\n<table data-toggle=\"table\" border=\"1\" align=\"center\">\n<tbody>\n<tr>\n<td><strong>Tool<\/strong><\/td>\n<td><strong>Presenters<\/strong><\/td>\n<td><strong>When<\/strong><\/td>\n<td><strong>Description<\/strong><\/td>\n<\/tr>\n<tr>\n<td>\n<div style=\"width: 8em; text-align: center;\"><strong><a href=\"www.keymaerax.org\" target=\"_blank\" rel=\"noopener noreferrer\">KeYmaera X<\/a><\/strong><\/div>\n<\/td>\n<td>\n<div style=\"width: 12em; text-align: center;\"><a href=\"http:\/\/www.cs.cmu.edu\/~smitsch\/\" target=\"_blank\" rel=\"noopener noreferrer\">Stefan Mitsch<\/a><\/div>\n<\/td>\n<td>\n<div style=\"width: 5em; text-align: center;\">Oct 11<\/div>\n<\/td>\n<td><span style=\"font-size: 80%;\">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 &#8211; 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.<\/span><\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<div style=\"margin-bottom: 1em;\"><\/div>\n<\/li>\n<li>\n<div style=\"font-variant: small-caps;\">CEA List<\/div>\n<div style=\"margin-bottom: 1em;\"><\/div>\n<table data-toggle=\"table\" border=\"1\" align=\"center\">\n<tbody>\n<tr>\n<td><strong>Tool<\/strong><\/td>\n<td><strong>Presenters<\/strong><\/td>\n<td><strong>When<\/strong><\/td>\n<td><strong>Description<\/strong><\/td>\n<\/tr>\n<tr>\n<td>\n<div style=\"width: 8em; text-align: center;\"><strong><a href=\"http:\/\/www.frama-c.com\/\" target=\"_blank\" rel=\"noopener noreferrer\">Frama-C<\/a><\/strong><\/div>\n<\/td>\n<td>\n<div style=\"width: 12em; text-align: center;\"><a href=\"https:\/\/allan-blanchard.fr\/\" target=\"_blank\" rel=\"noopener noreferrer\">Allan Blanchard<\/a>, <a href=\"https:\/\/www.researchgate.net\/profile\/Virgile_Prevosto\" target=\"_blank\" rel=\"noopener noreferrer\">Virgile Prevosto<\/a>, <a href=\"http:\/\/julien.signoles.free.fr\/\" target=\"_blank\" rel=\"noopener noreferrer\">Julien Signoles<\/a><\/div>\n<\/td>\n<td>\n<div style=\"width: 5em; text-align: center;\">Oct 9<\/div>\n<\/td>\n<td><span style=\"font-size: 80%;\">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.<\/span><\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<div style=\"margin-bottom: 1em;\"><\/div>\n<\/li>\n<li>\n<div style=\"font-variant: small-caps;\">Checkmarx<\/div>\n<div style=\"margin-bottom: 1em;\"><\/div>\n<table data-toggle=\"table\" border=\"1\" align=\"center\">\n<tbody>\n<tr>\n<td><strong>Tool<\/strong><\/td>\n<td><strong>Presenters<\/strong><\/td>\n<td><strong>When<\/strong><\/td>\n<td><strong>Description<\/strong><\/td>\n<\/tr>\n<tr>\n<td>\n<div style=\"width: 8em; text-align: center;\"><strong><a href=\"https:\/\/www.checkmarx.com\/technology\/static-code-analysis-sca\/\" target=\"_blank\" rel=\"noopener noreferrer\">CxSAST<\/a><\/strong><\/div>\n<\/td>\n<td>\n<div style=\"width: 12em; text-align: center;\"><a href=\"https:\/\/www.linkedin.com\/in\/nuno-oliveira-7b44799\/?locale=zh_CN\" target=\"_blank\" rel=\"noopener noreferrer\">Nuno Oliveira<\/a><\/div>\n<\/td>\n<td>\n<div style=\"width: 5em; text-align: center;\">Oct 9<\/div>\n<\/td>\n<td><span style=\"font-size: 80%;\">CxSAST &#8211; 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.<\/span><\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<div style=\"margin-bottom: 1em;\"><\/div>\n<\/li>\n<li>\n<div style=\"font-variant: small-caps;\">ClearSy<\/div>\n<div style=\"margin-bottom: 1em;\"><\/div>\n<table data-toggle=\"table\" border=\"1\" align=\"center\">\n<tbody>\n<tr>\n<td><strong>Tool<\/strong><\/td>\n<td><strong>Presenters<\/strong><\/td>\n<td><strong>When<\/strong><\/td>\n<td><strong>Description<\/strong><\/td>\n<\/tr>\n<tr>\n<td>\n<div style=\"width: 8em; text-align: center;\"><strong><a href=\"https:\/\/www.clearsy.com\/en\/our-tools\/clearsy-safety-platform\/\" target=\"_blank\" rel=\"noopener noreferrer\">Atelier B \/ Clearsy Safety Platform<\/a><\/strong><\/div>\n<\/td>\n<td>\n<div style=\"width: 12em; text-align: center;\"><a href=\"https:\/\/www.researchgate.net\/profile\/Etienne_Prun\" target=\"_blank\" rel=\"noopener noreferrer\">Etienne Prun<\/a>, <a href=\"https:\/\/www.clearsy.com\/en\/our-tools\/clearsy-safety-platform\/\" target=\"_blank\" rel=\"noopener noreferrer\">David Deharbe<\/a><\/div>\n<\/td>\n<td>\n<div style=\"width: 5em; text-align: center;\">Oct 7-11<\/div>\n<\/td>\n<td><span style=\"font-size: 80%;\">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.<\/span><\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<div style=\"margin-bottom: 1em;\"><\/div>\n<\/li>\n<li>\n<div style=\"font-variant: small-caps;\">FBK Trento<\/div>\n<div style=\"margin-bottom: 1em;\"><\/div>\n<table data-toggle=\"table\" border=\"1\" align=\"center\">\n<tbody>\n<tr>\n<td><strong>Tool<\/strong><\/td>\n<td><strong>Presenters<\/strong><\/td>\n<td><strong>When<\/strong><\/td>\n<td><strong>Description<\/strong><\/td>\n<\/tr>\n<tr>\n<td>\n<div style=\"width: 8em; text-align: center;\"><strong><a href=\"https:\/\/es.fbk.eu\/tools\/nuxmv\" target=\"_blank\" rel=\"noopener noreferrer\">nuXmv<\/a><\/strong>, <strong><a href=\"https:\/\/es.fbk.eu\/tools\/xsap\" target=\"_blank\" rel=\"noopener noreferrer\">xSAP<\/a><\/strong>, <strong><a href=\"https:\/\/es.fbk.eu\/tools\/ocra\" target=\"_blank\" rel=\"noopener noreferrer\">OCRA<\/a><\/strong><\/div>\n<\/td>\n<td>\n<div style=\"width: 12em; text-align: center;\"><a href=\"https:\/\/es-static.fbk.eu\/people\/tonetta\/\" target=\"_blank\" rel=\"noopener noreferrer\">Stefano Tonetta<\/a><\/div>\n<\/td>\n<td>\n<div style=\"width: 5em; text-align: center;\">Oct 11<\/div>\n<\/td>\n<td><span style=\"font-size: 80%;\">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.<\/span><\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<div style=\"margin-bottom: 1em;\"><\/div>\n<\/li>\n<li>\n<div style=\"font-variant: small-caps;\">Microsoft Research, Inria<\/div>\n<div style=\"margin-bottom: 1em;\"><\/div>\n<table data-toggle=\"table\" border=\"1\" align=\"center\">\n<tbody>\n<tr>\n<td><strong>Tool<\/strong><\/td>\n<td><strong>Presenters<\/strong><\/td>\n<td><strong>When<\/strong><\/td>\n<td><strong>Description<\/strong><\/td>\n<\/tr>\n<tr>\n<td>\n<div style=\"width: 8em; text-align: center;\"><strong><a href=\"https:\/\/lamport.azurewebsites.net\/tla\/tools.html\" target=\"_blank\" rel=\"noopener noreferrer\">TLA+ Tools<\/a><\/strong><\/div>\n<\/td>\n<td>\n<div style=\"width: 12em; text-align: center;\"><a href=\"https:\/\/www.linkedin.com\/in\/markus-kuppe-643559180\/\" target=\"_blank\" rel=\"noopener noreferrer\">Markus Kuppe<\/a>, <a href=\"https:\/\/members.loria.fr\/SMerz\/\" target=\"_blank\" rel=\"noopener noreferrer\">Stephan Merz<\/a><\/div>\n<\/td>\n<td>\n<div style=\"width: 5em; text-align: center;\">Oct 10-11 (+private demos on other days on request)<\/div>\n<\/td>\n<td><span style=\"font-size: 80%;\">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.<\/span><\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<div style=\"margin-bottom: 1em;\"><\/div>\n<\/li>\n<li>\n<div style=\"font-variant: small-caps;\">NASA Langley Research, National Institute of Aerospace<\/div>\n<div style=\"margin-bottom: 1em;\"><\/div>\n<table data-toggle=\"table\" border=\"1\" align=\"center\">\n<tbody>\n<tr>\n<td><strong>Tool<\/strong><\/td>\n<td><strong>Presenters<\/strong><\/td>\n<td><strong>When<\/strong><\/td>\n<td><strong>Description<\/strong><\/td>\n<\/tr>\n<tr>\n<td>\n<div style=\"width: 8em; text-align: center;\"><strong><a href=\"https:\/\/shemesh.larc.nasa.gov\/fm\/VSCode-PVS\" target=\"_blank\" rel=\"noopener noreferrer\">VSCode-PVS<\/a><\/strong><\/div>\n<\/td>\n<td>\n<div style=\"width: 12em; text-align: center;\"><a href=\"https:\/\/www.nianet.org\/directory\/research-staff\/paolo-masci\/\" target=\"_blank\" rel=\"noopener noreferrer\">Paolo Masci<\/a>, <a href=\"http:\/\/shemesh.larc.nasa.gov\/people\/cam\" target=\"_blank\" rel=\"noopener noreferrer\">C\u00e9sar Mu\u00f1oz<\/a><\/div>\n<\/td>\n<td>\n<div style=\"width: 5em; text-align: center;\">Oct 9-11<\/div>\n<\/td>\n<td><span style=\"font-size: 80%;\">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.<\/span><\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<div style=\"margin-bottom: 1em;\"><\/div>\n<\/li>\n<li>\n<div style=\"font-variant: small-caps;\">Newcastle University, SYSTRA UK<\/div>\n<div style=\"margin-bottom: 1em;\"><\/div>\n<table data-toggle=\"table\" border=\"1\" align=\"center\">\n<tbody>\n<tr>\n<td><strong>Tool<\/strong><\/td>\n<td><strong>Presenters<\/strong><\/td>\n<td><strong>When<\/strong><\/td>\n<td><strong>Description<\/strong><\/td>\n<\/tr>\n<tr>\n<td>\n<div style=\"width: 8em; text-align: center;\"><strong><a href=\"https:\/\/safecap.co.uk\/\" target=\"_blank\" rel=\"noopener noreferrer\">SafeCap<\/a><\/strong><\/div>\n<\/td>\n<td>\n<div style=\"width: 12em; text-align: center;\"><a href=\"https:\/\/safecap.co.uk\/?page_id=24\" target=\"_blank\" rel=\"noopener noreferrer\">Paulius Stankaitis<\/a>, <a href=\"https:\/\/www.ncl.ac.uk\/computing\/people\/profile\/alexeiiliasov.html\" target=\"_blank\" rel=\"noopener noreferrer\">Alexei Iliasov<\/a><\/div>\n<\/td>\n<td>\n<div style=\"width: 5em; text-align: center;\">Oct 9-11<\/div>\n<\/td>\n<td><span style=\"font-size: 80%;\">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<\/span><\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<div style=\"margin-bottom: 1em;\"><\/div>\n<\/li>\n<li>\n<div style=\"font-variant: small-caps;\">Prover<\/div>\n<div style=\"margin-bottom: 1em;\"><\/div>\n<table data-toggle=\"table\" border=\"1\" align=\"center\">\n<tbody>\n<tr>\n<td><strong>Tool<\/strong><\/td>\n<td><strong>Presenters<\/strong><\/td>\n<td><strong>When<\/strong><\/td>\n<td><strong>Description<\/strong><\/td>\n<\/tr>\n<tr>\n<td>\n<div style=\"width: 8em; text-align: center;\"><strong><a href=\"https:\/\/www.prover.com\/software-solutions-rail-control\/psl-prover-sl-ce\/\" target=\"_blank\" rel=\"noopener noreferrer\">PSL<\/a><\/strong>, <strong><a href=\"https:\/\/www.prover.com\/software-solutions-rail-control\/prover-certifier\/\" target=\"_blank\" rel=\"noopener noreferrer\">Prover Certifier<\/a><\/strong>, <strong><a href=\"https:\/\/www.prover.com\/software-solutions-rail-control\/hll-high-level-language\/\" target=\"_blank\" rel=\"noopener noreferrer\">HLL<\/a><\/strong><\/div>\n<\/td>\n<td>\n<div style=\"width: 12em; text-align: center;\"><a href=\"https:\/\/www.linkedin.com\/in\/lars-helander-7602785a\/\" target=\"_blank\" rel=\"noopener noreferrer\">Lars Helander<\/a>, <a href=\"https:\/\/www.linkedin.com\/in\/iagoabal\/\" target=\"_blank\" rel=\"noopener noreferrer\">Iago Abal<\/a><\/div>\n<\/td>\n<td>\n<div style=\"width: 5em; text-align: center;\">Oct 11<\/div>\n<\/td>\n<td><span style=\"font-size: 80%;\">Prover SL CE (PSL) is a state-of-the-art SAT-based model-checker, and the result of Prover&#8217;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&#8217;s search strategy to specific problems, and we have already obtained significant performance gains that add up to what is delivered by turbo-threading.<br \/>\nProver 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<br \/>\nThe 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.<\/span><\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<div style=\"margin-bottom: 1em;\"><\/div>\n<\/li>\n<li>\n<div style=\"font-variant: small-caps;\">Univ. D\u00fcsseldorf<\/div>\n<div style=\"margin-bottom: 1em;\"><\/div>\n<table data-toggle=\"table\" border=\"1\" align=\"center\">\n<tbody>\n<tr>\n<td><strong>Tool<\/strong><\/td>\n<td><strong>Presenters<\/strong><\/td>\n<td><strong>When<\/strong><\/td>\n<td><strong>Description<\/strong><\/td>\n<\/tr>\n<tr>\n<td>\n<div style=\"width: 8em; text-align: center;\"><strong><a href=\"https:\/\/www3.hhu.de\/stups\/prob\/\" target=\"_blank\" rel=\"noopener noreferrer\">ProB<\/a><\/strong><\/div>\n<\/td>\n<td>\n<div style=\"width: 12em; text-align: center;\"><a href=\"http:\/\/www.cs.hhu.de\/en\/research-groups\/software-engineering-and-programming-languages\/our-team\/team\/michael-leuschel.html\" target=\"_blank\" rel=\"noopener noreferrer\">Michael Leuschel<\/a><\/div>\n<\/td>\n<td>\n<div style=\"width: 5em; text-align: center;\">Oct 11<\/div>\n<\/td>\n<td><span style=\"font-size: 80%;\">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: &#8211; the <a href=\"https:\/\/gitlab.cs.uni-duesseldorf.de\/dgelessus\/prob2-jupyter-kernel\" target=\"_blank\" rel=\"noopener noreferrer\">ProB Jupyter kernel<\/a> for interactive notebooks for documentation; &#8211; the new Java FX user interface, along with new visualization techniques (e.g., based on SVG graphics); &#8211; a summary of new features in the ProB kernel (regular expressions, memoization, &#8230;) and the model checking backend (use of LTSmin, &#8230;); &#8211; a summary of recent industrial applications and T2 tool qualifications.<\/span><\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<div style=\"margin-bottom: 1em;\"><\/div>\n<\/li>\n<li>\n<div style=\"font-variant: small-caps;\">Univ. of Genoa, Univ. of Sassari<\/div>\n<div style=\"margin-bottom: 1em;\"><\/div>\n<table data-toggle=\"table\" border=\"1\" align=\"center\">\n<tbody>\n<tr>\n<td><strong>Tool<\/strong><\/td>\n<td><strong>Presenters<\/strong><\/td>\n<td><strong>When<\/strong><\/td>\n<td><strong>Description<\/strong><\/td>\n<\/tr>\n<tr>\n<td>\n<div style=\"width: 8em; text-align: center;\"><strong><a href=\"https:\/\/gitlab.sagelab.it\/sage\/ReqV\" target=\"_blank\" rel=\"noopener noreferrer\">ReqV<\/a><\/strong><\/div>\n<\/td>\n<td>\n<div style=\"width: 12em; text-align: center;\"><a href=\"http:\/\/idea.uniss.it\/index.php\/people\/pulina\" target=\"_blank\" rel=\"noopener noreferrer\">Luca Pulina<\/a><\/div>\n<\/td>\n<td>\n<div style=\"width: 5em; text-align: center;\">Oct 10-11<\/div>\n<\/td>\n<td><span style=\"font-size: 80%;\">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 =\u2217 c, where X is a variable of the system, c \u2208 R is a constant real number and the operator =\u2217\u2208 {&lt;, &lt;=, =, &gt;=, &gt;} 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.<\/span><\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<div style=\"margin-bottom: 1em;\"><\/div>\n<\/li>\n<li>\n<div style=\"font-variant: small-caps;\">Univ. of Oslo<\/div>\n<div style=\"margin-bottom: 1em;\"><\/div>\n<table data-toggle=\"table\" border=\"1\" align=\"center\">\n<tbody>\n<tr>\n<td><strong>Tool<\/strong><\/td>\n<td><strong>Presenters<\/strong><\/td>\n<td><strong>When<\/strong><\/td>\n<td><strong>Description<\/strong><\/td>\n<\/tr>\n<tr>\n<td>\n<div style=\"width: 8em; text-align: center;\"><strong><a href=\"https:\/\/www.mn.uio.no\/ifi\/english\/research\/projects\/railcons\/\" target=\"_blank\" rel=\"noopener noreferrer\">RailCons tools<\/a><\/strong><\/div>\n<\/td>\n<td>\n<div style=\"width: 12em; text-align: center;\"><a href=\"https:\/\/www.mn.uio.no\/its\/english\/people\/aca\/cristi\/\" target=\"_blank\" rel=\"noopener noreferrer\">Christian Johansen<\/a>, <a href=\"https:\/\/www.mn.uio.no\/ifi\/english\/research\/groups\/psy\/news\/news-Best-Paper-Award-Railway-Verification-iFM-2016.html\" target=\"_blank\" rel=\"noopener noreferrer\">Bj\u00f8rnar Luteberget<\/a><\/div>\n<\/td>\n<td>\n<div style=\"width: 5em; text-align: center;\">Oct 9-11<\/div>\n<\/td>\n<td><span style=\"font-size: 80%;\">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 &#8220;Automated Methods and Tools for Ensuring Consistency of Railway Designs&#8221;. 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&#8217;19, and the fifth is being submitted to iFM&#8217;19. More info exists on the project&#8217;s webpage (including videos, posters, papers, slides).<\/span><\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<div style=\"margin-bottom: 1em;\"><\/div>\n<\/li>\n<li>\n<div style=\"font-variant: small-caps;\">Uppsala University, Aalborg University<\/div>\n<div style=\"margin-bottom: 1em;\"><\/div>\n<table data-toggle=\"table\" border=\"1\" align=\"center\">\n<tbody>\n<tr>\n<td><strong>Tool<\/strong><\/td>\n<td><strong>Presenters<\/strong><\/td>\n<td><strong>When<\/strong><\/td>\n<td><strong>Description<\/strong><\/td>\n<\/tr>\n<tr>\n<td>\n<div style=\"width: 8em; text-align: center;\"><strong><a href=\"http:\/\/www.uppaal.org\/\" target=\"_blank\" rel=\"noopener noreferrer\">Uppaal<\/a><\/strong><\/div>\n<\/td>\n<td>\n<div style=\"width: 12em; text-align: center;\"><a href=\"https:\/\/dblp.org\/pers\/hd\/j\/Jensen:Peter_Gj=oslash=l\" target=\"_blank\" rel=\"noopener noreferrer\">Peter Gj\u00f8l Jensen<\/a>, <a href=\"http:\/\/people.cs.aau.dk\/~kgl\/\" target=\"_blank\" rel=\"noopener noreferrer\">Kim Guldstrand Larsen<\/a>, <a href=\"https:\/\/vbn.aau.dk\/da\/persons\/110046\" target=\"_blank\" rel=\"noopener noreferrer\">Marius Miku\u010dionis<\/a><\/div>\n<\/td>\n<td>\n<div style=\"width: 5em; text-align: center;\">Oct 10-11<\/div>\n<\/td>\n<td><span style=\"font-size: 80%;\">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.<\/span><\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<div style=\"margin-bottom: 1em;\"><\/div>\n<\/li>\n<\/ul>\n<div style=\"margin-bottom: 2em;\"><\/div>\n<h4>Call for Tools<\/h4>\n<p>The <strong>tool exhibition<\/strong> 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 <a href=\"http:\/\/formalmethods2019.inesctec.pt\/?page_id=353\">industry day<\/a> 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.<\/p>\n<h6>Financial conditions<\/h6>\n<ul>\n<li><strong>Academic tool<\/strong> developers: free with registration of the exhibitors.<\/li>\n<li><strong>Industrial tool<\/strong> developers: included with <a href=\"http:\/\/formalmethods2019.inesctec.pt\/?page_id=695\">sponsorship<\/a> of <strong>FM&#8217;19<\/strong> World Congress and registration of the exhibitors (basic sponsoring starts at \u20ac500, higher levels of sponsoring include registrations of participants).<\/li>\n<\/ul>\n<h6>Submisson<\/h6>\n<p>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 <strong>June 30, 2019<\/strong>, to the <strong>Tool Exhibition Chairs<\/strong>:<\/p>\n<ul>\n<li><a href=\"https:\/\/www.linkedin.com\/in\/thierry-lecomte-19695b\/\" target=\"_blank\" rel=\"noopener noreferrer\" data-ref=\"Thierry_Lecomte\">Thierry Lecomte<\/a> &#8211; Clearsy, thierry.lecomte@clearsy.com<\/li>\n<li><a href=\"https:\/\/members.loria.fr\/SMerz\/\" target=\"_blank\" rel=\"noopener noreferrer\" data-ref=\"Stephan_Merz\">Stephan Merz<\/a> &#8211; Inria, stephan.merz@inria.fr<\/li>\n<\/ul>\n<p>Informal enquiries are welcome.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>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 &#8230;<\/p>\n","protected":false},"author":3,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":[],"_links":{"self":[{"href":"http:\/\/formalmethods2019.inesctec.pt\/wp-json\/wp\/v2\/pages\/2101"}],"collection":[{"href":"http:\/\/formalmethods2019.inesctec.pt\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"http:\/\/formalmethods2019.inesctec.pt\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"http:\/\/formalmethods2019.inesctec.pt\/wp-json\/wp\/v2\/users\/3"}],"replies":[{"embeddable":true,"href":"http:\/\/formalmethods2019.inesctec.pt\/wp-json\/wp\/v2\/comments?post=2101"}],"version-history":[{"count":23,"href":"http:\/\/formalmethods2019.inesctec.pt\/wp-json\/wp\/v2\/pages\/2101\/revisions"}],"predecessor-version":[{"id":3835,"href":"http:\/\/formalmethods2019.inesctec.pt\/wp-json\/wp\/v2\/pages\/2101\/revisions\/3835"}],"wp:attachment":[{"href":"http:\/\/formalmethods2019.inesctec.pt\/wp-json\/wp\/v2\/media?parent=2101"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}