An introduction to practical formal methods using temporal logic
From MaRDI portal
automata-based model checking in SPINBüchi automatadeductionformal specificationmodel checkingsemanticsseparated normal formTSPASS tool
Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations (03-01) Temporal logic (03B44) Logic in computer science (03B70) Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)
Recommendations
Cited in
(12)- Concise guide to formal methods. Theory, fundamentals and industry applications
- A two-level approach based on model checking to support architecture conformance checking
- Guest editors' preface to special issue on interval temporal logics
- Compositional reasoning using intervals and time reversal
- Theorem proving using clausal resolution: from past to present
- Temporal logics in computer science. Finite-state systems
- Temporal logic and fair discrete systems
- Invariant-free clausal temporal resolution
- Specification and verification using temporal logics
- LTL-specification of bounded counter machines
- Fully automated verification of linear time-invariant systems against signal temporal logic specifications via reachability analysis
- Dynamic logic assigned to automata
This page was built for publication: An introduction to practical formal methods using temporal logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2996923)
