Model Checking LTL Formulae in RAISE with FDR

DOI10.1007/978-3-642-00255-7_16MaRDI QIDQ3605469zbMATH OpenOpenAlexFDO

Authors Abigail Parisaca Vargas, Ana G. Garis, Chris George, Silvia Lizeth Tapia Tarifa

Publication date 24 February 2009

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-00255-7_16

zbMATH Keywords

toolsFDRCSPmodel checkingformal methodsrefinementLTLRAISERSL

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Model checking LTL using constraint programming
• scientific article; zbMATH DE number 1948409
• scientific article; zbMATH DE number 1487868
• LTL-model-checking via model composition
• LTL Generalized Model Checking Revisited
• LTL model checking for recursive programs
• scientific article; zbMATH DE number 1796131
• The Maude LTL model checker

Cites work

• scientific article; zbMATH DE number 1693430 (Why is no real title available?)
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 108391 (Why is no real title available?)
• scientific article; zbMATH DE number 1796123 (Why is no real title available?)
• scientific article; zbMATH DE number 795680 (Why is no real title available?)
• scientific article; zbMATH DE number 795688 (Why is no real title available?)
• The temporal semantics of concurrent programs

Cited in

(2)

• scientific article; zbMATH DE number 1693430 (Why is no real title available?)
• Model checking RAISE applicative specifications

Describes a project that uses

Uses Software

• FDR2
• LTL2BA
• SPIN
• RAISE

This page was built for publication: Model Checking LTL Formulae in RAISE with FDR

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