Verification and Parameter Synthesis for Real-Time Programs using Refinement of Trace Abstraction*

DOI10.3233/FI-2021-1997zbMath1478.68053arXiv2007.10539MaRDI QIDQ4989166

Franck Cassez, Larsen Kim Guldstrand, Peter Gjøl Jensen

Publication date: 21 May 2021

Published in: Fundamenta Informaticae (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2007.10539

Mathematics Subject Classification ID

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

Uses Software

• IMITATOR
• PHAVer
• HyTech
• Uppaal
• z3
• SpaceEx

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• What's decidable about hybrid automata?
• A theory of timed automata
• Refinement of trace abstraction for real-time programs
• The expressive power of time Petri nets
• Symbolic quantitative robustness analysis of timed automata
• Infinite-state invariant checking with IC3 and predicate abstraction
• TCTL-preserving translations from timed-arc Petri nets to networks of timed automata
• Abstractions for hybrid systems
• Tools and algorithms for the construction and analysis of systems. 25 years of TACAS: TOOLympics, held as part of ETAPS 2019, Prague, Czech Republic, April 6--11, 2019. Proceedings. Part III
• Refinement of Trace Abstraction
• Trace Abstraction Refinement for Timed Automata
• Verification of Concurrent Programs Using Trace Abstraction Refinement
• Automatic Abstraction Refinement for Timed Automata
• A Counterexample-Guided Approach to Parameter Synthesis for Linear Hybrid Automata
• An iterative approach to precondition inference using constrained Horn clauses
• Hybrid Systems: Computation and Control
• Formal Modeling and Analysis of Timed Systems

This page was built for publication: Verification and Parameter Synthesis for Real-Time Programs using Refinement of Trace Abstraction*