Deductive verification of real-time systems using STeP

DOI10.1016/S0304-3975(00)00088-8zbMath0954.68084OpenAlexW1521410408WikidataQ127098303 ScholiaQ127098303MaRDI QIDQ1589585

T. E. Uribe, Zohar Manna, Henny B. Sipma, Nikolaj Bjørner

Publication date: 12 December 2000

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0304-3975(00)00088-8

zbMATH Keywords

real-time systemsmodularityreceptivenesstemporal verification

Mathematics Subject Classification ID

Formal languages and automata (68Q45)

Related Items (3)

RGITL: a temporal logic framework for compositional reasoning about interleaved programs ⋮ A practical integration of first-order reasoning and decision procedures ⋮ Specification of real-time and hybrid systems in rewriting logic

Uses Software

• Kronos
• LARCH
• PVS
• HyTech
• Uppaal
• STeP

Cites Work

• A calculus of durations
• Liveness in timed and untimed systems
• A theory of timed automata
• Temporal proof methodologies for timed transition systems
• Automatic generation of invariants and intermediate assertions
• Verification of clocked and hybrid systems
• Generalized temporal verification diagrams
• A practical integration of first-order reasoning and decision procedures
• Modularity for timed and hybrid systems
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Deductive verification of real-time systems using STeP