English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

: Model checking is a form of formal verification that can be used to check certain correctness properties of hardware or software systems mostly automatically. This project's overall objective was to improve the effectiveness and usefulness of model checking for embedded reactive software, the sort of software typically used in avionics. In particular, it sought to extend the scalability of model checking to systems with a very large or infinite state space, improve its accuracy, and develop modular model checking methods for infinite-state systems.! The project achieved its objectives by developing techniques based on automated reasoning engines called SMT solvers, which work with more powerful logics than propositional logic, the logic of choice in traditional model checking. These techniques were implemented in a automated model checker called Kind. Experimental results with Kind show that the new techniques provide superior scalability and precision. The tool has been adopted by several research groups from academia, government and industry. An internal reimplementation of Kind is now used regularly at a major avionics company.

Scalable and Accurate SMT-based Model Checking of Data Flow Systems