Property Driven Three-Valued Model Checking on Hybrid Automata

DOI10.1007/978-3-642-02261-6_18MaRDI QIDQ3638286zbMATH OpenOpenAlexFDO

Authors Kerstin Bauer, Klaus Schneider, Raffaella Gentilini

Publication date 2 July 2009

Published in Logic, Language, Information and Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-02261-6_18

Mathematics Subject Classification ID

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

Recommendations

• A bounded model checker for three-valued abstractions of concurrent software systems
• Instantiation reduction in iterative parameterised three-valued model checking
• scientific article; zbMATH DE number 2102712
• Model checking algorithms for hyperproperties (invited paper)
• 2-valued and 3-valued abstraction-refinement in model checking
• Constraint reusing and k-induction for three-valued bounded model checking

Cites work

• A theory of timed automata
• Computer Aided Verification
• scientific article; zbMATH DE number 1303067 (Why is no real title available?)
• scientific article; zbMATH DE number 1306878 (Why is no real title available?)
• scientific article; zbMATH DE number 1956633 (Why is no real title available?)
• scientific article; zbMATH DE number 1507210 (Why is no real title available?)
• scientific article; zbMATH DE number 1798190 (Why is no real title available?)
• scientific article; zbMATH DE number 2085344 (Why is no real title available?)
• scientific article; zbMATH DE number 1444359 (Why is no real title available?)
• scientific article; zbMATH DE number 2242595 (Why is no real title available?)
• scientific article; zbMATH DE number 3073037 (Why is no real title available?)
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control
• O-minimal hybrid systems.
• Successive Abstractions of Hybrid Automata for Monotonic CTL Model Checking
• What's decidable about hybrid automata?

Describes a project that uses

Uses Software

• RSOLVER
• HSolver

This page was built for publication: Property Driven Three-Valued Model Checking on Hybrid Automata

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3638286)