Modeling for Verification

DOI10.1007/978-3-319-10575-8_3MaRDI QIDQ3176361zbMATH OpenOpenAlexFDO

Authors Sanjit A. Seshia, Natasha Sharygina, Stavros Tripakis

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)

Recommendations

• Model Checking Software
• Formal verification of specification models
• scientific article; zbMATH DE number 910719
• Model checking
• Verification and validation of simulation models
• Hybrid Systems: Computation and Control
• Model checking, testing and verification working together

Cites work

• scientific article; zbMATH DE number 425394 (Why is no real title available?)
• scientific article; zbMATH DE number 3885321 (Why is no real title available?)
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 52331 (Why is no real title available?)
• scientific article; zbMATH DE number 3469994 (Why is no real title available?)
• scientific article; zbMATH DE number 3598362 (Why is no real title available?)
• scientific article; zbMATH DE number 1296290 (Why is no real title available?)
• scientific article; zbMATH DE number 1517989 (Why is no real title available?)
• scientific article; zbMATH DE number 1903346 (Why is no real title available?)
• scientific article; zbMATH DE number 910719 (Why is no real title available?)
• scientific article; zbMATH DE number 1412988 (Why is no real title available?)
• scientific article; zbMATH DE number 1444349 (Why is no real title available?)
• scientific article; zbMATH DE number 6783107 (Why is no real title available?)
• A calculus for network delay. I. Network elements in isolation
• A calculus of communicating systems
• A modular formal semantics for Ptolemy
• A theory of timed automata
• Abstract state machines. Theory and applications. International workshop, ASM 2000, Monte Verità, Switzerland, March 19--24, 2000. Proceedings
• Actors without Directors: A Kahnian View of Heterogeneous Systems
• Alternating Weighted Automata
• CPO semantics of timed interactive actor networks
• Denotational semantics in the cpo and metric approach
• Formal Methods for Components and Objects
• Graph-Based Algorithms for Boolean Function Manipulation
• LSCs: Breathing life into message sequence charts
• Marked directed graphs
• Model-checking in dense real-time
• On the verification of timed discrete-event models
• Properties of a Model for Parallel Computations: Determinacy, Termination, Queueing
• Proving the Correctness of Multiprocess Programs
• Quantitative Languages
• Recognizing safety and liveness
• Specification and Development of Interactive Systems
• Statecharts: a visual formalism for complex systems
• Stochastic model checking
• The Esterel synchronous programming language: Design, semantics, implementation
• The algorithmic analysis of hybrid systems
• Uppaal in a nutshell
• Validation of stochastic systems. A guide to current research.

Cited in

(8)

• A game of pawns
• A game of pawns
• Synergistic verification and validation of systems and software engineering models
• Machine learning and logic: a new frontier in artificial intelligence
• Temporal logic and fair discrete systems
• Abstraction and abstraction refinement
• scientific article; zbMATH DE number 5994839 (Why is no real title available?)
• Hybrid Systems: Computation and Control

Describes a project that uses

Uses Software

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

This page was built for publication: Modeling for Verification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3176361)