Safe Decomposition of Startup Requirements: Verification and Synthesis

DOI10.1007/978-3-030-45190-5_9OpenAlexW3016443504MaRDI QIDQ5039507

Greg Kimberly, Alessandro Cimatti, Alberto Griggio, Stefano Tonetta, Luca Geatti

Publication date: 13 October 2022

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-030-45190-5_9

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Uses Software

• MathSAT5

Cites Work

• Unnamed Item
• Combinatorial abstraction refinement for feasibility analysis of static priorities
• Stable models and difference logic
• A theory of timed automata
• SMT-based satisfiability of first-order LTL with event freezing functions and metric operators
• Infinite-state invariant checking with IC3 and predicate abstraction
• Parametric Deadlock-Freeness Checking Timed Automata
• Compositional Verification for Timed Systems Based on Automatic Invariant Generation
• AN INVERSE METHOD FOR PARAMETRIC TIMED AUTOMATA
• The MathSAT5 SMT Solver

This page was built for publication: Safe Decomposition of Startup Requirements: Verification and Synthesis