SMT-based scenario verification for hybrid systems

DOI10.1007/s10703-012-0158-0zbMath1284.03216WikidataQ62041178 ScholiaQ62041178MaRDI QIDQ2441772

Alessandro Cimatti, Sergio Mover, Stefano Tonetta

Publication date: 28 March 2014

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-012-0158-0

zbMATH Keywords

message sequence charts; bounded model checking; k-induction; network of hybrid automata; SMT-based verification

Mathematics Subject Classification ID

68Q45: Formal languages and automata

03D05: Automata and formal grammars in connection with logical questions

68Q60: Specification and verification (program logics, model checking, etc.)

68T20: Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)

03B44: Temporal logic

03D78: Computation over the reals, computable analysis

Related Items

SAT-LP-IIS joint-directed path-oriented bounded reachability analysis of linear hybrid automata, SMT-based scenario verification for hybrid systems, Unbounded-Time Analysis of Guarded LTI Systems with Inputs by Abstract Acceleration

Uses Software

• HySAT
• TASS
• HyTech
• NuSMV
• MathSAT
• HyDI

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Exploiting step semantics for efficient bounded model checking of asynchronous systems
• Scenario-based verification of real-time systems using UPPAAL
• HySAT: An efficient proof engine for bounded model checking of hybrid systems
• Interpreting message flow graphs
• SMT-based scenario verification for hybrid systems
• Towards a Notion of Unsatisfiable Cores for LTL
• On the Notion of Vacuous Truth
• Matching Scenarios with Timing Constraints
• Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems
• Bounded LTL model checking with stable models
• Automata and Logics for Timed Message Sequence Charts
• Verification, Model Checking, and Abstract Interpretation
• Computer Aided Verification
• LSCs: Breathing life into message sequence charts