Model checking linear dynamical systems under floating-point rounding

DOI10.1007/978-3-031-30823-9_3zbMATH Open1543.68222MaRDI QIDQ6535340

David Purser, Engel Lefaucheux, Joël Ouaknine, Mohammadamin Sharifi

Publication date: 13 December 2023

zbMATH Keywords

dynamical systemsmodel checkingfloating-point arithmetic

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cites Work

• Unnamed Item
• Unnamed Item
• Reachability problems for Markov chains
• Symbolic decision procedure for termination of linear programs
• Wielandt's proof of the exponent inequality for primitive nonnegative matrices
• Combining tools for optimization and analysis of floating-point computations
• Algebraic model checking for discrete linear dynamical systems
• A two-phase approach for conditional floating-point verification
• Deductive verification of floating-point Java programs in KeY
• Principles of systems design. Essays dedicated to Thomas A. Henzinger on the occasion of his 60th birthday
• On the Complexity of the Orbit Problem
• Polynomial-time algorithm for the orbit problem
• Computer Aided Verification
• Positivity Problems for Low-Order Linear Recurrence Sequences
• Termination of Integer Linear Programs
• On robustness for the Skolem and positivity problems
• Skolem meets schanuel
• The pseudo-reachability problem for diagonalisable linear dynamical systems
• Parameter synthesis for parametric probabilistic dynamical systems and prefix-independent specifications

Related Items (1)

Model verification in dynamics through strict upper error bounds

This page was built for publication: Model checking linear dynamical systems under floating-point rounding