Dynamic partitioning in linear relation analysis: application to the verification of reactive systems

DOI10.1023/A:1024480913162zbMath1067.68091MaRDI QIDQ1424999

Bertrand Jeannet

Publication date: 15 March 2004

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

zbMATH Keywords

partitioningreactive systemsabstract interpretationprogram verificationlinear relation analysis

Mathematics Subject Classification ID

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

Related Items (10)

Computing Program Reliability Using Forward-Backward Precondition Analysis and Model Counting ⋮ Out of control: reducing probabilistic models by control-state elimination ⋮ Causality problem in real-time calculus ⋮ Symbolic supervisory control of infinite transition systems under partial observation using abstract interpretation ⋮ Applying abstract acceleration to (co-)reachability analysis of reactive programs ⋮ Model-Based Test Selection for Infinite-State Reactive Systems ⋮ Decentralized control of infinite systems ⋮ Symbolic Model-based Test Selection ⋮ Extending Abstract Acceleration Methods to Data-Flow Programs with Numerical Inputs ⋮ Automating the addition of fault tolerance with discrete controller synthesis

Uses Software

• Uppaal

This page was built for publication: Dynamic partitioning in linear relation analysis: application to the verification of reactive systems