Refinement of LTL formulas for abstract model checking

DOI10.1007/3-540-45789-5_28MaRDI QIDQ4411974zbMATH OpenFDO

Authors María del Mar Gallardo, Pedro Merino, Ernesto Pimentel

Publication date 13 July 2003

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

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2477/24770395.htm

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

• LTL Generalized Model Checking Revisited
• The abstraction-refinement framework in model checking
• Abstraction and Refinement in Model Checking
• Computer Aided Verification
• An efficient approach for abstraction-refinement in model checking
• Refining and compressing abstract model checking
• Lattice-based refinement in bounded model checking
• Model checking with formula-dependent abstract models
• A satisfiability-based approach to abstraction refinement in model checking

Cited in

(17)

• On decidability of LTL model checking for process rewrite systems
• Combining search space partition and abstraction for LTL model checking
• A semantic framework for the abstract model checking of tccp programs
• A program analysis framework for \textit{tccp} based on abstract interpretation
• A new unfolding approach to LTL model checking
• An Asymptotically Correct Finite Path Semantics for LTL
• Foundations for using linear temporal logic in Event-B refinement
• Semi-external LTL Model Checking
• LTL Generalized Model Checking Revisited
• Model Checking LTL Formulae in RAISE with FDR
• Model checking with formula-dependent abstract models
• Refining and compressing abstract model checking
• Manipulating LTL Formulas Using Spot 1.0
• Algebraic Methodology and Software Technology
• On Decidability of LTL Model Checking for Process Rewrite Systems
• The role of abstraction in model checking
• 3-valued abstraction: More precision at less cost

Describes a project that uses

Uses Software

• Bandera

This page was built for publication: Refinement of LTL formulas for abstract model checking

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