Titlebook: NASA Formal Methods; 12th International S Ritchie Lee,Susmit Jha,Dimitra Giannakopoulou Conference proceedings 2020 Springer Nature Switzer

DOTE

concentrate

From Passive to Active: Learning Timed Automata Efficientlyues attain increasing interest. Still, many learning approaches can only learn relatively simple types of models and advanced properties like time are ignored in many cases. In this paper we present an active model learning technique for timed automata. For this, we build upon an existing passive le

致词

Generating Correct-by-Construction Distributed Implementations from Formal Maude Designss of a system . can yield correct designs as well as reliable performance predictions. In this paper we present a correct-by-construction automatic transformation mapping such a verified formal specification of a system design in Maude to a . satisfying the same safety and liveness properties. Two c

敌意

细查

拥挤前

Simplifying Neural Networks Using Formal Verificationness of these engines on real-world DNNs is an important step towards their wider adoption. We present a tool that can leverage existing verification engines in performing a novel application: neural network simplification, through the reduction of the size of a DNN without harming its accuracy. We

Statins

Neural Simplex Architecturelearning) of autonomous and other complex systems without unduly sacrificing performance. NSA is inspired by the Simplex control architecture of Sha et al., but with some significant differences. In the traditional approach, the advanced controller (AC) is treated as a black box; when the decision m

丧失

Antimicrobial

Benchmarking Software Model Checkers on Automotive Code automatically generated from Simulink open-loop controller models. Its diverse features (decision logic, floating-point and pointer arithmetic, rate limiters and state-flow systems) and the extensive use of floating-point variables make verifying the code highly challenging. Our study reveals large