Modeling for Verification

DOI10.1007/978-3-319-10575-8_3zbMath1392.68264OpenAlexW2803980942MaRDI QIDQ3176361

Stavros Tripakis, Natasha Sharygina, Sanjit A. Seshia

Publication date: 20 July 2018

Published in: Handbook of Model Checking (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-10575-8_3

Mathematics Subject Classification ID

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

Related Items (3)

Temporal Logic and Fair Discrete Systems ⋮ Abstraction and Abstraction Refinement ⋮ Machine learning and logic: a new frontier in artificial intelligence

Uses Software

• Kronos
• Uppaal
• Ptolemy
• LUSTRE
• Metropolis
• Esterel

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The algorithmic analysis of hybrid systems
• Model-checking in dense real-time
• CPO semantics of timed interactive actor networks
• Statecharts: a visual formalism for complex systems
• Recognizing safety and liveness
• A calculus of communicating systems
• The Esterel synchronous programming language: Design, semantics, implementation
• A theory of timed automata
• Denotational semantics in the cpo and metric approach
• Abstract state machines. Theory and applications. International workshop, ASM 2000, Monte Verità, Switzerland, March 19--24, 2000. Proceedings
• Uppaal in a nutshell
• Validation of stochastic systems. A guide to current research.
• Marked directed graphs
• Specification and Development of Interactive Systems
• On the Verification of Timed Discrete-Event Models
• A modular formal semantics for Ptolemy
• Stochastic Model Checking
• Alternating Weighted Automata
• A calculus for network delay. I. Network elements in isolation
• Quantitative Languages
• Actors without Directors: A Kahnian View of Heterogeneous Systems
• Graph-Based Algorithms for Boolean Function Manipulation
• Proving the Correctness of Multiprocess Programs
• Properties of a Model for Parallel Computations: Determinacy, Termination, Queueing
• Formal Methods for Components and Objects
• LSCs: Breathing life into message sequence charts

This page was built for publication: Modeling for Verification